Vl-expr-qmarksize-check
Look throughout an expression for any ?: expressions that have
wide tests.
- Signature
(vl-expr-qmarksize-check x ctx) → warnings
- Arguments
- x — Guard (vl-expr-p x).
- ctx — Guard (vl-context-p ctx).
- Returns
- warnings — Type (vl-warninglist-p 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 ctx)))
(vl-warninglist-p 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 ctx)))
(vl-warninglist-p warnings))
:rule-classes :rewrite)
Subtopics
- Vl-exprlist-qmarksize-check
