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 /arm/NeedOp.v | |
| parent | 7a6bb90048db7a254e959b1e3c308bac5fe6c418 (diff) | |
| download | compcert-kvx-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.tar.gz compcert-kvx-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.zip | |
Updated PR by removing whitespaces. Bug 17450.
Diffstat (limited to 'arm/NeedOp.v')
| -rw-r--r-- | arm/NeedOp.v | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/arm/NeedOp.v b/arm/NeedOp.v index e91ea64d..41b80941 100644 --- a/arm/NeedOp.v +++ b/arm/NeedOp.v @@ -120,7 +120,7 @@ Lemma needs_of_condition_sound: vagree_list args args' (needs_of_condition cond) -> eval_condition cond args' m' = Some b. Proof. - intros. unfold needs_of_condition in H0. + intros. unfold needs_of_condition in H0. eapply default_needs_of_condition_sound; eauto. Qed. @@ -129,10 +129,10 @@ Lemma needs_of_shift_sound: vagree v v' (needs_of_shift s nv) -> vagree (eval_shift s v) (eval_shift s v') nv. Proof. - intros. destruct s; simpl in *. + intros. destruct s; simpl in *. apply shlimm_sound; auto. apply shruimm_sound; auto. - apply shrimm_sound; auto. + apply shrimm_sound; auto. apply ror_sound; auto. Qed. @@ -157,32 +157,32 @@ Proof. - apply sign_ext_sound; auto. compute; auto. - apply sign_ext_sound; auto. compute; auto. - apply add_sound; auto. -- apply add_sound; auto. apply needs_of_shift_sound; auto. +- apply add_sound; auto. apply needs_of_shift_sound; auto. - apply add_sound; auto with na. -- replace (default nv) with All in *. - apply vagree_lessdef. apply val_sub_lessdef; auto with na. +- replace (default nv) with All in *. + apply vagree_lessdef. apply val_sub_lessdef; auto with na. apply lessdef_vagree. apply needs_of_shift_sound; auto with na. destruct nv; simpl; congruence. -- replace (default nv) with All in *. - apply vagree_lessdef. apply val_sub_lessdef; auto with na. +- replace (default nv) with All in *. + apply vagree_lessdef. apply val_sub_lessdef; auto with na. apply lessdef_vagree. apply needs_of_shift_sound; auto with na. destruct nv; simpl; congruence. -- apply mul_sound; auto. -- apply add_sound; auto. apply mul_sound; auto. +- apply mul_sound; auto. +- apply add_sound; auto. apply mul_sound; auto. - apply and_sound; auto. -- apply and_sound; auto. apply needs_of_shift_sound; auto. +- apply and_sound; auto. apply needs_of_shift_sound; auto. - apply andimm_sound; auto. - apply or_sound; auto. -- apply or_sound; auto. apply needs_of_shift_sound; auto. +- apply or_sound; auto. apply needs_of_shift_sound; auto. - apply orimm_sound; auto. - apply xor_sound; auto. -- apply xor_sound; auto. apply needs_of_shift_sound; auto. +- apply xor_sound; auto. apply needs_of_shift_sound; auto. - apply xor_sound; auto with na. -- apply and_sound; auto. apply notint_sound; auto. -- apply and_sound; auto. apply notint_sound. apply needs_of_shift_sound; auto. -- apply notint_sound; auto. +- apply and_sound; auto. apply notint_sound; auto. +- apply and_sound; auto. apply notint_sound. apply needs_of_shift_sound; auto. +- apply notint_sound; auto. - apply notint_sound. apply needs_of_shift_sound; auto. -- apply needs_of_shift_sound; auto. +- apply needs_of_shift_sound; auto. Qed. Lemma operation_is_redundant_sound: @@ -195,7 +195,7 @@ Proof. intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst. - apply sign_ext_redundant_sound; auto. omega. - apply sign_ext_redundant_sound; auto. omega. -- apply andimm_redundant_sound; auto. +- apply andimm_redundant_sound; auto. - apply orimm_redundant_sound; auto. Qed. |