		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-lint-print-all-warnings

Signature
(vl-lint-print-all-warnings filename label reportcard &key (ps 'ps)) → ps
Arguments: filename — Guard (stringp filename).; label — Guard (stringp label).; reportcard — Guard (vl-reportcard-p reportcard).

Definitions and Theorems

Function: vl-lint-print-all-warnings-fn

(defun vl-lint-print-all-warnings-fn (filename label reportcard ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (and (stringp filename)
                             (stringp label)
                             (vl-reportcard-p reportcard))))
 (let ((__function__ 'vl-lint-print-all-warnings))
  (declare (ignorable __function__))
  (b* ((reportcard (vl-clean-reportcard reportcard))
       (count (length (append-alist-vals reportcard)))
       (- (cond ((eql count 0)
                 (cw "~s0: No ~s1 Warnings.~%"
                     filename label))
                ((eql count 1)
                 (cw "~s0: One ~s1 Warning.~%"
                     filename label))
                (t (cw "~s0: ~x1 ~s2 Warnings.~%"
                       filename count label)))))
   (vl-ps-seq (cond ((eql count 0)
                     (vl-cw "No ~s0 Warnings.~%~%" label))
                    ((eql count 1)
                     (vl-cw "One ~s0 Warning:~%~%" label))
                    (t (vl-cw "~x0 ~s1 Warnings:~%~%" count label)))
              (vl-print-reportcard reportcard
                                   :elide nil)))))