(vl-mark-wires-for-modinst x alist warnings) → (mv new-alist new-warnings warning-wires)
Function:
(defun vl-mark-wires-for-modinst (x alist warnings) (declare (xargs :guard (and (vl-modinst-p x) (vl-wireinfo-alistp alist) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-mark-wires-for-modinst)) (declare (ignorable __function__)) (b* ((portargs (vl-modinst->portargs x)) (paramargs (vl-modinst->paramargs x)) (range (vl-modinst->range x)) ((mv alist warning-wires) (vl-mark-wires-for-arguments portargs alist)) (warnings (if (not warning-wires) (ok) (warn :type :vl-modinst-args-unresolved :msg "In ~a0, arguments are not resolved." :args (list x)))) (param-wires (vl-exprlist-names (vl-paramargs-allexprs paramargs))) (range-wires (vl-exprlist-names (vl-maybe-range-allexprs range))) (alist (vl-mark-wires-used param-wires t alist)) (alist (vl-mark-wires-used range-wires t alist))) (mv alist warnings warning-wires))))
Theorem:
(defthm vl-wireinfo-alistp-of-vl-mark-wires-for-modinst.new-alist (implies (and (force (vl-modinst-p x)) (force (vl-wireinfo-alistp alist))) (b* (((mv ?new-alist ?new-warnings ?warning-wires) (vl-mark-wires-for-modinst x alist warnings))) (vl-wireinfo-alistp new-alist))) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-mark-wires-for-modinst.new-warnings (b* (((mv ?new-alist ?new-warnings ?warning-wires) (vl-mark-wires-for-modinst x alist warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm string-listp-of-vl-mark-wires-for-modinst.warning-wires (implies (and (force (vl-modinst-p x)) (force (vl-wireinfo-alistp alist))) (b* (((mv ?new-alist ?new-warnings ?warning-wires) (vl-mark-wires-for-modinst x alist warnings))) (string-listp warning-wires))) :rule-classes :rewrite)