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 /driver/Configuration.mli | |
| 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 'driver/Configuration.mli')
| -rw-r--r-- | driver/Configuration.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/driver/Configuration.mli b/driver/Configuration.mli index 20c45518..72810456 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -31,6 +31,8 @@ val stdlib_path: string (** Path to CompCert's library *) val has_runtime_lib: bool (** True if CompCert's library is available. *) +val has_standard_headers: bool + (** True if CompCert's standard header files is available. *) val advanced_debug: bool (** True if advanced debug is implement for the Target *) |