		Search-engine friendly clone of the ACL2 documentation.

Selfassigns

Vl-assign-check-selfassigns

(vl-assign-check-selfassigns x mod ialist) checks an assignment for bits that occur on the lhs and rhs.

Signature
(vl-assign-check-selfassigns x mod ialist) → warnings
Arguments: x — Guard (vl-assign-p x).; mod — Guard (vl-module-p mod).; ialist — Guard (equal ialist (vl-make-moditem-alist mod)).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-assign-check-selfassigns

(defun vl-assign-check-selfassigns (x mod ialist)
 (declare
    (xargs :guard (and (vl-assign-p x)
                       (vl-module-p mod)
                       (equal ialist (vl-make-moditem-alist mod)))))
 (let ((__function__ 'vl-assign-check-selfassigns))
  (declare (ignorable __function__))
  (b*
   (((vl-assign x) x)
    (lhs-bits (mergesort (vl-expr-approx-bits x.lvalue mod ialist)))
    (rhs-bits (mergesort (vl-expr-approx-bits x.expr mod ialist)))
    (oops (intersect lhs-bits rhs-bits)))
   (if oops
     (list (make-vl-warning :type :vl-warn-selfassign
                            :msg "~a0: lhs bits occur on rhs: ~&1."
                            :args (list x oops)
                            :fatalp nil
                            :fn __function__))
     nil))))

Theorem: vl-warninglist-p-of-vl-assign-check-selfassigns

(defthm vl-warninglist-p-of-vl-assign-check-selfassigns
  (b* ((warnings (vl-assign-check-selfassigns x mod ialist)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)