		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-test-failures-field

Generate the Java field that keeps track of failures in the test Java class.

Signature
(atj-gen-test-failures-field) → field
Returns: field — Type (jfieldp field).

This is a private static boolean field that is initially false, and gets set if and when any test fails (see below).

This is generated only if the :tests input is not nil.

Definitions and Theorems

Function: atj-gen-test-failures-field

(defun atj-gen-test-failures-field nil
  (declare (xargs :guard t))
  (let ((__function__ 'atj-gen-test-failures-field))
    (declare (ignorable __function__))
    (make-jfield :access (jaccess-private)
                 :static? t
                 :final? nil
                 :transient? nil
                 :volatile? nil
                 :type (jtype-boolean)
                 :name "failures"
                 :init? (jexpr-literal-false))))

Theorem: jfieldp-of-atj-gen-test-failures-field

(defthm jfieldp-of-atj-gen-test-failures-field
  (b* ((field (atj-gen-test-failures-field)))
    (jfieldp field))
  :rule-classes :rewrite)