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 | |
| 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')
| -rw-r--r-- | driver/Configuration.ml | 5 | ||||
| -rw-r--r-- | driver/Configuration.mli | 2 | ||||
| -rw-r--r-- | driver/Driver.ml | 4 |
3 files changed, 9 insertions, 2 deletions
diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 2cea2b80..70131fc6 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -82,6 +82,11 @@ let has_runtime_lib = | "true" -> true | "false" -> false | v -> bad_config "has_runtime_lib" [v] +let has_standard_headers = + match get_config_string "has_standard_headers" with + | "true" -> true + | "false" -> false + | v -> bad_config "has_standard_headers" [v] let stdlib_path = if has_runtime_lib then get_config_string "stdlib_path" 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 *) diff --git a/driver/Driver.ml b/driver/Driver.ml index aaaeb5b5..480cf665 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -93,8 +93,8 @@ let preprocess ifile ofile = let cmd = List.concat [ Configuration.prepro; ["-D__COMPCERT__"]; - (if Configuration.has_runtime_lib - then ["-I" ^ !stdlib_path] + (if Configuration.has_standard_headers + then ["-I" ^ Filename.concat !stdlib_path "include" ] else []); List.rev !prepro_options; [ifile] |