diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-22 08:26:42 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-22 08:26:42 +0200 |
| commit | f775eda608d8b5ab71a32a5c11779aa6c5647b37 (patch) | |
| tree | 8faf9374b7e8bc7c9b5d6099c12de29c34ee76e8 /kvx/ValueAOp.v | |
| parent | cdb48111d4baff50d8708b979f8b31ef21505247 (diff) | |
| download | compcert-kvx-f775eda608d8b5ab71a32a5c11779aa6c5647b37.tar.gz compcert-kvx-f775eda608d8b5ab71a32a5c11779aa6c5647b37.zip | |
reflect changes
Diffstat (limited to 'kvx/ValueAOp.v')
| -rw-r--r-- | kvx/ValueAOp.v | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v index ed8de163..0206352e 100644 --- a/kvx/ValueAOp.v +++ b/kvx/ValueAOp.v @@ -544,16 +544,6 @@ Proof. inv H1; simpl; try constructor. all: destruct Int.ltu; [simpl | constructor; fail]. all: auto with va. - - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with - | Vlong n2 => Vlong (Int64.add n n2) - | Vptr b2 ofs2 => - if Archi.ptr64 - then Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int64 n)) - else Vundef - | _ => Vundef - end) with (Val.addl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))). - + eauto with va. - + destruct a1; destruct shift; reflexivity. - inv H1; constructor. - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with | Vlong n2 => Vlong (Int64.sub n n2) @@ -561,10 +551,6 @@ Proof. end) with (Val.subl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))). + eauto with va. + destruct a1; destruct shift; reflexivity. - - (* shrxl *) - inv H1; simpl; try constructor. - all: destruct Int.ltu; [simpl | constructor; fail]. - all: auto with va. - apply of_optbool_sound. eapply eval_static_condition_sound; eauto. (* extfz *) |