From 3fa79790e617d87584598746296e626e0ce3b256 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 24 May 2014 09:46:07 +0000 Subject: Refactoring: move symbol_offset into Genv. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/Asmgenproof.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'ia32/Asmgenproof.v') diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index fa8ce6c..881375f 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -613,7 +613,7 @@ Opaque loadind. left; econstructor; split. apply plus_one. eapply exec_step_internal. eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. - simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. eauto. + simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. eauto. econstructor; eauto. econstructor; eauto. eapply agree_sp_def; eauto. @@ -665,7 +665,7 @@ Opaque loadind. econstructor; eauto. apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto. eapply agree_change_sp; eauto. eapply parent_sp_def; eauto. - rewrite Pregmap.gss. unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. + rewrite Pregmap.gss. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto. - (* Mbuiltin *) inv AT. monadInv H3. @@ -900,13 +900,13 @@ Proof. econstructor; split. econstructor. eapply Genv.init_mem_transf_partial; eauto. - replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero) + replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Int.zero) with (Vptr fb Int.zero). econstructor; eauto. constructor. apply Mem.extends_refl. split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. - unfold symbol_offset. + unfold Genv.symbol_address. rewrite (transform_partial_program_main _ _ TRANSF). rewrite symbols_preserved. unfold ge; rewrite H1. auto. -- cgit v1.2.3