(vl-make-duplicate-warning type locs modname) → warning
Function:
(defun vl-make-duplicate-warning (type locs modname) (declare (xargs :guard (and (stringp type) (vl-locationlist-p locs) (stringp modname)))) (let ((__function__ 'vl-make-duplicate-warning)) (declare (ignorable __function__)) (b* ((locs (list-fix locs)) (elide-p (> (len locs) 9)) (elided-locs (if elide-p (take 9 locs) locs))) (make-vl-warning :type :vl-warn-duplicates :msg (cat "In module ~m0, found duplicated " type " at " (vl-locationlist-string (len elided-locs)) (if elide-p " (and other locations)." ".")) :args (cons modname elided-locs) :fatalp nil :fn 'vl-make-duplicate-warning))))
Theorem:
(defthm vl-warning-p-of-vl-make-duplicate-warning (b* ((warning (vl-make-duplicate-warning type locs modname))) (vl-warning-p warning)) :rule-classes :rewrite)