diff options
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 cec3b59..02d3bee 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. |