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 --- backend/ValueDomain.v | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) (limited to 'backend/ValueDomain.v') diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 2ece8cdb..c8431bb7 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -1075,15 +1075,12 @@ Definition genv_match (ge: genv) : Prop := (forall id b, Genv.find_symbol ge id = Some b <-> bc b = BCglob id) /\(forall b, Plt b (Genv.genv_next ge) -> bc b <> BCinvalid /\ bc b <> BCstack). -Definition symbol_address (ge: genv) (id: ident) (ofs: int) : val := - match Genv.find_symbol ge id with Some b => Vptr b ofs | None => Vundef end. - Lemma symbol_address_sound: forall ge id ofs, genv_match ge -> - vmatch (symbol_address ge id ofs) (Ptr (Gl id ofs)). + vmatch (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)). Proof. - intros. unfold symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F. + intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F. constructor. constructor. apply H; auto. constructor. Qed. @@ -1092,9 +1089,9 @@ Lemma vmatch_ptr_gl: forall ge v id ofs, genv_match ge -> vmatch v (Ptr (Gl id ofs)) -> - Val.lessdef v (symbol_address ge id ofs). + Val.lessdef v (Genv.symbol_address ge id ofs). Proof. - intros. unfold symbol_address. inv H0. + intros. unfold Genv.symbol_address. inv H0. - inv H3. replace (Genv.find_symbol ge id) with (Some b). constructor. symmetry. apply H; auto. - constructor. -- cgit