From 7698300cfe2d3f944ce2e1d4a60a263620487718 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 20 Dec 2013 13:05:53 +0000 Subject: Merge of branch value-analysis. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/SelectOpproof.v | 18 +----------------- 1 file changed, 1 insertion(+), 17 deletions(-) (limited to 'ia32/SelectOpproof.v') diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index cec3b599..02d3bee5 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -145,22 +145,6 @@ Proof. intros. unfold symbol_address. destruct (Genv.find_symbol); auto. Qed. -Lemma eval_offset_addressing: - forall addr n args v, - eval_addressing ge sp addr args = Some v -> - eval_addressing ge sp (offset_addressing addr n) args = Some (Val.add v (Vint n)). -Proof. - intros. destruct addr; simpl in *; FuncInv; subst; simpl. - rewrite Val.add_assoc. auto. - repeat rewrite Val.add_assoc. auto. - rewrite Val.add_assoc. auto. - repeat rewrite Val.add_assoc. auto. - rewrite shift_symbol_address. auto. - rewrite shift_symbol_address. repeat rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut. - rewrite shift_symbol_address. repeat rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut. - rewrite Val.add_assoc. auto. -Qed. - Theorem eval_addimm: forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)). Proof. @@ -170,7 +154,7 @@ Proof. destruct x; simpl; auto. rewrite Int.add_zero. auto. rewrite Int.add_zero. auto. case (addimm_match a); intros; InvEval; simpl. TrivialExists; simpl. rewrite Int.add_commut. auto. - inv H0. simpl in H6. TrivialExists. simpl. eapply eval_offset_addressing; eauto. + inv H0. simpl in H6. TrivialExists. simpl. eapply eval_offset_addressing_total; eauto. TrivialExists. Qed. -- cgit