		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-print-certain-warnings

Print warnings of interest to standard output, while hiding other warnings.

Signature
(vl-print-certain-warnings mods show hide) → *
Arguments: mods — Modules to print warnings for.
Guard (vl-modulelist-p mods).; show — Types of warnings to show.
Guard (symbol-listp show).; hide — Types of warnings to hide.
Guard (symbol-listp hide).

You can use this to print just a few warnings you are interested in while hiding other warnings you know you are not interested in. If there are warnings of other types (that you haven't said to show or hide), they too will be hidden but you'll at least get a message saying that they aren't being shown.

Definitions and Theorems

Function: vl-print-certain-warnings

(defun vl-print-certain-warnings (mods show hide)
 (declare (xargs :guard (and (vl-modulelist-p mods)
                             (symbol-listp show)
                             (symbol-listp hide))))
 (let ((__function__ 'vl-print-certain-warnings))
  (declare (ignorable __function__))
  (b* ((warnings (vl-modulelist-flat-warnings-exec mods nil))
       (types (mergesort (vl-warninglist->types-exec warnings nil)))
       (hide (if hide (mergesort hide) types))
       (show (mergesort show))
       (misc (difference types (union show hide)))
       (warnings (vl-keep-warnings show warnings)))
    (vl-cw-ps-seq
         (vl-ps-update-autowrap-col 65)
         (vl-print-warnings warnings)
         (vl-println "")
         (if (not misc)
             ps
           (vl-ps-seq (vl-cw "Note: not showing ~&0 warnings.~%"
                             misc)
                      (vl-println "")))))))