Rules about apconvert-expr-value.
These leave most expression values unchanged, but they convert integer arrays with object designators to pointers.
Theorem:
(defthm apconvert-expr-value-when-not-value-array (implies (not (value-case x :array)) (equal (apconvert-expr-value (expr-value x objdes)) (expr-value x objdes))))
Theorem:
(defthm apconvert-expr-value-when-uchar-arrayp (implies (and (uchar-arrayp x) (objdesignp objdes)) (equal (apconvert-expr-value (expr-value x objdes)) (expr-value (value-pointer (pointer-valid objdes) (type-uchar)) nil))))
Theorem:
(defthm apconvert-expr-value-when-schar-arrayp (implies (and (schar-arrayp x) (objdesignp objdes)) (equal (apconvert-expr-value (expr-value x objdes)) (expr-value (value-pointer (pointer-valid objdes) (type-schar)) nil))))
Theorem:
(defthm apconvert-expr-value-when-ushort-arrayp (implies (and (ushort-arrayp x) (objdesignp objdes)) (equal (apconvert-expr-value (expr-value x objdes)) (expr-value (value-pointer (pointer-valid objdes) (type-ushort)) nil))))
Theorem:
(defthm apconvert-expr-value-when-sshort-arrayp (implies (and (sshort-arrayp x) (objdesignp objdes)) (equal (apconvert-expr-value (expr-value x objdes)) (expr-value (value-pointer (pointer-valid objdes) (type-sshort)) nil))))
Theorem:
(defthm apconvert-expr-value-when-uint-arrayp (implies (and (uint-arrayp x) (objdesignp objdes)) (equal (apconvert-expr-value (expr-value x objdes)) (expr-value (value-pointer (pointer-valid objdes) (type-uint)) nil))))
Theorem:
(defthm apconvert-expr-value-when-sint-arrayp (implies (and (sint-arrayp x) (objdesignp objdes)) (equal (apconvert-expr-value (expr-value x objdes)) (expr-value (value-pointer (pointer-valid objdes) (type-sint)) nil))))
Theorem:
(defthm apconvert-expr-value-when-ulong-arrayp (implies (and (ulong-arrayp x) (objdesignp objdes)) (equal (apconvert-expr-value (expr-value x objdes)) (expr-value (value-pointer (pointer-valid objdes) (type-ulong)) nil))))
Theorem:
(defthm apconvert-expr-value-when-slong-arrayp (implies (and (slong-arrayp x) (objdesignp objdes)) (equal (apconvert-expr-value (expr-value x objdes)) (expr-value (value-pointer (pointer-valid objdes) (type-slong)) nil))))
Theorem:
(defthm apconvert-expr-value-when-ullong-arrayp (implies (and (ullong-arrayp x) (objdesignp objdes)) (equal (apconvert-expr-value (expr-value x objdes)) (expr-value (value-pointer (pointer-valid objdes) (type-ullong)) nil))))
Theorem:
(defthm apconvert-expr-value-when-sllong-arrayp (implies (and (sllong-arrayp x) (objdesignp objdes)) (equal (apconvert-expr-value (expr-value x objdes)) (expr-value (value-pointer (pointer-valid objdes) (type-sllong)) nil))))
Theorem:
(defthm apconvert-expr-value-when-not-value-array-alt (implies (not (equal (value-kind (expr-value->value eval)) :array)) (equal (apconvert-expr-value eval) (expr-value-fix eval))))