		Search-engine friendly clone of the ACL2 documentation.

Oddexpr-check

Vl-oddexpr-check

Signature
(vl-oddexpr-check x ctx ss) → warnings
Arguments: x — Guard (vl-expr-p x).; ctx — Guard (vl-context-p ctx).; ss — Guard (vl-scopestack-p ss).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-oddexpr-check

(defun vl-oddexpr-check (x ctx ss)
 (declare (xargs :guard (and (vl-expr-p x)
                             (vl-context-p ctx)
                             (vl-scopestack-p ss))))
 (let ((__function__ 'vl-oddexpr-check))
  (declare (ignorable __function__))
  (b* ((details (append (vl-warn-odd-binary-expression x ss)))
       ((unless details) nil))
   (list
    (make-vl-warning
     :type :vl-warn-oddexpr
     :msg
     (cat
      "~a0: found ~s1 that suggest precedence problems may be ~
                      present.  Maybe add explicit parens?  Details:~%"
      (with-local-ps (vl-pp-oddexpr-details details)))
     :args (list ctx
                 (if (vl-plural-p details)
                     "subexpressions"
                   "a subexpression")))))))

Theorem: vl-warninglist-p-of-vl-oddexpr-check

(defthm vl-warninglist-p-of-vl-oddexpr-check
  (b* ((warnings (vl-oddexpr-check x ctx ss)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)