From 8b9a4cb340bc135da9907c7d313caa11d078cb16 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 14 Mar 2020 07:56:47 +0100 Subject: Icond --- backend/CSE3proof.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'backend/CSE3proof.v') diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 3a7590ea..8a49fe87 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -642,9 +642,10 @@ Proof. * IND_STEP. - (* Icond *) econstructor. split. - + eapply exec_Icond; try eassumption. - * erewrite transf_function_at by eauto. simpl. - admit. + + eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption. + * TR_AT. reflexivity. + * rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. + eassumption. * reflexivity. + econstructor; eauto. destruct b; IND_STEP. -- cgit