		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucidocclist-drop-bad-modinsts

Removes occurrences from unresolved module instances.

Signature
(vl-lucidocclist-drop-bad-modinsts x) → new-x
Arguments: x — Guard (vl-lucidocclist-p x).
Returns: new-x — Type (vl-lucidocclist-p new-x).

The problem we are solving here happens when there is a buggy module instance.

Suppose a module being instanced has a parse error, or that we hit some problem resolving the arguments of the instance, for whatever reason. In this case, for lucid's usual use/set checking, the right thing to do (to suppress false positives) is to pretend each argument to the module is both used and set.

However, for multidrive warnings this is counterproductive and causes us to think inputs are driven! So, for multidrive detection, drop module instances whose arguments are not sensibly resolved.

Definitions and Theorems

Function: vl-lucidocclist-drop-bad-modinsts

(defun vl-lucidocclist-drop-bad-modinsts (x)
 (declare (xargs :guard (vl-lucidocclist-p x)))
 (let ((__function__ 'vl-lucidocclist-drop-bad-modinsts))
  (declare (ignorable __function__))
  (b* (((when (atom x)) nil)
       (elem (vl-lucidctx->elem (vl-lucidocc->ctx (car x))))
       (modinst-p (mbe :logic (vl-modinst-p elem)
                       :exec (eq (tag elem) :vl-modinst)))
       ((when (and modinst-p
                   (not (vl-lucid-modinst-nicely-resolved-p elem))))
        (vl-lucidocclist-drop-bad-modinsts (cdr x))))
    (cons (vl-lucidocc-fix (car x))
          (vl-lucidocclist-drop-bad-modinsts (cdr x))))))

Theorem: vl-lucidocclist-p-of-vl-lucidocclist-drop-bad-modinsts

(defthm vl-lucidocclist-p-of-vl-lucidocclist-drop-bad-modinsts
  (b* ((new-x (vl-lucidocclist-drop-bad-modinsts x)))
    (vl-lucidocclist-p new-x))
  :rule-classes :rewrite)

Theorem: vl-lucidocclist-drop-bad-modinsts-of-vl-lucidocclist-fix-x

(defthm vl-lucidocclist-drop-bad-modinsts-of-vl-lucidocclist-fix-x
  (equal (vl-lucidocclist-drop-bad-modinsts (vl-lucidocclist-fix x))
         (vl-lucidocclist-drop-bad-modinsts x)))

Theorem: vl-lucidocclist-drop-bad-modinsts-vl-lucidocclist-equiv-congruence-on-x

(defthm
 vl-lucidocclist-drop-bad-modinsts-vl-lucidocclist-equiv-congruence-on-x
 (implies (vl-lucidocclist-equiv x x-equiv)
          (equal (vl-lucidocclist-drop-bad-modinsts x)
                 (vl-lucidocclist-drop-bad-modinsts x-equiv)))
 :rule-classes :congruence)