Rules for executing assignment expressions to array subscript expressions.
Theorem:
(defthm exec-expr-asg-arrsub-when-schar-arrayp (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (equal var (expr-ident->get arr)) (not (zp limit)) (equal arr-val (read-var var compst)) (valuep arr-val) (equal eptr (apconvert-expr-value (expr-value arr-val (objdesign-of-var var compst)))) (expr-valuep eptr) (equal ptr (expr-value->value eptr)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-schar)) (equal array (read-object (value-pointer->designator ptr) compst)) (schar-arrayp array) (equal eindex (exec-expr-pure sub compst)) (expr-valuep eindex) (equal eindex1 (apconvert-expr-value eindex)) (expr-valuep eindex1) (equal index (expr-value->value eindex1)) (cintegerp index) (schar-array-index-okp array index) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (scharp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (schar-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-schar-arrayp-for-modular-proofs (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (not (zp limit)) (equal arr-eval (exec-expr-pure arr compst)) (expr-valuep arr-eval) (equal ptr-eval (apconvert-expr-value arr-eval)) (expr-valuep ptr-eval) (equal ptr (expr-value->value ptr-eval)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-schar)) (equal array (read-object (value-pointer->designator ptr) compst)) (schar-arrayp array) (equal sub-eval (exec-expr-pure sub compst)) (expr-valuep sub-eval) (equal index-eval (apconvert-expr-value sub-eval)) (expr-valuep index-eval) (equal index (expr-value->value index-eval)) (cintegerp index) (schar-array-index-okp array index) (equal right-eval (exec-expr-pure right compst)) (expr-valuep right-eval) (equal eval (apconvert-expr-value right-eval)) (expr-valuep eval) (equal val (expr-value->value eval)) (scharp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (schar-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-uchar-arrayp (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (equal var (expr-ident->get arr)) (not (zp limit)) (equal arr-val (read-var var compst)) (valuep arr-val) (equal eptr (apconvert-expr-value (expr-value arr-val (objdesign-of-var var compst)))) (expr-valuep eptr) (equal ptr (expr-value->value eptr)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-uchar)) (equal array (read-object (value-pointer->designator ptr) compst)) (uchar-arrayp array) (equal eindex (exec-expr-pure sub compst)) (expr-valuep eindex) (equal eindex1 (apconvert-expr-value eindex)) (expr-valuep eindex1) (equal index (expr-value->value eindex1)) (cintegerp index) (uchar-array-index-okp array index) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (ucharp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (uchar-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-uchar-arrayp-for-modular-proofs (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (not (zp limit)) (equal arr-eval (exec-expr-pure arr compst)) (expr-valuep arr-eval) (equal ptr-eval (apconvert-expr-value arr-eval)) (expr-valuep ptr-eval) (equal ptr (expr-value->value ptr-eval)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-uchar)) (equal array (read-object (value-pointer->designator ptr) compst)) (uchar-arrayp array) (equal sub-eval (exec-expr-pure sub compst)) (expr-valuep sub-eval) (equal index-eval (apconvert-expr-value sub-eval)) (expr-valuep index-eval) (equal index (expr-value->value index-eval)) (cintegerp index) (uchar-array-index-okp array index) (equal right-eval (exec-expr-pure right compst)) (expr-valuep right-eval) (equal eval (apconvert-expr-value right-eval)) (expr-valuep eval) (equal val (expr-value->value eval)) (ucharp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (uchar-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-sshort-arrayp (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (equal var (expr-ident->get arr)) (not (zp limit)) (equal arr-val (read-var var compst)) (valuep arr-val) (equal eptr (apconvert-expr-value (expr-value arr-val (objdesign-of-var var compst)))) (expr-valuep eptr) (equal ptr (expr-value->value eptr)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-sshort)) (equal array (read-object (value-pointer->designator ptr) compst)) (sshort-arrayp array) (equal eindex (exec-expr-pure sub compst)) (expr-valuep eindex) (equal eindex1 (apconvert-expr-value eindex)) (expr-valuep eindex1) (equal index (expr-value->value eindex1)) (cintegerp index) (sshort-array-index-okp array index) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (sshortp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (sshort-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-sshort-arrayp-for-modular-proofs (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (not (zp limit)) (equal arr-eval (exec-expr-pure arr compst)) (expr-valuep arr-eval) (equal ptr-eval (apconvert-expr-value arr-eval)) (expr-valuep ptr-eval) (equal ptr (expr-value->value ptr-eval)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-sshort)) (equal array (read-object (value-pointer->designator ptr) compst)) (sshort-arrayp array) (equal sub-eval (exec-expr-pure sub compst)) (expr-valuep sub-eval) (equal index-eval (apconvert-expr-value sub-eval)) (expr-valuep index-eval) (equal index (expr-value->value index-eval)) (cintegerp index) (sshort-array-index-okp array index) (equal right-eval (exec-expr-pure right compst)) (expr-valuep right-eval) (equal eval (apconvert-expr-value right-eval)) (expr-valuep eval) (equal val (expr-value->value eval)) (sshortp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (sshort-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-ushort-arrayp (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (equal var (expr-ident->get arr)) (not (zp limit)) (equal arr-val (read-var var compst)) (valuep arr-val) (equal eptr (apconvert-expr-value (expr-value arr-val (objdesign-of-var var compst)))) (expr-valuep eptr) (equal ptr (expr-value->value eptr)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-ushort)) (equal array (read-object (value-pointer->designator ptr) compst)) (ushort-arrayp array) (equal eindex (exec-expr-pure sub compst)) (expr-valuep eindex) (equal eindex1 (apconvert-expr-value eindex)) (expr-valuep eindex1) (equal index (expr-value->value eindex1)) (cintegerp index) (ushort-array-index-okp array index) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (ushortp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (ushort-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-ushort-arrayp-for-modular-proofs (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (not (zp limit)) (equal arr-eval (exec-expr-pure arr compst)) (expr-valuep arr-eval) (equal ptr-eval (apconvert-expr-value arr-eval)) (expr-valuep ptr-eval) (equal ptr (expr-value->value ptr-eval)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-ushort)) (equal array (read-object (value-pointer->designator ptr) compst)) (ushort-arrayp array) (equal sub-eval (exec-expr-pure sub compst)) (expr-valuep sub-eval) (equal index-eval (apconvert-expr-value sub-eval)) (expr-valuep index-eval) (equal index (expr-value->value index-eval)) (cintegerp index) (ushort-array-index-okp array index) (equal right-eval (exec-expr-pure right compst)) (expr-valuep right-eval) (equal eval (apconvert-expr-value right-eval)) (expr-valuep eval) (equal val (expr-value->value eval)) (ushortp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (ushort-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-sint-arrayp (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (equal var (expr-ident->get arr)) (not (zp limit)) (equal arr-val (read-var var compst)) (valuep arr-val) (equal eptr (apconvert-expr-value (expr-value arr-val (objdesign-of-var var compst)))) (expr-valuep eptr) (equal ptr (expr-value->value eptr)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-sint)) (equal array (read-object (value-pointer->designator ptr) compst)) (sint-arrayp array) (equal eindex (exec-expr-pure sub compst)) (expr-valuep eindex) (equal eindex1 (apconvert-expr-value eindex)) (expr-valuep eindex1) (equal index (expr-value->value eindex1)) (cintegerp index) (sint-array-index-okp array index) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (sintp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (sint-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-sint-arrayp-for-modular-proofs (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (not (zp limit)) (equal arr-eval (exec-expr-pure arr compst)) (expr-valuep arr-eval) (equal ptr-eval (apconvert-expr-value arr-eval)) (expr-valuep ptr-eval) (equal ptr (expr-value->value ptr-eval)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-sint)) (equal array (read-object (value-pointer->designator ptr) compst)) (sint-arrayp array) (equal sub-eval (exec-expr-pure sub compst)) (expr-valuep sub-eval) (equal index-eval (apconvert-expr-value sub-eval)) (expr-valuep index-eval) (equal index (expr-value->value index-eval)) (cintegerp index) (sint-array-index-okp array index) (equal right-eval (exec-expr-pure right compst)) (expr-valuep right-eval) (equal eval (apconvert-expr-value right-eval)) (expr-valuep eval) (equal val (expr-value->value eval)) (sintp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (sint-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-uint-arrayp (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (equal var (expr-ident->get arr)) (not (zp limit)) (equal arr-val (read-var var compst)) (valuep arr-val) (equal eptr (apconvert-expr-value (expr-value arr-val (objdesign-of-var var compst)))) (expr-valuep eptr) (equal ptr (expr-value->value eptr)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-uint)) (equal array (read-object (value-pointer->designator ptr) compst)) (uint-arrayp array) (equal eindex (exec-expr-pure sub compst)) (expr-valuep eindex) (equal eindex1 (apconvert-expr-value eindex)) (expr-valuep eindex1) (equal index (expr-value->value eindex1)) (cintegerp index) (uint-array-index-okp array index) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (uintp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (uint-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-uint-arrayp-for-modular-proofs (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (not (zp limit)) (equal arr-eval (exec-expr-pure arr compst)) (expr-valuep arr-eval) (equal ptr-eval (apconvert-expr-value arr-eval)) (expr-valuep ptr-eval) (equal ptr (expr-value->value ptr-eval)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-uint)) (equal array (read-object (value-pointer->designator ptr) compst)) (uint-arrayp array) (equal sub-eval (exec-expr-pure sub compst)) (expr-valuep sub-eval) (equal index-eval (apconvert-expr-value sub-eval)) (expr-valuep index-eval) (equal index (expr-value->value index-eval)) (cintegerp index) (uint-array-index-okp array index) (equal right-eval (exec-expr-pure right compst)) (expr-valuep right-eval) (equal eval (apconvert-expr-value right-eval)) (expr-valuep eval) (equal val (expr-value->value eval)) (uintp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (uint-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-slong-arrayp (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (equal var (expr-ident->get arr)) (not (zp limit)) (equal arr-val (read-var var compst)) (valuep arr-val) (equal eptr (apconvert-expr-value (expr-value arr-val (objdesign-of-var var compst)))) (expr-valuep eptr) (equal ptr (expr-value->value eptr)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-slong)) (equal array (read-object (value-pointer->designator ptr) compst)) (slong-arrayp array) (equal eindex (exec-expr-pure sub compst)) (expr-valuep eindex) (equal eindex1 (apconvert-expr-value eindex)) (expr-valuep eindex1) (equal index (expr-value->value eindex1)) (cintegerp index) (slong-array-index-okp array index) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (slongp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (slong-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-slong-arrayp-for-modular-proofs (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (not (zp limit)) (equal arr-eval (exec-expr-pure arr compst)) (expr-valuep arr-eval) (equal ptr-eval (apconvert-expr-value arr-eval)) (expr-valuep ptr-eval) (equal ptr (expr-value->value ptr-eval)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-slong)) (equal array (read-object (value-pointer->designator ptr) compst)) (slong-arrayp array) (equal sub-eval (exec-expr-pure sub compst)) (expr-valuep sub-eval) (equal index-eval (apconvert-expr-value sub-eval)) (expr-valuep index-eval) (equal index (expr-value->value index-eval)) (cintegerp index) (slong-array-index-okp array index) (equal right-eval (exec-expr-pure right compst)) (expr-valuep right-eval) (equal eval (apconvert-expr-value right-eval)) (expr-valuep eval) (equal val (expr-value->value eval)) (slongp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (slong-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-ulong-arrayp (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (equal var (expr-ident->get arr)) (not (zp limit)) (equal arr-val (read-var var compst)) (valuep arr-val) (equal eptr (apconvert-expr-value (expr-value arr-val (objdesign-of-var var compst)))) (expr-valuep eptr) (equal ptr (expr-value->value eptr)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-ulong)) (equal array (read-object (value-pointer->designator ptr) compst)) (ulong-arrayp array) (equal eindex (exec-expr-pure sub compst)) (expr-valuep eindex) (equal eindex1 (apconvert-expr-value eindex)) (expr-valuep eindex1) (equal index (expr-value->value eindex1)) (cintegerp index) (ulong-array-index-okp array index) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (ulongp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (ulong-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-ulong-arrayp-for-modular-proofs (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (not (zp limit)) (equal arr-eval (exec-expr-pure arr compst)) (expr-valuep arr-eval) (equal ptr-eval (apconvert-expr-value arr-eval)) (expr-valuep ptr-eval) (equal ptr (expr-value->value ptr-eval)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-ulong)) (equal array (read-object (value-pointer->designator ptr) compst)) (ulong-arrayp array) (equal sub-eval (exec-expr-pure sub compst)) (expr-valuep sub-eval) (equal index-eval (apconvert-expr-value sub-eval)) (expr-valuep index-eval) (equal index (expr-value->value index-eval)) (cintegerp index) (ulong-array-index-okp array index) (equal right-eval (exec-expr-pure right compst)) (expr-valuep right-eval) (equal eval (apconvert-expr-value right-eval)) (expr-valuep eval) (equal val (expr-value->value eval)) (ulongp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (ulong-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-sllong-arrayp (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (equal var (expr-ident->get arr)) (not (zp limit)) (equal arr-val (read-var var compst)) (valuep arr-val) (equal eptr (apconvert-expr-value (expr-value arr-val (objdesign-of-var var compst)))) (expr-valuep eptr) (equal ptr (expr-value->value eptr)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-sllong)) (equal array (read-object (value-pointer->designator ptr) compst)) (sllong-arrayp array) (equal eindex (exec-expr-pure sub compst)) (expr-valuep eindex) (equal eindex1 (apconvert-expr-value eindex)) (expr-valuep eindex1) (equal index (expr-value->value eindex1)) (cintegerp index) (sllong-array-index-okp array index) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (sllongp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (sllong-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-sllong-arrayp-for-modular-proofs (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (not (zp limit)) (equal arr-eval (exec-expr-pure arr compst)) (expr-valuep arr-eval) (equal ptr-eval (apconvert-expr-value arr-eval)) (expr-valuep ptr-eval) (equal ptr (expr-value->value ptr-eval)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-sllong)) (equal array (read-object (value-pointer->designator ptr) compst)) (sllong-arrayp array) (equal sub-eval (exec-expr-pure sub compst)) (expr-valuep sub-eval) (equal index-eval (apconvert-expr-value sub-eval)) (expr-valuep index-eval) (equal index (expr-value->value index-eval)) (cintegerp index) (sllong-array-index-okp array index) (equal right-eval (exec-expr-pure right compst)) (expr-valuep right-eval) (equal eval (apconvert-expr-value right-eval)) (expr-valuep eval) (equal val (expr-value->value eval)) (sllongp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (sllong-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-ullong-arrayp (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (equal var (expr-ident->get arr)) (not (zp limit)) (equal arr-val (read-var var compst)) (valuep arr-val) (equal eptr (apconvert-expr-value (expr-value arr-val (objdesign-of-var var compst)))) (expr-valuep eptr) (equal ptr (expr-value->value eptr)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-ullong)) (equal array (read-object (value-pointer->designator ptr) compst)) (ullong-arrayp array) (equal eindex (exec-expr-pure sub compst)) (expr-valuep eindex) (equal eindex1 (apconvert-expr-value eindex)) (expr-valuep eindex1) (equal index (expr-value->value eindex1)) (cintegerp index) (ullong-array-index-okp array index) (equal eval (exec-expr-pure right compst)) (expr-valuep eval) (equal eval1 (apconvert-expr-value eval)) (expr-valuep eval1) (equal val (expr-value->value eval1)) (ullongp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (ullong-array-write array index val) compst))))
Theorem:
(defthm exec-expr-asg-arrsub-when-ullong-arrayp-for-modular-proofs (implies (and (equal (expr-kind e) :binary) (equal (binop-kind (expr-binary->op e)) :asg) (equal left (expr-binary->arg1 e)) (equal right (expr-binary->arg2 e)) (equal (expr-kind left) :arrsub) (equal arr (expr-arrsub->arr left)) (equal sub (expr-arrsub->sub left)) (equal (expr-kind arr) :ident) (not (zp limit)) (equal arr-eval (exec-expr-pure arr compst)) (expr-valuep arr-eval) (equal ptr-eval (apconvert-expr-value arr-eval)) (expr-valuep ptr-eval) (equal ptr (expr-value->value ptr-eval)) (value-case ptr :pointer) (value-pointer-validp ptr) (equal (value-pointer->reftype ptr) (type-ullong)) (equal array (read-object (value-pointer->designator ptr) compst)) (ullong-arrayp array) (equal sub-eval (exec-expr-pure sub compst)) (expr-valuep sub-eval) (equal index-eval (apconvert-expr-value sub-eval)) (expr-valuep index-eval) (equal index (expr-value->value index-eval)) (cintegerp index) (ullong-array-index-okp array index) (equal right-eval (exec-expr-pure right compst)) (expr-valuep right-eval) (equal eval (apconvert-expr-value right-eval)) (expr-valuep eval) (equal val (expr-value->value eval)) (ullongp val)) (equal (exec-expr-asg e compst fenv limit) (write-object (value-pointer->designator ptr) (ullong-array-write array index val) compst))))