From ce4951549999f403446415c135ad1403a16a15c3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 12 Nov 2012 13:42:22 +0000 Subject: Globalenvs: allocate one-byte block with permissions Nonempty for each function definition, so that comparisons between function pointers are correctly defined. AST, Globalenvs, and many other files: represent programs as a list of (function or variable) definitions instead of two lists, one for functions and the other for variables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Inliningproof.v | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'backend/Inliningproof.v') diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 9ca351a3..8de84875 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -358,7 +358,8 @@ Inductive match_globalenvs (F: meminj) (bound: Z): Prop := (DOMAIN: forall b, b < bound -> F b = Some(b, 0)) (IMAGE: forall b1 b2 delta, F b1 = Some(b2, delta) -> b2 < bound -> b1 = b2) (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound) - (INFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound). + (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound) + (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound). Lemma find_function_agree: forall ros rs fd F ctx rs' bound, @@ -374,9 +375,9 @@ Proof. exploit Genv.find_funct_inv; eauto. intros [b EQ]. assert (A: val_inject F rs#r rs'#(sreg ctx r)). eapply agree_val_reg; eauto. rewrite EQ in A; inv A. - inv H1. rewrite DOMAIN in H5. inv H5. auto. - rewrite EQ in H; rewrite Genv.find_funct_find_funct_ptr in H. - exploit Genv.find_funct_ptr_negative. unfold ge in H; eexact H. omega. + inv H1. rewrite DOMAIN in H5. inv H5. auto. + apply FUNCTIONS with fd. + rewrite EQ in H; rewrite Genv.find_funct_find_funct_ptr in H. auto. rewrite H2. eapply functions_translated; eauto. (* symbol *) rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try discriminate. @@ -1219,7 +1220,8 @@ Proof. apply Mem.nextblock_pos. unfold Mem.flat_inj. apply zlt_true; auto. unfold Mem.flat_inj in H. destruct (zlt b1 (Mem.nextblock m0)); congruence. - eapply Genv.find_symbol_not_fresh; eauto. + eapply Genv.find_symbol_not_fresh; eauto. + eapply Genv.find_funct_ptr_not_fresh; eauto. eapply Genv.find_var_info_not_fresh; eauto. omega. eapply Genv.initmem_inject; eauto. -- cgit