diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-09-04 19:15:10 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2022-09-23 13:55:44 +0200 |
| commit | 5ba25e22bc28005a5b8893d546eba5606898667c (patch) | |
| tree | 81cc2b5ba02642654bba523d099a981bc469f41e /driver/Frontend.ml | |
| parent | 43de01e92a629d6728b48be1a7d38ee9a37c2626 (diff) | |
| download | compcert-5ba25e22bc28005a5b8893d546eba5606898667c.tar.gz compcert-5ba25e22bc28005a5b8893d546eba5606898667c.zip | |
Support the `-std=<standard>` option (#456)
It has two effects:
- With a GNU toolchain, it's passed down to the preprocessor.
This influences the contents of standard includes.
- It determines the default effect of the "C11 feature" warning:
-std=c99: warn on the use of C11 features
-std=c11 or -std=c18: don't warn
For backward compatiblity, the default, if no `-std` option is given,
is to not warn, but to pass `-std=c99` to the preprocessor.
Co-authored-by: Bernhard Schommer <bschommer@users.noreply.github.com>
Diffstat (limited to 'driver/Frontend.ml')
| -rw-r--r-- | driver/Frontend.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 4ee5c712..5d45306d 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -57,6 +57,9 @@ let preprocess ifile ofile = if ofile = "-" then None else Some ofile in let cmd = List.concat [ Configuration.prepro; + (if Configuration.gnu_toolchain + then ["-std=" ^ !option_std] + else []); predefined_macros; (if !Clflags.use_standard_headers then ["-I" ^ Filename.concat !Clflags.stdlib_path "include" ] |