From a5ffc59246b09a389e5f8cbc2f217e323e76990f Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 13 Jun 2011 18:11:19 +0000 Subject: Revised handling of annotation statements, and more generally built-in functions, and more generally external functions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Reloadproof.v | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) (limited to 'backend/Reloadproof.v') diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 09a91010..49640a34 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -799,7 +799,7 @@ Proof. FL. FL. destruct s0; FL; FL; FL. destruct s0; FL; FL; FL. - FL. + destruct (ef_reloads e). FL. FL. FL. destruct o; FL. Qed. @@ -1254,8 +1254,9 @@ Proof. (* Lbuiltin *) ExploitWT; inv WTI. + case_eq (ef_reloads ef); intro RELOADS. exploit add_reloads_correct. - instantiate (1 := args). apply arity_ok_enough. rewrite H3. auto. auto. + instantiate (1 := args). apply arity_ok_enough. rewrite H3. destruct H5. auto. congruence. auto. intros [ls2 [A [B C]]]. exploit external_call_mem_extends; eauto. apply agree_locs; eauto. @@ -1273,6 +1274,19 @@ Proof. rewrite E. rewrite Locmap.gss. auto. intros. rewrite F; auto. rewrite Locmap.gso. rewrite undef_temps_others; auto. apply reg_for_diff; auto. + (* no reload *) + exploit external_call_mem_extends; eauto. + apply agree_locs; eauto. + intros [v' [tm' [P [Q [R S]]]]]. + assert (EQ: v = Vundef). + destruct ef; simpl in RELOADS; try congruence. simpl in H; inv H. auto. + subst v. + left; econstructor; split. + apply plus_one. eapply exec_Lannot. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto with coqlib. + apply agree_set with ls; auto. (* Llabel *) left; econstructor; split. -- cgit