diff options
| -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 *) |