		Search-engine friendly clone of the ACL2 documentation.

Duperhs-check

Vl-maybe-warn-duperhs

Create warnings for assignments that share some RHS.

Signature
(vl-maybe-warn-duperhs rhs assigns warnings) → new-warnings
Arguments: rhs — The shared RHS among all these assignments.
Guard (vl-expr-p rhs).; assigns — A list of assignments that share this RHS.
Guard (vl-assignlist-p assigns).; warnings — A warnings accumulator to extend.
Guard (vl-warninglist-p warnings).
Returns: new-warnings — Type (vl-warninglist-p new-warnings).

Definitions and Theorems

Function: vl-maybe-warn-duperhs

(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*
   (((when (or (atom assigns)
               (atom (cdr assigns))))
     (ok))
    ((when (vl-duperhs-too-trivial-p rhs))
     (ok))
    (rhs-names (vl-expr-names 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: vl-warninglist-p-of-vl-maybe-warn-duperhs

(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)