(vl-mark-wires-for-arguments x alist) → (mv new-alist warning-wires)
Function:
(defun vl-mark-wires-for-arguments (x alist) (declare (xargs :guard (and (vl-arguments-p x) (vl-wireinfo-alistp alist)))) (let ((__function__ 'vl-mark-wires-for-arguments)) (declare (ignorable __function__)) (vl-arguments-case x :vl-arguments-named (mv alist (vl-exprlist-names (vl-namedarglist-allexprs x.args))) :vl-arguments-plain (vl-mark-wires-for-plainarglist x.args alist nil))))
Theorem:
(defthm vl-wireinfo-alistp-of-vl-mark-wires-for-arguments.new-alist (implies (and (force (vl-arguments-p x)) (force (vl-wireinfo-alistp alist))) (b* (((mv ?new-alist ?warning-wires) (vl-mark-wires-for-arguments x alist))) (vl-wireinfo-alistp new-alist))) :rule-classes :rewrite)
Theorem:
(defthm string-listp-of-vl-mark-wires-for-arguments.warning-wires (implies (and (force (vl-arguments-p x)) (force (vl-wireinfo-alistp alist))) (b* (((mv ?new-alist ?warning-wires) (vl-mark-wires-for-arguments x alist))) (string-listp warning-wires))) :rule-classes :rewrite)