Skip to content

GitLab

Commit 361c153b authored by Vincent Lefevre's avatar Vincent Lefevre
Browse files

Update of INSTALL file about CompCert.

parent f75b0c38
Hide whitespace changes
Inline Side-by-side
INSTALL
View file @ 361c153b
...@@ -709,15 +709,15 @@ The relevant build projects are available here: ...@@ -709,15 +709,15 @@ The relevant build projects are available here:
d. Using the CompCert compiler d. Using the CompCert compiler
============================== ==============================
[this was tested with CompCert 3.7 and MPFR revision 13851 on x86_64-linux] [Tested with CompCert 3.10 and MPFR master-11992-f75b0c388 on x86_64-linux]
CompCert (http://compcert.inria.fr/) is a formally verified compiler. CompCert (https://compcert.org/) is a formally verified compiler.
To compile MPFR with CompCert: To compile MPFR with CompCert:
$ ./configure CC=ccomp CFLAGS="-fbitfields -flongdouble -fstruct-passing" --disable-shared $ ./configure --disable-shared CC=ccomp CFLAGS="-flongdouble -fstruct-passing"
You also need to unset LD_LIBRARY_PATH, and/or you might need to change You also need to unset LD_LIBRARY_PATH, and/or you might need to change
wl="" into wl="-Wl," in the libtool file. wl="" into wl="-Wl," in the libtool file (after running configure).
All tests (make check) should pass (tget_set_d64, tget_set_d128 and All tests (make check) should pass (tget_set_d64, tget_set_d128 and
tset_float128 are skipped, since CompCert does not support _Decimal64, tset_float128 are skipped, since CompCert does not support _Decimal64,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment