		Search-engine friendly clone of the ACL2 documentation.

Condcheck

Vl-iftest-condcheck

Signature
(vl-iftest-condcheck x tests-above ctx ifstmtp) → warnings
Arguments: x — The test of the IF statement or ?: operator.
Guard (vl-expr-p x).; tests-above — Guard (vl-exprlist-p tests-above).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-iftest-condcheck

(defun vl-iftest-condcheck (x tests-above ctx ifstmtp)
 (declare (xargs :guard (and (vl-expr-p x)
                             (vl-exprlist-p tests-above))))
 (let ((__function__ 'vl-iftest-condcheck))
  (declare (ignorable __function__))
  (b* ((x (vl-expr-fix x))
       (tests-above (vl-exprlist-fix tests-above))
       (test-fix (vl-condcheck-fix x))
       (~test-fix (vl-condcheck-negate test-fix))
       (warning-descrip (if ifstmtp "an IF statement"
                          "a ?: operator")))
   (cond
    ((vl-expr-case x :vl-literal)
     (list
      (make-vl-warning
       :type
       (if ifstmtp :vl-warn-ifstmt-const
         :vl-warn-qmark-const)
       :msg
       "found ~s3 with constant ~
                                expression ~a1 as its test: ~a2.~%"
       :args (list ctx x x warning-descrip)
       :fatalp nil
       :fn __function__)))
    ((member-equal test-fix tests-above)
     (list
      (make-vl-warning
       :type
       (if ifstmtp :vl-warn-ifstmt-always-true
         :vl-warn-qmark-always-true)
       :msg
       "found ~s3 that is considering ~
                                whether ~a1 holds, but an equivalent case was ~
                                considered above, so this will always be ~
                                true. The sub-expression is ~a2."
       :args (list ctx x x warning-descrip)
       :fatalp nil
       :fn __function__)))
    ((member-equal ~test-fix tests-above)
     (list
      (make-vl-warning
       :type
       (if ifstmtp :vl-warn-ifstmt-always-false
         :vl-warn-qmark-always-false)
       :msg
       "found ~s3 that is considering ~
                                whether ~a1 holds, but an equivalent case was ~
                                considered above, so this will always be ~
                                false. The sub-expression is ~a2."
       :args (list ctx x x warning-descrip)
       :fatalp nil
       :fn __function__)))
    (t nil)))))

Theorem: vl-warninglist-p-of-vl-iftest-condcheck

(defthm vl-warninglist-p-of-vl-iftest-condcheck
  (b* ((warnings (vl-iftest-condcheck x tests-above ctx ifstmtp)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-iftest-condcheck-of-vl-expr-fix-x

(defthm vl-iftest-condcheck-of-vl-expr-fix-x
  (equal (vl-iftest-condcheck (vl-expr-fix x)
                              tests-above ctx ifstmtp)
         (vl-iftest-condcheck x tests-above ctx ifstmtp)))

Theorem: vl-iftest-condcheck-vl-expr-equiv-congruence-on-x

(defthm vl-iftest-condcheck-vl-expr-equiv-congruence-on-x
 (implies
      (vl-expr-equiv x x-equiv)
      (equal (vl-iftest-condcheck x tests-above ctx ifstmtp)
             (vl-iftest-condcheck x-equiv tests-above ctx ifstmtp)))
 :rule-classes :congruence)

Theorem: vl-iftest-condcheck-of-vl-exprlist-fix-tests-above

(defthm vl-iftest-condcheck-of-vl-exprlist-fix-tests-above
  (equal (vl-iftest-condcheck x (vl-exprlist-fix tests-above)
                              ctx ifstmtp)
         (vl-iftest-condcheck x tests-above ctx ifstmtp)))

Theorem: vl-iftest-condcheck-vl-exprlist-equiv-congruence-on-tests-above

(defthm
    vl-iftest-condcheck-vl-exprlist-equiv-congruence-on-tests-above
 (implies
      (vl-exprlist-equiv tests-above tests-above-equiv)
      (equal (vl-iftest-condcheck x tests-above ctx ifstmtp)
             (vl-iftest-condcheck x tests-above-equiv ctx ifstmtp)))
 :rule-classes :congruence)