		Search-engine friendly clone of the ACL2 documentation.

Duplicate-detect

Vl-duplicate-warning

Signature
(vl-duplicate-warning type dupes) → warning
Arguments: type — Guard (stringp type).; dupes — Guard (vl-modelementlist-p dupes).
Returns: warning — Type (vl-warning-p warning).

Definitions and Theorems

Function: vl-duplicate-warning

(defun vl-duplicate-warning (type dupes)
 (declare (xargs :guard (and (stringp type)
                             (vl-modelementlist-p dupes))))
 (declare (xargs :guard (<= 2 (len dupes))))
 (let ((__function__ 'vl-duplicate-warning))
   (declare (ignorable __function__))
   (b* ((msg (with-local-ps
                  (vl-ps-update-autowrap-col 100)
                  (vl-ps-update-autowrap-ind 10)
                  (vl-print "Found duplicated ")
                  (vl-print-str type)
                  (vl-println ":")
                  (vl-indent 6)
                  (vl-print "  // From ")
                  (vl-print-loc (vl-modelement->loc (first dupes)))
                  (vl-println "")
                  (vl-indent 6)
                  (vl-pp-modelement (first dupes))
                  (vl-indent 6)
                  (vl-print "  // From ")
                  (vl-print-loc (vl-modelement->loc (second dupes)))
                  (vl-println "")
                  (vl-indent 6)
                  (vl-pp-modelement (second dupes))
                  (if (atom (cddr dupes))
                      ps
                    (vl-ps-seq (vl-println "")
                               (vl-indent 6)
                               (vl-print "  // And ")
                               (vl-print-nat (- (len dupes) 2))
                               (vl-print " more."))))))
     (make-vl-warning :type :vl-warn-duplicates
                      :msg "~s0"
                      :args (list msg dupes)
                      :fatalp nil
                      :fn __function__))))

Theorem: vl-warning-p-of-vl-duplicate-warning

(defthm vl-warning-p-of-vl-duplicate-warning
  (b* ((warning (vl-duplicate-warning type dupes)))
    (vl-warning-p warning))
  :rule-classes :rewrite)