Rules for executing the indirection unary operation.
Theorem:
(defthm exec-indir-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))))) (valuep x) (value-case x :pointer) (value-pointer-validp x) (equal (value-pointer->reftype x) (type-schar)) (unop-case op :indir) (equal objdes (value-pointer->designator x)) (equal val (read-object objdes compst)) (scharp val)) (equal (exec-unary op (expr-value x objdes-x) compst) (expr-value val objdes))))
Theorem:
(defthm exec-indir-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))))) (valuep x) (value-case x :pointer) (value-pointer-validp x) (equal (value-pointer->reftype x) (type-uchar)) (unop-case op :indir) (equal objdes (value-pointer->designator x)) (equal val (read-object objdes compst)) (ucharp val)) (equal (exec-unary op (expr-value x objdes-x) compst) (expr-value val objdes))))
Theorem:
(defthm exec-indir-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))))) (valuep x) (value-case x :pointer) (value-pointer-validp x) (equal (value-pointer->reftype x) (type-sshort)) (unop-case op :indir) (equal objdes (value-pointer->designator x)) (equal val (read-object objdes compst)) (sshortp val)) (equal (exec-unary op (expr-value x objdes-x) compst) (expr-value val objdes))))
Theorem:
(defthm exec-indir-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))))) (valuep x) (value-case x :pointer) (value-pointer-validp x) (equal (value-pointer->reftype x) (type-ushort)) (unop-case op :indir) (equal objdes (value-pointer->designator x)) (equal val (read-object objdes compst)) (ushortp val)) (equal (exec-unary op (expr-value x objdes-x) compst) (expr-value val objdes))))
Theorem:
(defthm exec-indir-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))))) (valuep x) (value-case x :pointer) (value-pointer-validp x) (equal (value-pointer->reftype x) (type-sint)) (unop-case op :indir) (equal objdes (value-pointer->designator x)) (equal val (read-object objdes compst)) (sintp val)) (equal (exec-unary op (expr-value x objdes-x) compst) (expr-value val objdes))))
Theorem:
(defthm exec-indir-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))))) (valuep x) (value-case x :pointer) (value-pointer-validp x) (equal (value-pointer->reftype x) (type-uint)) (unop-case op :indir) (equal objdes (value-pointer->designator x)) (equal val (read-object objdes compst)) (uintp val)) (equal (exec-unary op (expr-value x objdes-x) compst) (expr-value val objdes))))
Theorem:
(defthm exec-indir-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))))) (valuep x) (value-case x :pointer) (value-pointer-validp x) (equal (value-pointer->reftype x) (type-slong)) (unop-case op :indir) (equal objdes (value-pointer->designator x)) (equal val (read-object objdes compst)) (slongp val)) (equal (exec-unary op (expr-value x objdes-x) compst) (expr-value val objdes))))
Theorem:
(defthm exec-indir-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))))) (valuep x) (value-case x :pointer) (value-pointer-validp x) (equal (value-pointer->reftype x) (type-ulong)) (unop-case op :indir) (equal objdes (value-pointer->designator x)) (equal val (read-object objdes compst)) (ulongp val)) (equal (exec-unary op (expr-value x objdes-x) compst) (expr-value val objdes))))
Theorem:
(defthm exec-indir-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))))) (valuep x) (value-case x :pointer) (value-pointer-validp x) (equal (value-pointer->reftype x) (type-sllong)) (unop-case op :indir) (equal objdes (value-pointer->designator x)) (equal val (read-object objdes compst)) (sllongp val)) (equal (exec-unary op (expr-value x objdes-x) compst) (expr-value val objdes))))
Theorem:
(defthm exec-indir-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))))) (valuep x) (value-case x :pointer) (value-pointer-validp x) (equal (value-pointer->reftype x) (type-ullong)) (unop-case op :indir) (equal objdes (value-pointer->designator x)) (equal val (read-object objdes compst)) (ullongp val)) (equal (exec-unary op (expr-value x objdes-x) compst) (expr-value val objdes))))