From 60e4ad85c6cd433c9e28c9e407a957ca3a302c22 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 16 Apr 2020 18:00:14 +0200 Subject: CSE3: better builtin handling --- backend/CSE3proof.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'backend/CSE3proof.v') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 19fb20be..53872e62 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -224,7 +224,6 @@ Proof. eapply function_ptr_translated; eauto. Qed. -Check sem_rel_b. Inductive match_stackframes: list stackframe -> list stackframe -> signature -> Prop := | match_stackframes_nil: forall sg, sg.(sig_res) = Tint -> @@ -428,8 +427,8 @@ Ltac IND_STEP := destruct ((fst (preanalysis tenv fn)) # mpc) as [zinv | ]; simpl in *; intuition; - eapply rel_ge; eauto with cse3; - idtac mpc mpc' fn minstr + eapply rel_ge; eauto with cse3 (* ; for printing + idtac mpc mpc' fn minstr *) end. Lemma if_same : forall {T : Type} (b : bool) (x : T), @@ -753,6 +752,9 @@ Proof. + econstructor; eauto. * eapply wt_exec_Ibuiltin with (f:=f); eauto with wt. * IND_STEP. + apply kill_builtin_res_sound; eauto with cse3. + eapply external_call_sound; eauto with cse3. + - (* Icond *) econstructor. split. + eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption. -- cgit