From a36948c2af873559e5df4a2d96fdbc5bbfcfaca8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 9 Jan 2020 08:02:36 +0100 Subject: fix bug and forward in proofs --- backend/ForwardMovesproof.v | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) (limited to 'backend/ForwardMovesproof.v') diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v index 99b546c7..aa516df4 100644 --- a/backend/ForwardMovesproof.v +++ b/backend/ForwardMovesproof.v @@ -403,7 +403,22 @@ Proof. rewrite subst_args_ok; eassumption. constructor; auto. - admit. + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + apply get_rb_sem_ge with (rb2 := map # pc); trivial. + replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. + destruct b; tauto. + } + unfold apply_instr'. + unfold get_rb_sem in *. + destruct (map # pc) in *; try contradiction. + rewrite H. + reflexivity. (* jumptbl *) - econstructor; split. -- cgit