Warn if the top level of x is a
(vl-expr-qmarksize-check-aux x ss) → warnings
Function:
(defun vl-expr-qmarksize-check-aux (x ss) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss)))) (let ((__function__ 'vl-expr-qmarksize-check-aux)) (declare (ignorable __function__)) (vl-expr-case x :vl-qmark (b* (((mv warnings test-size) (vl-expr-selfsize x.test ss (vl-elabscopes-init-ss ss))) ((unless test-size) warnings) ((unless (or (eql test-size 1) (vl-expr-qmarksize-test-trivial x.test ss))) (warn :type :vl-warn-qmark-width :msg "~x1-bit wide \"test\" expression for ?: operator, ~a2." :args (list nil test-size x.test)))) warnings) :otherwise nil)))
Theorem:
(defthm vl-warninglist-p-of-vl-expr-qmarksize-check-aux (b* ((warnings (vl-expr-qmarksize-check-aux x ss))) (vl-warninglist-p warnings)) :rule-classes :rewrite)