diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
commit | 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f (patch) | |
tree | 1961b41815fc6e392cc0bd2beeb0fb504bc160ce /ia32/NeedOp.v | |
parent | 7a6bb90048db7a254e959b1e3c308bac5fe6c418 (diff) | |
download | compcert-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.tar.gz compcert-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.zip |
Updated PR by removing whitespaces. Bug 17450.
Diffstat (limited to 'ia32/NeedOp.v')
-rw-r--r-- | ia32/NeedOp.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/ia32/NeedOp.v b/ia32/NeedOp.v index 52b9fcbe..07eec160 100644 --- a/ia32/NeedOp.v +++ b/ia32/NeedOp.v @@ -116,7 +116,7 @@ Proof. intros. destruct cond; simpl in H; try (eapply default_needs_of_condition_sound; eauto; fail); simpl in *; FuncInv; InvAgree. -- eapply maskzero_sound; eauto. +- eapply maskzero_sound; eauto. - destruct (Val.maskzero_bool v i) as [b'|] eqn:MZ; try discriminate. erewrite maskzero_sound; eauto. Qed. @@ -132,8 +132,8 @@ Proof. unfold needs_of_addressing; intros. destruct addr; simpl in *; FuncInv; InvAgree; TrivialExists; auto using add_sound, mul_sound with na. - apply add_sound; auto with na. apply add_sound; rewrite modarith_idem; auto. - apply add_sound; auto. apply add_sound; rewrite modarith_idem; auto with na. + apply add_sound; auto with na. apply add_sound; rewrite modarith_idem; auto. + apply add_sound; auto. apply add_sound; rewrite modarith_idem; auto with na. apply mul_sound; rewrite modarith_idem; auto with na. Qed. @@ -148,9 +148,9 @@ Lemma needs_of_operation_sound: Proof. unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail); simpl in *; FuncInv; InvAgree; TrivialExists. -- apply sign_ext_sound; auto. compute; auto. +- apply sign_ext_sound; auto. compute; auto. - apply zero_ext_sound; auto. omega. -- apply sign_ext_sound; auto. compute; auto. +- apply sign_ext_sound; auto. compute; auto. - apply zero_ext_sound; auto. omega. - apply neg_sound; auto. - apply mul_sound; auto. @@ -164,10 +164,10 @@ Proof. - apply notint_sound; auto. - apply shlimm_sound; auto. - apply shrimm_sound; auto. -- apply shruimm_sound; auto. -- apply ror_sound; auto. +- apply shruimm_sound; auto. +- apply ror_sound; auto. - eapply needs_of_addressing_sound; eauto. -- destruct (eval_condition c args m) as [b|] eqn:EC; simpl in H2. +- destruct (eval_condition c args m) as [b|] eqn:EC; simpl in H2. erewrite needs_of_condition_sound by eauto. subst v; simpl. auto with na. subst v; auto with na. @@ -185,7 +185,7 @@ Proof. - apply zero_ext_redundant_sound; auto. omega. - apply sign_ext_redundant_sound; auto. omega. - apply zero_ext_redundant_sound; auto. omega. -- apply andimm_redundant_sound; auto. +- apply andimm_redundant_sound; auto. - apply orimm_redundant_sound; auto. Qed. |