		Search-engine friendly clone of the ACL2 documentation.

Duplicate-detect

Vl-duplicate-assign-warnings

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

Definitions and Theorems

Function: vl-duplicate-assign-warnings

(defun vl-duplicate-assign-warnings (dupes fixed orig modname)
  (declare (xargs :guard (and (vl-assignlist-p dupes)
                              (vl-assignlist-p fixed)
                              (vl-assignlist-p orig)
                              (stringp modname))))
  (declare (xargs :guard (same-lengthp fixed orig)))
  (let ((__function__ 'vl-duplicate-assign-warnings))
    (declare (ignorable __function__))
    (b* (((when (atom dupes)) nil)
         (locs (vl-duplicate-assign-locations (car dupes)
                                              fixed orig))
         (lvalue (vl-assign->lvalue (car dupes)))
         (type (if (vl-idexpr-p lvalue)
                   (cat "assignments to "
                        (vl-idexpr->name lvalue))
                 (let ((lvalue-str (vl-pps-origexpr lvalue)))
                   (if (< (length lvalue-str) 40)
                       (cat "assignments to " lvalue-str)
                     (cat "assignments to \""
                          (subseq lvalue-str 0 40)
                          "...\"")))))
         (warning (vl-make-duplicate-warning type locs modname))
         (rest (vl-duplicate-assign-warnings (cdr dupes)
                                             fixed orig modname)))
      (cons warning rest))))

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

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