		Search-engine friendly clone of the ACL2 documentation.

Condcheck

Vl-expr-condcheck

Look for strange conditions throughout an expression.

Signature
(vl-expr-condcheck x tests-above) → warnings
Arguments: x — Guard (vl-expr-p x).; tests-above — Guard (vl-exprlist-p tests-above).
Returns: warnings — Type (vl-warningtree-p warnings).

We recursively look throughout x for problematic tests.

The tests-above are all the tests we have seen as we have descended through expressions of the form

test ? then : else

Except:

all of the tests-above have been fixed with vl-condcheck-fix, and
when we descend into the else branch, we add ~test to tests-above; more precisely, we use vl-condcheck-negate to form this term.

The basic idea is that tests-above acts as a list of things we can assume must be true as we are seeing X.

ctx is a vl-context-p that should explain where this expression occurs, and is used in any warning messages we produce.

Theorem: return-type-of-vl-expr-condcheck.warnings

(defthm return-type-of-vl-expr-condcheck.warnings
  (b* ((?warnings (vl-expr-condcheck x tests-above)))
    (vl-warningtree-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-exprlist-condcheck.warnings

(defthm return-type-of-vl-exprlist-condcheck.warnings
  (b* ((?warnings (vl-exprlist-condcheck x tests-above)))
    (vl-warningtree-p warnings))
  :rule-classes :rewrite)

Theorem: vl-expr-condcheck-of-vl-expr-fix-x

(defthm vl-expr-condcheck-of-vl-expr-fix-x
  (equal (vl-expr-condcheck (vl-expr-fix x)
                            tests-above)
         (vl-expr-condcheck x tests-above)))

Theorem: vl-expr-condcheck-of-vl-exprlist-fix-tests-above

(defthm vl-expr-condcheck-of-vl-exprlist-fix-tests-above
  (equal (vl-expr-condcheck x (vl-exprlist-fix tests-above))
         (vl-expr-condcheck x tests-above)))

Theorem: vl-exprlist-condcheck-of-vl-exprlist-fix-x

(defthm vl-exprlist-condcheck-of-vl-exprlist-fix-x
  (equal (vl-exprlist-condcheck (vl-exprlist-fix x)
                                tests-above)
         (vl-exprlist-condcheck x tests-above)))

Theorem: vl-exprlist-condcheck-of-vl-exprlist-fix-tests-above

(defthm vl-exprlist-condcheck-of-vl-exprlist-fix-tests-above
  (equal (vl-exprlist-condcheck x (vl-exprlist-fix tests-above))
         (vl-exprlist-condcheck x tests-above)))

Theorem: vl-expr-condcheck-vl-expr-equiv-congruence-on-x

(defthm vl-expr-condcheck-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-expr-condcheck x tests-above)
                  (vl-expr-condcheck x-equiv tests-above)))
  :rule-classes :congruence)

Theorem: vl-expr-condcheck-vl-exprlist-equiv-congruence-on-tests-above

(defthm
      vl-expr-condcheck-vl-exprlist-equiv-congruence-on-tests-above
  (implies (vl-exprlist-equiv tests-above tests-above-equiv)
           (equal (vl-expr-condcheck x tests-above)
                  (vl-expr-condcheck x tests-above-equiv)))
  :rule-classes :congruence)

Theorem: vl-exprlist-condcheck-vl-exprlist-equiv-congruence-on-x

(defthm vl-exprlist-condcheck-vl-exprlist-equiv-congruence-on-x
  (implies (vl-exprlist-equiv x x-equiv)
           (equal (vl-exprlist-condcheck x tests-above)
                  (vl-exprlist-condcheck x-equiv tests-above)))
  :rule-classes :congruence)

Theorem: vl-exprlist-condcheck-vl-exprlist-equiv-congruence-on-tests-above

(defthm
  vl-exprlist-condcheck-vl-exprlist-equiv-congruence-on-tests-above
  (implies (vl-exprlist-equiv tests-above tests-above-equiv)
           (equal (vl-exprlist-condcheck x tests-above)
                  (vl-exprlist-condcheck x tests-above-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-exprlist-condcheck