Lint-like warnings about right hand sides being extended.
(vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx warnings) → new-warnings
Function:
(defun vl-warn-about-implicit-extension (lhs-size x-selfsize x ss ctx warnings) (declare (xargs :guard (and (natp lhs-size) (natp x-selfsize) (vl-expr-p x) (vl-scopestack-p ss) (vl-context-p ctx) (vl-warninglist-p warnings)))) (declare (xargs :guard (> lhs-size x-selfsize))) (let ((__function__ 'vl-warn-about-implicit-extension)) (declare (ignorable __function__)) (b* ((lhs-size (lnfix lhs-size)) (x-selfsize (lnfix x-selfsize)) (x (vl-expr-fix x)) (ss (vl-scopestack-fix ss)) (ctx (vl-context-fix ctx)) (type (vl-classify-extension-warning-hook lhs-size x-selfsize x ss ctx)) ((unless type) (ok))) (warn :type type :msg "~a0: implicit extension from ~x1-bit expression to ~x2-bit ~ lvalue.~% rhs: ~a3" :args (list ctx x-selfsize lhs-size x)))))
Theorem:
(defthm vl-warninglist-p-of-vl-warn-about-implicit-extension (b* ((new-warnings (vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-warn-about-implicit-extension-of-nfix-lhs-size (equal (vl-warn-about-implicit-extension (nfix lhs-size) x-selfsize x ss ctx warnings) (vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx warnings)))
Theorem:
(defthm vl-warn-about-implicit-extension-nat-equiv-congruence-on-lhs-size (implies (acl2::nat-equiv lhs-size lhs-size-equiv) (equal (vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx warnings) (vl-warn-about-implicit-extension lhs-size-equiv x-selfsize x ss ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-warn-about-implicit-extension-of-nfix-x-selfsize (equal (vl-warn-about-implicit-extension lhs-size (nfix x-selfsize) x ss ctx warnings) (vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx warnings)))
Theorem:
(defthm vl-warn-about-implicit-extension-nat-equiv-congruence-on-x-selfsize (implies (acl2::nat-equiv x-selfsize x-selfsize-equiv) (equal (vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx warnings) (vl-warn-about-implicit-extension lhs-size x-selfsize-equiv x ss ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-warn-about-implicit-extension-of-vl-expr-fix-x (equal (vl-warn-about-implicit-extension lhs-size x-selfsize (vl-expr-fix x) ss ctx warnings) (vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx warnings)))
Theorem:
(defthm vl-warn-about-implicit-extension-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx warnings) (vl-warn-about-implicit-extension lhs-size x-selfsize x-equiv ss ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-warn-about-implicit-extension-of-vl-scopestack-fix-ss (equal (vl-warn-about-implicit-extension lhs-size x-selfsize x (vl-scopestack-fix ss) ctx warnings) (vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx warnings)))
Theorem:
(defthm vl-warn-about-implicit-extension-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx warnings) (vl-warn-about-implicit-extension lhs-size x-selfsize x ss-equiv ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-warn-about-implicit-extension-of-vl-context-fix-ctx (equal (vl-warn-about-implicit-extension lhs-size x-selfsize x ss (vl-context-fix ctx) warnings) (vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx warnings)))
Theorem:
(defthm vl-warn-about-implicit-extension-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx warnings) (vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-warn-about-implicit-extension-of-vl-warninglist-fix-warnings (equal (vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx (vl-warninglist-fix warnings)) (vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx warnings)))
Theorem:
(defthm vl-warn-about-implicit-extension-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx warnings) (vl-warn-about-implicit-extension lhs-size x-selfsize x ss ctx warnings-equiv))) :rule-classes :congruence)