diff options
| author | zimmerma <zimmerma@280ebfd0-de03-0410-8827-d642c229c3f4> | 2020-04-03 06:32:52 +0000 |
|---|---|---|
| committer | zimmerma <zimmerma@280ebfd0-de03-0410-8827-d642c229c3f4> | 2020-04-03 06:32:52 +0000 |
| commit | 62e1e2957224b87f1e1ca6ef324b8c8589824cb2 (patch) | |
| tree | 34f15ebd29ef002abb94812f36a000516351d063 /INSTALL | |
| parent | 7e215e6b878e1f00be81ac7dc49ade09d9744492 (diff) | |
| download | mpfr-62e1e2957224b87f1e1ca6ef324b8c8589824cb2.tar.gz | |
[INSTALL] update CompCert instructions
git-svn-id: svn://scm.gforge.inria.fr/svn/mpfr/trunk@13866 280ebfd0-de03-0410-8827-d642c229c3f4
Diffstat (limited to 'INSTALL')
| -rw-r--r-- | INSTALL | 8 |
1 files changed, 4 insertions, 4 deletions
@@ -688,11 +688,11 @@ d. Using the CompCert compiler CompCert (http://compcert.inria.fr/) is a formally verified compiler. To compile MPFR with CompCert: -$ ./configure CC=ccomp LDFLAGS="-L$PREFIX/lib/compcert" CFLAGS="-fbitfields -flongdouble -fstruct-passing -I$PREFIX/lib/compcert/include" --disable-shared - -where $PREFIX is the directory where you have installed $PREFIX. +$ ./configure CC=ccomp CFLAGS="-fbitfields -flongdouble -fstruct-passing" --disable-shared You also need to unset LD_LIBRARY_PATH, and/or you might need to change wl="" into wl="-Wl," in the libtool file. -All tests (make check) pass. +All tests (make check) should pass (tget_set_d64, tget_set_d128 and +tset_float128 are skipped, since CompCert does not support _Decimal64, +_Decimal128 nor _Float128). |