diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-04-06 14:48:47 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-04-06 14:48:47 +0200 |
| commit | df7b43a096e9a274b5b3ba8ca85275c637557c12 (patch) | |
| tree | ff810640608a3d65f1ec362f4b546a0a014b56ea /driver/Frontend.ml | |
| parent | df1024c6ac6e065d44023df5208bd2b5d9fbec5f (diff) | |
| download | compcert-kvx-df7b43a096e9a274b5b3ba8ca85275c637557c12.tar.gz compcert-kvx-df7b43a096e9a274b5b3ba8ca85275c637557c12.zip | |
Define C11 conditional feature macros (#77)
These macros can be defined to indicate that variable length
arrays, the _Complex type, atomics and threads are not supported.
Since the _Complex type is not supported, we also need
to undefine __STDC_IEC_559_COMPLEX__
Bug 23408
Diffstat (limited to 'driver/Frontend.ml')
| -rw-r--r-- | driver/Frontend.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 209e72e9..9b7d5328 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -17,6 +17,15 @@ open Driveraux (* Common frontend functions between clightgen and ccomp *) +let predefined_macros = + [ + "-D__COMPCERT__"; + "-U__STDC_IEC_559_COMPLEX__"; + "-D__STDC_NO_ATOMICS__"; + "-D__STDC_NO_COMPLEX__"; + "-D__STDC_NO_THREADS__"; + "-D__STDC_NO_VLA__" + ] (* From C to preprocessed C *) @@ -26,7 +35,7 @@ let preprocess ifile ofile = if ofile = "-" then None else Some ofile in let cmd = List.concat [ Configuration.prepro; - ["-D__COMPCERT__"]; + predefined_macros; (if !Clflags.use_standard_headers then ["-I" ^ Filename.concat !Clflags.stdlib_path "include" ] else []); |