diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-06-13 18:11:19 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-06-13 18:11:19 +0000 |
| commit | a5ffc59246b09a389e5f8cbc2f217e323e76990f (patch) | |
| tree | e1bc7cc54518aad7c20645f187cee8110de8cff9 /backend/Reloadproof.v | |
| parent | 4daccd62b92b23016d3f343d5691f9c164a8a951 (diff) | |
| download | compcert-a5ffc59246b09a389e5f8cbc2f217e323e76990f.tar.gz compcert-a5ffc59246b09a389e5f8cbc2f217e323e76990f.zip | |
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
Diffstat (limited to 'backend/Reloadproof.v')
| -rw-r--r-- | backend/Reloadproof.v | 18 |
1 files changed, 16 insertions, 2 deletions
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. |