Vl-expr-condcheck
Look for strange conditions throughout an expression.
- Signature
(vl-expr-condcheck x tests-above ctx) → warnings
- Arguments
- x — Guard (vl-expr-p x).
- tests-above — Guard (and (vl-exprlist-p tests-above) (true-listp tests-above)).
- ctx — Guard (vl-context-p ctx).
- Returns
- warnings — Type (vl-warninglist-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 ctx)))
(vl-warninglist-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 ctx)))
(vl-warninglist-p warnings))
:rule-classes :rewrite)
Subtopics
- Vl-exprlist-condcheck
