(vl-maybe-warn-about-implicit-truncation lvalue lw expr ew ss) → warnings
Function:
(defun vl-maybe-warn-about-implicit-truncation (lvalue lw expr ew ss) (declare (xargs :guard (and (vl-maybe-expr-p lvalue) (natp lw) (vl-expr-p expr) (natp ew) (vl-scopestack-p ss)))) (let ((__function__ 'vl-maybe-warn-about-implicit-truncation)) (declare (ignorable __function__)) (b* ((lw (lnfix lw)) (ew (lnfix ew)) ((unless (< lw ew)) nil) (lvalue (vl-maybe-expr-fix lvalue)) (expr (vl-expr-fix expr)) ((when (vl-okay-to-truncate-expr lw expr ss)) nil) (atoms (vl-expr-interesting-size-atoms expr)) (toobig (vl-collect-toobig-constant-atoms lw atoms)) (probably-minor-p (and (equal ew 32) (not toobig) (vl-some-unsized-atom-p atoms ss))) (warning (make-vl-warning :type (if probably-minor-p :vl-warn-truncation-minor :vl-warn-truncation) :msg "implicit truncation from ~x0-bit expression ~ to ~x1-bit lvalue/type.~% ~ lhs: ~a2~% ~ rhs: ~a3~%~%" :args (list ew lw (or lvalue 'n/a) expr) :fatalp nil :fn __function__))) (list warning))))
Theorem:
(defthm vl-warninglist-p-of-vl-maybe-warn-about-implicit-truncation (b* ((warnings (vl-maybe-warn-about-implicit-truncation lvalue lw expr ew ss))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-maybe-warn-about-implicit-truncation (b* ((?warnings (vl-maybe-warn-about-implicit-truncation lvalue lw expr ew ss))) (true-listp warnings)) :rule-classes :type-prescription)
Theorem:
(defthm vl-maybe-warn-about-implicit-truncation-of-vl-maybe-expr-fix-lvalue (equal (vl-maybe-warn-about-implicit-truncation (vl-maybe-expr-fix lvalue) lw expr ew ss) (vl-maybe-warn-about-implicit-truncation lvalue lw expr ew ss)))
Theorem:
(defthm vl-maybe-warn-about-implicit-truncation-vl-maybe-expr-equiv-congruence-on-lvalue (implies (vl-maybe-expr-equiv lvalue lvalue-equiv) (equal (vl-maybe-warn-about-implicit-truncation lvalue lw expr ew ss) (vl-maybe-warn-about-implicit-truncation lvalue-equiv lw expr ew ss))) :rule-classes :congruence)
Theorem:
(defthm vl-maybe-warn-about-implicit-truncation-of-nfix-lw (equal (vl-maybe-warn-about-implicit-truncation lvalue (nfix lw) expr ew ss) (vl-maybe-warn-about-implicit-truncation lvalue lw expr ew ss)))
Theorem:
(defthm vl-maybe-warn-about-implicit-truncation-nat-equiv-congruence-on-lw (implies (acl2::nat-equiv lw lw-equiv) (equal (vl-maybe-warn-about-implicit-truncation lvalue lw expr ew ss) (vl-maybe-warn-about-implicit-truncation lvalue lw-equiv expr ew ss))) :rule-classes :congruence)
Theorem:
(defthm vl-maybe-warn-about-implicit-truncation-of-vl-expr-fix-expr (equal (vl-maybe-warn-about-implicit-truncation lvalue lw (vl-expr-fix expr) ew ss) (vl-maybe-warn-about-implicit-truncation lvalue lw expr ew ss)))
Theorem:
(defthm vl-maybe-warn-about-implicit-truncation-vl-expr-equiv-congruence-on-expr (implies (vl-expr-equiv expr expr-equiv) (equal (vl-maybe-warn-about-implicit-truncation lvalue lw expr ew ss) (vl-maybe-warn-about-implicit-truncation lvalue lw expr-equiv ew ss))) :rule-classes :congruence)
Theorem:
(defthm vl-maybe-warn-about-implicit-truncation-of-nfix-ew (equal (vl-maybe-warn-about-implicit-truncation lvalue lw expr (nfix ew) ss) (vl-maybe-warn-about-implicit-truncation lvalue lw expr ew ss)))
Theorem:
(defthm vl-maybe-warn-about-implicit-truncation-nat-equiv-congruence-on-ew (implies (acl2::nat-equiv ew ew-equiv) (equal (vl-maybe-warn-about-implicit-truncation lvalue lw expr ew ss) (vl-maybe-warn-about-implicit-truncation lvalue lw expr ew-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-maybe-warn-about-implicit-truncation-of-vl-scopestack-fix-ss (equal (vl-maybe-warn-about-implicit-truncation lvalue lw expr ew (vl-scopestack-fix ss)) (vl-maybe-warn-about-implicit-truncation lvalue lw expr ew ss)))
Theorem:
(defthm vl-maybe-warn-about-implicit-truncation-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-maybe-warn-about-implicit-truncation lvalue lw expr ew ss) (vl-maybe-warn-about-implicit-truncation lvalue lw expr ew ss-equiv))) :rule-classes :congruence)