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 --- powerpc/Asmgenproof.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'powerpc/Asmgenproof.v') diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 5c992312..879d7524 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -642,7 +642,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. @@ -733,7 +733,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. eapply functions_transl; eauto. eapply find_instr_tail. repeat (eapply code_tail_next_int; auto). eauto. - simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. traceEq. + simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto. traceEq. (* match states *) econstructor; eauto. assert (AG3: agree rs (Vptr stk soff) rs3). @@ -972,13 +972,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