diff options
Diffstat (limited to 'verilog/ConstpropOpproof.v')
| -rw-r--r-- | verilog/ConstpropOpproof.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/verilog/ConstpropOpproof.v b/verilog/ConstpropOpproof.v index 74dc4a05..efeec6f6 100644 --- a/verilog/ConstpropOpproof.v +++ b/verilog/ConstpropOpproof.v @@ -17,6 +17,8 @@ Require Import Integers Floats Values Memory Globalenvs Events. Require Import Op Registers RTL ValueDomain. Require Import ConstpropOp. +#[local] Opaque Archi.ptr64. + Section STRENGTH_REDUCTION. Variable bc: block_classification. @@ -201,7 +203,8 @@ Proof. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. exists (e#r); split; auto. destruct (e#r); simpl; auto; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto. - destruct Archi.ptr64; auto. + destruct Archi.ptr64 eqn:?; auto. + exists (Val.add e#r (Vint n)); split; auto. exists (Val.add e#r (Vint n)); split; auto. Qed. @@ -406,7 +409,7 @@ Proof. predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. subst. exists (e#r); split; auto. destruct (e#r); simpl; auto; rewrite ? Int64.add_zero, ? Ptrofs.add_zero; auto. - destruct Archi.ptr64; auto. + destruct Archi.ptr64 eqn:?; auto; exists (Val.addl e#r (Vlong n)); split; auto. Qed. |