diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-03-14 00:59:49 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-14 00:59:49 +0000 |
| commit | 246ae564d9ce6c04ba4169b80d2ff9ce21deca34 (patch) | |
| tree | 08c86fe1c3c32641b98bfbe9b2588162caa40652 /verilog/ConstpropOpproof.v | |
| parent | 20096af8d044ccea01360822834c748e17acd572 (diff) | |
| download | compcert-kvx-vericert-kvx.tar.gz compcert-kvx-vericert-kvx.zip | |
Fix proofs for ptr64vericert-kvx
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. |