Vl-expr-qmarksize-check
Look throughout an expression for any ?: expressions that have
wide tests.
- Signature
(vl-expr-qmarksize-check x ss) → warnings
- Arguments
- x — Guard (vl-expr-p x).
- ss — Guard (vl-scopestack-p ss).
- Returns
- warnings — Type (and (vl-warninglist-p warnings) (true-listp warnings)).
We look through the expression x for any ?:
sub-expressions with wide tests, and produce a warning whenever we find one.
The ctx is a vl-context-p that says where x occurs, and is
just used to generate more meaningful error messages.
Theorem: return-type-of-vl-expr-qmarksize-check.warnings
(defthm return-type-of-vl-expr-qmarksize-check.warnings
(b* ((?warnings (vl-expr-qmarksize-check x ss)))
(and (vl-warninglist-p warnings)
(true-listp warnings)))
:rule-classes :rewrite)
Theorem: return-type-of-vl-exprlist-qmarksize-check.warnings
(defthm return-type-of-vl-exprlist-qmarksize-check.warnings
(b* ((?warnings (vl-exprlist-qmarksize-check x ss)))
(vl-warninglist-p warnings))
:rule-classes :rewrite)
Subtopics
- Vl-exprlist-qmarksize-check