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/Stackingproof.v | |
| parent | dcb9f48f51cec5e864565862a700c27df2a1a7e6 (diff) | |
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/Stackingproof.v')
| -rw-r--r-- | backend/Stackingproof.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 1cfb738..1d87ad3 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1734,7 +1734,8 @@ Inductive match_globalenvs (j: meminj) (bound: Z) : Prop := (DOMAIN: forall b, b < bound -> j b = Some(b, 0)) (IMAGE: forall b1 b2 delta, j 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). Inductive match_stacks (j: meminj) (m m': mem): list Linear.stackframe -> list stackframe -> signature -> Z -> Z -> Prop := @@ -2170,9 +2171,8 @@ Proof. exploit function_ptr_translated; eauto. intros [tf [A B]]. exists b; exists tf; split; auto. simpl. generalize (AG m0). rewrite EQ. intro INJ. inv INJ. - exploit Genv.find_funct_ptr_negative. unfold ge in FF; eexact FF. intros. - inv MG. rewrite (DOMAIN b) in H2. inv H2. auto. omega. - revert FF. case_eq (Genv.find_symbol ge i); intros; try discriminate. + inv MG. rewrite DOMAIN in H2. inv H2. simpl. auto. eapply FUNCTIONS; eauto. + destruct (Genv.find_symbol ge i) as [b|]_eqn; try discriminate. exploit function_ptr_translated; eauto. intros [tf [A B]]. exists b; exists tf; split; auto. simpl. rewrite symbols_preserved. auto. @@ -2742,6 +2742,7 @@ Proof. intros. unfold Mem.flat_inj. apply zlt_true; auto. unfold Mem.flat_inj; intros. destruct (zlt b1 (Mem.nextblock m0)); congruence. intros. change (Mem.valid_block m0 b0). eapply Genv.find_symbol_not_fresh; eauto. + intros. change (Mem.valid_block m0 b0). eapply Genv.find_funct_ptr_not_fresh; eauto. intros. change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto. rewrite H3. red; intros. contradiction. eapply Genv.find_funct_ptr_prop. eexact wt_prog. |