Remove any warning wires that we know are used and set.
(vl-clean-up-warning-wires wires alist) → new-warning-wires
We are given the list of warning wires that have been generated, and the completedly wireinfo alist. We only want to actually warn about wires which were (1) flagged as maybe bad, and (2) currently appear to be unset or unused. The other wires are thrown away.
Function:
(defun vl-clean-up-warning-wires (wires alist) (declare (xargs :guard (and (string-listp wires) (vl-wireinfo-alistp alist)))) (let ((__function__ 'vl-clean-up-warning-wires)) (declare (ignorable __function__)) (b* (((when (atom wires)) nil) (entry (cdr (hons-get (car wires) alist))) (really-warnp (or (not entry) (not (vl-wireinfo->usedp entry)) (not (vl-wireinfo->setp entry)))) ((when really-warnp) (cons (car wires) (vl-clean-up-warning-wires (cdr wires) alist)))) (vl-clean-up-warning-wires (cdr wires) alist))))
Theorem:
(defthm string-listp-of-vl-clean-up-warning-wires (implies (and (force (string-listp wires)) (force (vl-wireinfo-alistp alist))) (b* ((new-warning-wires (vl-clean-up-warning-wires wires alist))) (string-listp new-warning-wires))) :rule-classes :rewrite)