Rules for executing array subscript expressions.
Theorem:
(defthm exec-arrsub-when-schar-arrayp (implies (and (equal ex (apconvert-expr-value (expr-value x objdes-x))) (expr-valuep ex) (equal a (expr-value->value ex)) (value-case a :pointer) (value-pointer-validp a) (equal (value-pointer->reftype a) (type-schar)) (equal objdes (value-pointer->designator a)) (equal array (read-object objdes compst)) (schar-arrayp array) (cintegerp y) (schar-array-index-okp array y)) (equal (exec-arrsub (expr-value x objdes-x) (expr-value y objdes-y) compst) (expr-value (schar-array-read array y) (objdesign-element objdes (integer-from-cinteger y))))))
Theorem:
(defthm exec-arrsub-when-uchar-arrayp (implies (and (equal ex (apconvert-expr-value (expr-value x objdes-x))) (expr-valuep ex) (equal a (expr-value->value ex)) (value-case a :pointer) (value-pointer-validp a) (equal (value-pointer->reftype a) (type-uchar)) (equal objdes (value-pointer->designator a)) (equal array (read-object objdes compst)) (uchar-arrayp array) (cintegerp y) (uchar-array-index-okp array y)) (equal (exec-arrsub (expr-value x objdes-x) (expr-value y objdes-y) compst) (expr-value (uchar-array-read array y) (objdesign-element objdes (integer-from-cinteger y))))))
Theorem:
(defthm exec-arrsub-when-sshort-arrayp (implies (and (equal ex (apconvert-expr-value (expr-value x objdes-x))) (expr-valuep ex) (equal a (expr-value->value ex)) (value-case a :pointer) (value-pointer-validp a) (equal (value-pointer->reftype a) (type-sshort)) (equal objdes (value-pointer->designator a)) (equal array (read-object objdes compst)) (sshort-arrayp array) (cintegerp y) (sshort-array-index-okp array y)) (equal (exec-arrsub (expr-value x objdes-x) (expr-value y objdes-y) compst) (expr-value (sshort-array-read array y) (objdesign-element objdes (integer-from-cinteger y))))))
Theorem:
(defthm exec-arrsub-when-ushort-arrayp (implies (and (equal ex (apconvert-expr-value (expr-value x objdes-x))) (expr-valuep ex) (equal a (expr-value->value ex)) (value-case a :pointer) (value-pointer-validp a) (equal (value-pointer->reftype a) (type-ushort)) (equal objdes (value-pointer->designator a)) (equal array (read-object objdes compst)) (ushort-arrayp array) (cintegerp y) (ushort-array-index-okp array y)) (equal (exec-arrsub (expr-value x objdes-x) (expr-value y objdes-y) compst) (expr-value (ushort-array-read array y) (objdesign-element objdes (integer-from-cinteger y))))))
Theorem:
(defthm exec-arrsub-when-sint-arrayp (implies (and (equal ex (apconvert-expr-value (expr-value x objdes-x))) (expr-valuep ex) (equal a (expr-value->value ex)) (value-case a :pointer) (value-pointer-validp a) (equal (value-pointer->reftype a) (type-sint)) (equal objdes (value-pointer->designator a)) (equal array (read-object objdes compst)) (sint-arrayp array) (cintegerp y) (sint-array-index-okp array y)) (equal (exec-arrsub (expr-value x objdes-x) (expr-value y objdes-y) compst) (expr-value (sint-array-read array y) (objdesign-element objdes (integer-from-cinteger y))))))
Theorem:
(defthm exec-arrsub-when-uint-arrayp (implies (and (equal ex (apconvert-expr-value (expr-value x objdes-x))) (expr-valuep ex) (equal a (expr-value->value ex)) (value-case a :pointer) (value-pointer-validp a) (equal (value-pointer->reftype a) (type-uint)) (equal objdes (value-pointer->designator a)) (equal array (read-object objdes compst)) (uint-arrayp array) (cintegerp y) (uint-array-index-okp array y)) (equal (exec-arrsub (expr-value x objdes-x) (expr-value y objdes-y) compst) (expr-value (uint-array-read array y) (objdesign-element objdes (integer-from-cinteger y))))))
Theorem:
(defthm exec-arrsub-when-slong-arrayp (implies (and (equal ex (apconvert-expr-value (expr-value x objdes-x))) (expr-valuep ex) (equal a (expr-value->value ex)) (value-case a :pointer) (value-pointer-validp a) (equal (value-pointer->reftype a) (type-slong)) (equal objdes (value-pointer->designator a)) (equal array (read-object objdes compst)) (slong-arrayp array) (cintegerp y) (slong-array-index-okp array y)) (equal (exec-arrsub (expr-value x objdes-x) (expr-value y objdes-y) compst) (expr-value (slong-array-read array y) (objdesign-element objdes (integer-from-cinteger y))))))
Theorem:
(defthm exec-arrsub-when-ulong-arrayp (implies (and (equal ex (apconvert-expr-value (expr-value x objdes-x))) (expr-valuep ex) (equal a (expr-value->value ex)) (value-case a :pointer) (value-pointer-validp a) (equal (value-pointer->reftype a) (type-ulong)) (equal objdes (value-pointer->designator a)) (equal array (read-object objdes compst)) (ulong-arrayp array) (cintegerp y) (ulong-array-index-okp array y)) (equal (exec-arrsub (expr-value x objdes-x) (expr-value y objdes-y) compst) (expr-value (ulong-array-read array y) (objdesign-element objdes (integer-from-cinteger y))))))
Theorem:
(defthm exec-arrsub-when-sllong-arrayp (implies (and (equal ex (apconvert-expr-value (expr-value x objdes-x))) (expr-valuep ex) (equal a (expr-value->value ex)) (value-case a :pointer) (value-pointer-validp a) (equal (value-pointer->reftype a) (type-sllong)) (equal objdes (value-pointer->designator a)) (equal array (read-object objdes compst)) (sllong-arrayp array) (cintegerp y) (sllong-array-index-okp array y)) (equal (exec-arrsub (expr-value x objdes-x) (expr-value y objdes-y) compst) (expr-value (sllong-array-read array y) (objdesign-element objdes (integer-from-cinteger y))))))
Theorem:
(defthm exec-arrsub-when-ullong-arrayp (implies (and (equal ex (apconvert-expr-value (expr-value x objdes-x))) (expr-valuep ex) (equal a (expr-value->value ex)) (value-case a :pointer) (value-pointer-validp a) (equal (value-pointer->reftype a) (type-ullong)) (equal objdes (value-pointer->designator a)) (equal array (read-object objdes compst)) (ullong-arrayp array) (cintegerp y) (ullong-array-index-okp array y)) (equal (exec-arrsub (expr-value x objdes-x) (expr-value y objdes-y) compst) (expr-value (ullong-array-read array y) (objdesign-element objdes (integer-from-cinteger y))))))