Annotate vardecls with the results of use-set analysis.
(vl-annotate-vardecl-with-wireinfo x alist wwires) → new-x
We add as many as two annotations to X. The possible annotations we add are
(defun vl-annotate-vardecl-with-wireinfo (x alist wwires) (declare (xargs :guard (and (vl-vardecl-p x) (vl-wireinfo-alistp alist) (string-listp wwires)))) (let ((__function__ 'vl-annotate-vardecl-with-wireinfo)) (declare (ignorable __function__)) (b* ((name (vl-vardecl->name x)) (info (cdr (hons-get name alist))) ((unless info) (raise "No wireinfo entry for ~s0." name) x) (usedp (vl-wireinfo->usedp info)) (setp (vl-wireinfo->setp info)) ((when (and usedp setp)) x) (atts (vl-vardecl->atts x)) (warnp (member-equal name wwires)) (atts (cond (usedp atts) (warnp (cons (list "VL_MAYBE_UNUSED") atts)) (t (cons (list "VL_UNUSED") atts)))) (atts (cond (setp atts) (warnp (cons (list "VL_MAYBE_UNSET") atts)) (t (cons (list "VL_UNSET") atts))))) (change-vl-vardecl x :atts atts))))
(defthm vl-vardecl-p-of-vl-annotate-vardecl-with-wireinfo (implies (force (vl-vardecl-p x)) (b* ((new-x (vl-annotate-vardecl-with-wireinfo x alist wwires))) (vl-vardecl-p new-x))) :rule-classes :rewrite)