(vl-casestmt-matchexpr-size-warnings test match-exprs ctx) → warnings
Function:
(defun vl-casestmt-matchexpr-size-warnings (test match-exprs ctx) (declare (xargs :guard (and (vl-expr-p test) (vl-exprlist-p match-exprs) (vl-modelement-p ctx)))) (let ((__function__ 'vl-casestmt-matchexpr-size-warnings)) (declare (ignorable __function__)) (b* (((when (atom match-exprs)) nil) (test (vl-expr-fix test)) (expr1 (vl-expr-fix (car match-exprs))) (ctx (vl-modelement-fix ctx)) (rest (vl-casestmt-matchexpr-size-warnings test (cdr match-exprs) ctx)) ((unless (vl-expr->finaltype expr1)) (warn :type :vl-case-stmt-type :msg "In ~a0: failed to determine signedness of case-statement ~ match expression: ~a1." :args (list ctx expr1) :acc rest)) ((unless (eql (vl-expr->finalwidth test) (vl-expr->finalwidth expr1))) (warn :type :vl-case-stmt-size :msg "In ~a0: case statement sizes are incompatible:~% ~ - ~x1-bit test: ~a3~% ~ - ~x2-bit match: ~a4" :args (list ctx (vl-expr->finalwidth test) (vl-expr->finalwidth expr1) test expr1) :acc rest))) rest)))
Theorem:
(defthm vl-warninglist-p-of-vl-casestmt-matchexpr-size-warnings (b* ((warnings (vl-casestmt-matchexpr-size-warnings test match-exprs ctx))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-casestmt-matchexpr-size-warnings (b* ((warnings (vl-casestmt-matchexpr-size-warnings test match-exprs ctx))) (true-listp warnings)) :rule-classes :type-prescription)
Theorem:
(defthm vl-casestmt-matchexpr-size-warnings-correct (implies (not (vl-casestmt-matchexpr-size-warnings test match-exprs ctx)) (vl-casestmt-matchexpr-sizes-agreep test match-exprs)))
Theorem:
(defthm vl-casestmt-matchexpr-size-warnings-of-vl-expr-fix-test (equal (vl-casestmt-matchexpr-size-warnings (vl-expr-fix test) match-exprs ctx) (vl-casestmt-matchexpr-size-warnings test match-exprs ctx)))
Theorem:
(defthm vl-casestmt-matchexpr-size-warnings-vl-expr-equiv-congruence-on-test (implies (vl-expr-equiv test test-equiv) (equal (vl-casestmt-matchexpr-size-warnings test match-exprs ctx) (vl-casestmt-matchexpr-size-warnings test-equiv match-exprs ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-matchexpr-size-warnings-of-vl-exprlist-fix-match-exprs (equal (vl-casestmt-matchexpr-size-warnings test (vl-exprlist-fix match-exprs) ctx) (vl-casestmt-matchexpr-size-warnings test match-exprs ctx)))
Theorem:
(defthm vl-casestmt-matchexpr-size-warnings-vl-exprlist-equiv-congruence-on-match-exprs (implies (vl-exprlist-equiv match-exprs match-exprs-equiv) (equal (vl-casestmt-matchexpr-size-warnings test match-exprs ctx) (vl-casestmt-matchexpr-size-warnings test match-exprs-equiv ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-matchexpr-size-warnings-of-vl-modelement-fix-ctx (equal (vl-casestmt-matchexpr-size-warnings test match-exprs (vl-modelement-fix ctx)) (vl-casestmt-matchexpr-size-warnings test match-exprs ctx)))
Theorem:
(defthm vl-casestmt-matchexpr-size-warnings-vl-modelement-equiv-congruence-on-ctx (implies (vl-modelement-equiv ctx ctx-equiv) (equal (vl-casestmt-matchexpr-size-warnings test match-exprs ctx) (vl-casestmt-matchexpr-size-warnings test match-exprs ctx-equiv))) :rule-classes :congruence)