diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-12-20 13:05:53 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-12-20 13:05:53 +0000 |
| commit | 7698300cfe2d3f944ce2e1d4a60a263620487718 (patch) | |
| tree | 74292bb5f65bc797906b5c768df2e2e937e869b6 /ia32/SelectOpproof.v | |
| parent | c511207bd0f25c4199770233175924a725526bd3 (diff) | |
| download | compcert-7698300cfe2d3f944ce2e1d4a60a263620487718.tar.gz compcert-7698300cfe2d3f944ce2e1d4a60a263620487718.zip | |
Merge of branch value-analysis.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/SelectOpproof.v')
| -rw-r--r-- | ia32/SelectOpproof.v | 18 |
1 files changed, 1 insertions, 17 deletions
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. |