Generate any sizing warnings for an final statement.
(vl-final-size-warnings x ss scopes) → warnings
Function:
(defun vl-final-size-warnings (x ss scopes) (declare (xargs :guard (and (vl-final-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (let ((__function__ 'vl-final-size-warnings)) (declare (ignorable __function__)) (b* (((vl-final x) (vl-final-fix x)) ((mv ?ok warnings ?svstmts) (vl-stmt->svstmts x.stmt ss scopes (make-svstmt-config :nonblockingp t) nil))) warnings)))
Theorem:
(defthm vl-warninglist-p-of-vl-final-size-warnings (b* ((warnings (vl-final-size-warnings x ss scopes))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-final-size-warnings-of-vl-final-fix-x (equal (vl-final-size-warnings (vl-final-fix x) ss scopes) (vl-final-size-warnings x ss scopes)))
Theorem:
(defthm vl-final-size-warnings-vl-final-equiv-congruence-on-x (implies (vl-final-equiv x x-equiv) (equal (vl-final-size-warnings x ss scopes) (vl-final-size-warnings x-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-final-size-warnings-of-vl-scopestack-fix-ss (equal (vl-final-size-warnings x (vl-scopestack-fix ss) scopes) (vl-final-size-warnings x ss scopes)))
Theorem:
(defthm vl-final-size-warnings-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-final-size-warnings x ss scopes) (vl-final-size-warnings x ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-final-size-warnings-of-vl-elabscopes-fix-scopes (equal (vl-final-size-warnings x ss (vl-elabscopes-fix scopes)) (vl-final-size-warnings x ss scopes)))
Theorem:
(defthm vl-final-size-warnings-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-final-size-warnings x ss scopes) (vl-final-size-warnings x ss scopes-equiv))) :rule-classes :congruence)