diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-03-07 09:22:56 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-03-07 09:22:56 +0000 |
| commit | fdcaf6fabd3d594e40a2b7a31341202e9a93f5cb (patch) | |
| tree | 807d8c24c96db39b596a7e75d746d70ba196e01f /powerpc/SelectOpproof.v | |
| parent | 2f37eb9bd85b6638cce1c2e75c71cdc642acf80a (diff) | |
| download | compcert-kvx-fdcaf6fabd3d594e40a2b7a31341202e9a93f5cb.tar.gz compcert-kvx-fdcaf6fabd3d594e40a2b7a31341202e9a93f5cb.zip | |
PowerPC: remove the fmadd and fmsub operators/Asm instructions
(definitely not semantics-preserving; hard to justify).
CPragmas: make sure SDAs are not recognized on MacOSX.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1836 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/SelectOpproof.v')
| -rw-r--r-- | powerpc/SelectOpproof.v | 15 |
1 files changed, 2 insertions, 13 deletions
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 1d35d9f8..27a0fd01 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -631,23 +631,12 @@ Qed. Theorem eval_addf: binary_constructor_sound addf Val.addf. Proof. - red; intros until y; unfold addf. - destruct (use_fused_mul tt); simpl. - case (addf_match a b); intros; InvEval. - TrivialExists. simpl. congruence. - TrivialExists. simpl. rewrite Val.addf_commut. congruence. - intros. TrivialExists. - intros. TrivialExists. + red; intros; TrivialExists. Qed. Theorem eval_subf: binary_constructor_sound subf Val.subf. Proof. - red; intros until y; unfold subf. - destruct (use_fused_mul tt); simpl. - case (subf_match a); intros; InvEval. - TrivialExists. simpl. congruence. - TrivialExists. - intros. TrivialExists. + red; intros; TrivialExists. Qed. Theorem eval_mulf: binary_constructor_sound mulf Val.mulf. |