diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-06-08 08:32:53 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-06-08 08:32:53 +0200 |
| commit | 744dc278d24b15a72ef471fc25c1c8a8df62cc4e (patch) | |
| tree | 6d7340f815cf1c01d50e10313ae034a2821b6a2a /configure | |
| parent | 584eac7027cd4d29c5ca8744453ffeea8f18b501 (diff) | |
| parent | 1cdf4f22706dea5371f6d553538ac68f1f0a159f (diff) | |
| download | compcert-744dc278d24b15a72ef471fc25c1c8a8df62cc4e.tar.gz compcert-744dc278d24b15a72ef471fc25c1c8a8df62cc4e.zip | |
Merge pull request #43 from AbsInt/standard-headers
Merge of the "standard-headers" branch. This provides CompCert-compatible implementations of the following standard headers: float.h, stdarg.h, stdbool.h, stddef.h, varargs.h.
These are the headers that are provided by GCC, Clang, and TCC. Other standard headers are provided by Glibc and similar C standard libraries.
So far in CompCert we rely on the headers provided by whatever C compiler is installed on the host platform. This causes some difficulties that this branch addresses:
1- Diab C's stdarg.h is not compatible with CompCert
2- On IA32 and PowerPC, CompCert's "long double" type differs from the "long double" type specified by the ABI. Hence, the platform's float.h gives "long double" parameters that do not match CompCert.
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 12 |
1 files changed, 11 insertions, 1 deletions
@@ -18,6 +18,7 @@ libdir='$(PREFIX)/lib/compcert' toolprefix='' target='' has_runtime_lib=true +has_standard_headers=true build_checklink=true advanced_debug=false @@ -49,6 +50,7 @@ Options: -libdir <dir> Install libraries in <dir> -toolprefix <pref> Prefix names of tools ("gcc", etc) with <pref> -no-runtime-lib Do not compile nor install the runtime support library + -no-standard-headers Do not install nor use the standard .h headers ' # Parse command-line arguments @@ -66,6 +68,8 @@ while : ; do toolprefix="$2"; shift;; -no-runtime-lib) has_runtime_lib=false;; + -no-standard-headers) + has_standard_headers=false;; -no-checklink) build_checklink=false;; *) @@ -357,6 +361,7 @@ CASMRUNTIME=$casmruntime CLINKER=$clinker LIBMATH=$libmath HAS_RUNTIME_LIB=$has_runtime_lib +HAS_STANDARD_HEADERS=$has_standard_headers CCHECKLINK=$cchecklink ASM_SUPPORTS_CFI=$asm_supports_cfi ADVANCED_DEBUG=$advanced_debug @@ -428,9 +433,12 @@ CLINKER=gcc # Math library. Set to empty under MacOS X LIBMATH=-lm -# Do not change +# Turn on/off the installation and use of the runtime support library HAS_RUNTIME_LIB=true +# Turn on/off the installation and use of the standard header files +HAS_STANDARD_HEADERS=true + # Whether the assembler $(CASM) supports .cfi debug directives ASM_SUPPORTS_CFI=false #ASM_SUPPORTS_CFI=true @@ -471,6 +479,8 @@ CompCert configuration: Binaries installed in......... $bindirexp Runtime library provided...... $has_runtime_lib Library files installed in.... $libdirexp + Standard headers provided..... $has_standard_headers + Standard headers installed in. $libdirexp/include cchecklink tool supported..... $cchecklink Build command to use.......... $make |