From f775eda608d8b5ab71a32a5c11779aa6c5647b37 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 22 Sep 2020 08:26:42 +0200 Subject: reflect changes --- kvx/ValueAOp.v | 14 -------------- 1 file changed, 14 deletions(-) (limited to 'kvx/ValueAOp.v') 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 *) -- cgit