Rules for executing tests on values.
Each rule turns
Theorem:
(defthm test-value-when-scharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (scharp x)) (equal (test-value x) (boolean-from-schar x))))
Theorem:
(defthm test-value-when-ucharp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ucharp x)) (equal (test-value x) (boolean-from-uchar x))))
Theorem:
(defthm test-value-when-sshortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sshortp x)) (equal (test-value x) (boolean-from-sshort x))))
Theorem:
(defthm test-value-when-ushortp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ushortp x)) (equal (test-value x) (boolean-from-ushort x))))
Theorem:
(defthm test-value-when-sintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sintp x)) (equal (test-value x) (boolean-from-sint x))))
Theorem:
(defthm test-value-when-uintp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (uintp x)) (equal (test-value x) (boolean-from-uint x))))
Theorem:
(defthm test-value-when-slongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (slongp x)) (equal (test-value x) (boolean-from-slong x))))
Theorem:
(defthm test-value-when-ulongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ulongp x)) (equal (test-value x) (boolean-from-ulong x))))
Theorem:
(defthm test-value-when-sllongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (sllongp x)) (equal (test-value x) (boolean-from-sllong x))))
Theorem:
(defthm test-value-when-ullongp (implies (and (syntaxp (or (atom x) (not (member-eq (car x) '(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value))))) (ullongp x)) (equal (test-value x) (boolean-from-ullong x))))