		Search-engine friendly clone of the ACL2 documentation.

Duplicate-detect

Vl-duplicate-gateinst-warnings

Signature
(vl-duplicate-gateinst-warnings dupes fixed orig modname) → warnings
Arguments: dupes — The gateinsts that were duplicated. (fixed).
Guard (vl-gateinstlist-p dupes).; fixed — Fixed versions of orig.
Guard (vl-gateinstlist-p fixed).; orig — Original gate instances, i.e., before fixing.
Guard (vl-gateinstlist-p orig).; modname — Guard (stringp modname).
Returns: warnings — Warnings for each duplicate gateinst.
Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-duplicate-gateinst-warnings

(defun vl-duplicate-gateinst-warnings (dupes fixed orig modname)
 (declare (xargs :guard (and (vl-gateinstlist-p dupes)
                             (vl-gateinstlist-p fixed)
                             (vl-gateinstlist-p orig)
                             (stringp modname))))
 (declare (xargs :guard (same-lengthp fixed orig)))
 (let ((__function__ 'vl-duplicate-gateinst-warnings))
   (declare (ignorable __function__))
   (b*
    (((when (atom dupes)) nil)
     (locs (vl-duplicate-gateinst-locations (car dupes)
                                            fixed orig))
     (warning
          (vl-make-duplicate-warning "gate instances" locs modname))
     (rest (vl-duplicate-gateinst-warnings (cdr dupes)
                                           fixed orig modname)))
    (cons warning rest))))

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

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