		Search-engine friendly clone of the ACL2 documentation.

Duplicate-detect

Vl-duplicate-warnings

Signature
(vl-duplicate-warnings dupes fixed orig) → warnings
Arguments: dupes — The duplicated (stripped) elements.
Guard (vl-modelementlist-p dupes).; fixed — The stripped versions of orig.
Guard (vl-modelementlist-p fixed).; orig — Original elements (before fixing).
Guard (vl-modelementlist-p orig).
Returns: warnings — Warnings for each duplicate modinst.
Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-duplicate-warnings

(defun vl-duplicate-warnings (dupes fixed orig)
 (declare (xargs :guard (and (vl-modelementlist-p dupes)
                             (vl-modelementlist-p fixed)
                             (vl-modelementlist-p orig))))
 (declare (xargs :guard (same-lengthp fixed orig)))
 (let ((__function__ 'vl-duplicate-warnings))
  (declare (ignorable __function__))
  (b*
   (((when (atom dupes)) nil)
    (matches
         (vl-collect-original-elements-matching-dupe (car dupes)
                                                     fixed orig))
    ((unless (<= 2 (len matches)))
     (raise
      "Not enough matches for duplicate?  Jared thinks this should be impossible."))
    (warning
     (vl-duplicate-warning
        (case (tag (car dupes))
              (:vl-modinst "module instances")
              (:vl-assign "assignments")
              (:vl-gateinst "gate instances")
              (:vl-alias "aliases")
              (:vl-always "always blocks")
              (:vl-initial "initial blocks")
              (:vl-final "final statements")
              (:vl-property "property declarations")
              (:vl-sequence "sequence declarations")
              (:vl-assertion "immediate assertions")
              (:vl-cassertion "concurrent assertions")
              (otherwise (ec-call (symbol-name (tag (car dupes))))))
        matches))
    (rest (vl-duplicate-warnings (cdr dupes)
                                 fixed orig)))
   (cons warning rest))))

Theorem: vl-warninglist-p-of-vl-duplicate-warnings

(defthm vl-warninglist-p-of-vl-duplicate-warnings
  (b* ((warnings (vl-duplicate-warnings dupes fixed orig)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)