(vl-mark-wire-used x warnp alist) → new-alist
Function:
(defun vl-mark-wire-used (x warnp alist) (declare (xargs :guard (and (stringp x) (vl-wireinfo-alistp alist)))) (let ((__function__ 'vl-mark-wire-used)) (declare (ignorable __function__)) (b* ((info (cdr (hons-get x alist))) (- (or info (not warnp) (cw "In vl-mark-wire-used: expected all wires to be in the ~ wireinfo-alist, but ~x0 is not. Adding a new entry for ~ it.~%" x))) (current-usedp (and info (vl-wireinfo->usedp info))) (current-setp (and info (vl-wireinfo->setp info))) ((when current-usedp) alist)) (hons-acons x (make-vl-wireinfo :usedp t :setp current-setp) alist))))
Theorem:
(defthm vl-wireinfo-alistp-of-vl-mark-wire-used (implies (and (force (stringp x)) (force (vl-wireinfo-alistp alist))) (b* ((new-alist (vl-mark-wire-used x warnp alist))) (vl-wireinfo-alistp new-alist))) :rule-classes :rewrite)