diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-08 14:22:21 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-08 14:22:21 +0100 |
| commit | de098d0ea0ea48e6d13a4922ef58a4b918f1b551 (patch) | |
| tree | 5d9d3190f5fbc587f859a0fd44310f12245e69ef /backend/SelectDivproof.v | |
| parent | 292db3a22261821b759abdca011ab93ed01f3cce (diff) | |
| download | compcert-kvx-de098d0ea0ea48e6d13a4922ef58a4b918f1b551.tar.gz compcert-kvx-de098d0ea0ea48e6d13a4922ef58a4b918f1b551.zip | |
Desactivated Omulhs 32-bits optimization (division by constant)
Diffstat (limited to 'backend/SelectDivproof.v')
| -rw-r--r-- | backend/SelectDivproof.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 75713289..aa6750ed 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -660,9 +660,9 @@ Proof. + eapply eval_divs_base; eauto. EvalOp. - destruct (Compopts.optim_for_size tt). + eapply eval_divs_base; eauto. EvalOp. - + destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. + + (* destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. * exists (Vint (Int.divs i n2)); split; auto. - econstructor; eauto. eapply eval_divs_mul; eauto. + econstructor; eauto. eapply eval_divs_mul; eauto. *) (* FIXME - hack K1 *) * eapply eval_divs_base; eauto. EvalOp. Qed. @@ -709,11 +709,11 @@ Proof. + eapply eval_mods_base; eauto. EvalOp. - destruct (Compopts.optim_for_size tt). + eapply eval_mods_base; eauto. EvalOp. - + destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. + + (* destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. * econstructor; split. econstructor. eauto. apply eval_mod_from_div with (x := i); auto. eapply eval_divs_mul with (x := i); eauto. - simpl. auto. + simpl. auto. *) (* FIXME - hack K1 *) * eapply eval_mods_base; eauto. EvalOp. Qed. |