diff options
| author | vlefevre <vlefevre@280ebfd0-de03-0410-8827-d642c229c3f4> | 2018-08-23 09:57:09 +0000 |
|---|---|---|
| committer | vlefevre <vlefevre@280ebfd0-de03-0410-8827-d642c229c3f4> | 2018-08-23 09:57:09 +0000 |
| commit | 302a32e1ce4f6590aa9753298e724331742c6c23 (patch) | |
| tree | 9944fd80461f16371598c90f1d30657a5b2011a0 /configure.ac | |
| parent | e111d39aa694f3c42e97c9f10c9e31715610ad4a (diff) | |
| download | mpfr-302a32e1ce4f6590aa9753298e724331742c6c23.tar.gz | |
For --enable-formally-proven-code, instead of requiring a check of the
type sizes in configure, just enable the proven code only if the types
have the sizes expected by this code.
* configure.ac: removed the FIXME.
* src/add1sp.c, src/mul.c: updated the #if test that enables the
proven code (add1sp1_extracted.c and mul_1_extracted.c).
git-svn-id: svn://scm.gforge.inria.fr/svn/mpfr/trunk@13015 280ebfd0-de03-0410-8827-d642c229c3f4
Diffstat (limited to 'configure.ac')
| -rw-r--r-- | configure.ac | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/configure.ac b/configure.ac index 908c7ec0e..d2ba87d3a 100644 --- a/configure.ac +++ b/configure.ac @@ -404,10 +404,6 @@ AC_ARG_ENABLE(lto, *) AC_MSG_ERROR([bad value for --enable-lto: yes or no]) ;; esac]) -dnl FIXME: add checks for the type sizes since the extracted code assumes -dnl that mpfr_prec_t is uint32_t (though mpfr_prec_t is signed), mpfr_exp_t -dnl is int32_t and mp_limb_t is uint64_t. For instance, many tests fail -dnl with -m32. AC_ARG_ENABLE(formally-proven-code, [ --enable-formally-proven-code use formally proven code when available |