		Search-engine friendly clone of the ACL2 documentation.

Selfassigns

Vl-module-check-selfassigns

Check the assignments of a module for self-assignments to bits.

Signature
(vl-module-check-selfassigns x) → new-x
Arguments: x — Guard (vl-module-p x).
Returns: new-x — Type (vl-module-p new-x), given the guard.

(vl-module-check-selfassigns x) checks all of the assignments in the module x for selfassigns, and adds any warnings to the module.

Definitions and Theorems

Function: vl-module-check-selfassigns

(defun vl-module-check-selfassigns (x)
 (declare (xargs :guard (vl-module-p x)))
 (let ((__function__ 'vl-module-check-selfassigns))
  (declare (ignorable __function__))
  (b* ((assigns (vl-module->assigns x))
       ((unless assigns) x)
       (ialist (vl-make-moditem-alist x))
       (warnings (vl-assignlist-check-selfassigns assigns x ialist))
       (- (fast-alist-free ialist))
       ((unless warnings) x))
    (change-vl-module
         x
         :warnings (append warnings (vl-module->warnings x))))))

Theorem: vl-module-p-of-vl-module-check-selfassigns

(defthm vl-module-p-of-vl-module-check-selfassigns
  (implies (and (force (vl-module-p x)))
           (b* ((new-x (vl-module-check-selfassigns x)))
             (vl-module-p new-x)))
  :rule-classes :rewrite)