Lint-like warnings about right hand sides being extended.
(vl-maybe-warn-about-implicit-extension lhs-size x-selfsize x ss) → warnings
Function:
(defun vl-maybe-warn-about-implicit-extension (lhs-size x-selfsize x ss) (declare (xargs :guard (and (natp lhs-size) (natp x-selfsize) (vl-expr-p x) (vl-scopestack-p ss)))) (let ((__function__ 'vl-maybe-warn-about-implicit-extension)) (declare (ignorable __function__)) (b* ((lhs-size (lnfix lhs-size)) (x-selfsize (lnfix x-selfsize)) ((unless (> lhs-size x-selfsize)) nil) (x (vl-expr-fix x)) (ss (vl-scopestack-fix ss)) (type (vl-classify-extension-warning-hook lhs-size x-selfsize x ss)) ((unless type) nil)) (list (make-vl-warning :type type :msg "implicit extension from ~x0-bit expression to ~x1 bits: ~a2" :args (list x-selfsize lhs-size x) :fn __function__)))))
Theorem:
(defthm vl-warninglist-p-of-vl-maybe-warn-about-implicit-extension (b* ((warnings (vl-maybe-warn-about-implicit-extension lhs-size x-selfsize x ss))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-maybe-warn-about-implicit-extension (b* ((?warnings (vl-maybe-warn-about-implicit-extension lhs-size x-selfsize x ss))) (true-listp warnings)) :rule-classes :type-prescription)
Theorem:
(defthm vl-maybe-warn-about-implicit-extension-of-nfix-lhs-size (equal (vl-maybe-warn-about-implicit-extension (nfix lhs-size) x-selfsize x ss) (vl-maybe-warn-about-implicit-extension lhs-size x-selfsize x ss)))
Theorem:
(defthm vl-maybe-warn-about-implicit-extension-nat-equiv-congruence-on-lhs-size (implies (acl2::nat-equiv lhs-size lhs-size-equiv) (equal (vl-maybe-warn-about-implicit-extension lhs-size x-selfsize x ss) (vl-maybe-warn-about-implicit-extension lhs-size-equiv x-selfsize x ss))) :rule-classes :congruence)
Theorem:
(defthm vl-maybe-warn-about-implicit-extension-of-nfix-x-selfsize (equal (vl-maybe-warn-about-implicit-extension lhs-size (nfix x-selfsize) x ss) (vl-maybe-warn-about-implicit-extension lhs-size x-selfsize x ss)))
Theorem:
(defthm vl-maybe-warn-about-implicit-extension-nat-equiv-congruence-on-x-selfsize (implies (acl2::nat-equiv x-selfsize x-selfsize-equiv) (equal (vl-maybe-warn-about-implicit-extension lhs-size x-selfsize x ss) (vl-maybe-warn-about-implicit-extension lhs-size x-selfsize-equiv x ss))) :rule-classes :congruence)
Theorem:
(defthm vl-maybe-warn-about-implicit-extension-of-vl-expr-fix-x (equal (vl-maybe-warn-about-implicit-extension lhs-size x-selfsize (vl-expr-fix x) ss) (vl-maybe-warn-about-implicit-extension lhs-size x-selfsize x ss)))
Theorem:
(defthm vl-maybe-warn-about-implicit-extension-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-maybe-warn-about-implicit-extension lhs-size x-selfsize x ss) (vl-maybe-warn-about-implicit-extension lhs-size x-selfsize x-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-maybe-warn-about-implicit-extension-of-vl-scopestack-fix-ss (equal (vl-maybe-warn-about-implicit-extension lhs-size x-selfsize x (vl-scopestack-fix ss)) (vl-maybe-warn-about-implicit-extension lhs-size x-selfsize x ss)))
Theorem:
(defthm vl-maybe-warn-about-implicit-extension-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-maybe-warn-about-implicit-extension lhs-size x-selfsize x ss) (vl-maybe-warn-about-implicit-extension lhs-size x-selfsize x ss-equiv))) :rule-classes :congruence)