Create warnings for assignments that share some RHS.
(vl-maybe-warn-duperhs rhs assigns warnings) → new-warnings
Function:
(defun vl-maybe-warn-duperhs (rhs assigns warnings) (declare (xargs :guard (and (vl-expr-p rhs) (vl-assignlist-p assigns) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-maybe-warn-duperhs)) (declare (ignorable __function__)) (b* ((assigns (vl-assignlist-fix assigns)) ((when (or (atom assigns) (atom (cdr assigns)))) (ok)) ((when (vl-duperhs-too-trivial-p rhs)) (ok)) (rhs-names (vl-expr-varnames rhs)) (special-names (append (str::collect-strs-with-isubstr "ph1" rhs-names) (str::collect-strs-with-isubstr "reset" rhs-names) (str::collect-strs-with-isubstr "clear" rhs-names) (str::collect-strs-with-isubstr "enable" rhs-names) (str::collect-strs-with-isubstr "clken" rhs-names) (str::collect-strs-with-isubstr "valid" rhs-names))) ((when (consp special-names)) (ok))) (warn :type :vl-warn-same-rhs :msg "Found assignments that have exactly the same right-hand side, ~ which might indicate a copy/paste error:~%~s0" :args (list (str::prefix-lines (with-local-ps (vl-ps-update-autowrap-col 200) (vl-pp-assignlist assigns)) " ") assigns)))))
Theorem:
(defthm vl-warninglist-p-of-vl-maybe-warn-duperhs (b* ((new-warnings (vl-maybe-warn-duperhs rhs assigns warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-maybe-warn-duperhs-of-vl-expr-fix-rhs (equal (vl-maybe-warn-duperhs (vl-expr-fix rhs) assigns warnings) (vl-maybe-warn-duperhs rhs assigns warnings)))
Theorem:
(defthm vl-maybe-warn-duperhs-vl-expr-equiv-congruence-on-rhs (implies (vl-expr-equiv rhs rhs-equiv) (equal (vl-maybe-warn-duperhs rhs assigns warnings) (vl-maybe-warn-duperhs rhs-equiv assigns warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-maybe-warn-duperhs-of-vl-assignlist-fix-assigns (equal (vl-maybe-warn-duperhs rhs (vl-assignlist-fix assigns) warnings) (vl-maybe-warn-duperhs rhs assigns warnings)))
Theorem:
(defthm vl-maybe-warn-duperhs-vl-assignlist-equiv-congruence-on-assigns (implies (vl-assignlist-equiv assigns assigns-equiv) (equal (vl-maybe-warn-duperhs rhs assigns warnings) (vl-maybe-warn-duperhs rhs assigns-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-maybe-warn-duperhs-of-vl-warninglist-fix-warnings (equal (vl-maybe-warn-duperhs rhs assigns (vl-warninglist-fix warnings)) (vl-maybe-warn-duperhs rhs assigns warnings)))
Theorem:
(defthm vl-maybe-warn-duperhs-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-maybe-warn-duperhs rhs assigns warnings) (vl-maybe-warn-duperhs rhs assigns warnings-equiv))) :rule-classes :congruence)