diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-11-12 13:42:22 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-11-12 13:42:22 +0000 |
| commit | ce4951549999f403446415c135ad1403a16a15c3 (patch) | |
| tree | cac9bbb2fea29fce331916b277c38ed8fe29e471 /backend/Inliningproof.v | |
| parent | dcb9f48f51cec5e864565862a700c27df2a1a7e6 (diff) | |
| download | compcert-kvx-ce4951549999f403446415c135ad1403a16a15c3.tar.gz compcert-kvx-ce4951549999f403446415c135ad1403a16a15c3.zip | |
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
Diffstat (limited to 'backend/Inliningproof.v')
| -rw-r--r-- | backend/Inliningproof.v | 12 |
1 files changed, 7 insertions, 5 deletions
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. |