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>

3 files changed, 24 insertions, 4 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 25c3e1dd..8fbda738 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -64,6 +64,7 @@ let option_small_data =
        then 8 else 0)
 let option_small_const = ref (!option_small_data)
 let option_timings = ref false
+let option_std = ref "c99"
 let stdlib_path = ref Configuration.stdlib_path
 let use_standard_headers =  ref Configuration.has_standard_headers
 let main_function_name = ref "main"
diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml
index 9da1e533..2a3bd740 100644
--- a/driver/CommonOptions.ml
+++ b/driver/CommonOptions.ml
@@ -10,20 +10,21 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+open Printf
 open Clflags
 open Commandline
 
 (* The version string for [tool_name] *)
 let version_string tool_name =
   if Version.buildnr <> "" && Version.tag <> "" && Version.branch <> "" then
-    Printf.sprintf "The CompCert %s, Release: %s, Build: %s, Tag: %s, Branch: %s\n"
+    sprintf "The CompCert %s, Release: %s, Build: %s, Tag: %s, Branch: %s\n"
       tool_name Version.version Version.buildnr Version.tag Version.branch
   else
-    Printf.sprintf "The CompCert %s, version %s\n" tool_name Version.version
+    sprintf "The CompCert %s, version %s\n" tool_name Version.version
 
 (* Print the version string and exit the program *)
 let print_version_and_exit tool_name () =
-  Printf.printf "%s" (version_string tool_name); exit 0
+  printf "%s" (version_string tool_name); exit 0
 
 let version_options tool_name =
   [ Exact "-version", Unit (print_version_and_exit tool_name);
@@ -42,8 +43,21 @@ let f_opt name ref =
 let set_all opts () = List.iter (fun r -> r := true) opts
 let unset_all opts () = List.iter (fun r -> r := false) opts
 
+let set_std s =
+  let s = String.lowercase_ascii s in
+  option_std := s;
+  match s with
+  | "c99" ->
+      Diagnostics.(activate_warning Celeven_extension ())
+  | "c11" | "c18" ->
+      Diagnostics.(deactivate_warning Celeven_extension ())
+  | _ ->
+      raise (CmdError (sprintf
+                         "wrong -std option: unknown standard '%s'" s))
+
 let language_support_options =
-  [ Exact "-fall", Unit (set_all all_language_support_options);
+  [ longopt "-std" set_std;
+    Exact "-fall", Unit (set_all all_language_support_options);
     Exact "-fnone", Unit (unset_all all_language_support_options);
     Exact "-fbitfields", Unit (fun () -> ()); ]
   @ f_opt "longdouble" option_flongdouble
@@ -56,6 +70,8 @@ let language_support_options =
 
 let language_support_help =
   {|Language support options (use -fno-<opt> to turn off -f<opt>) :
+  -std=c99  or  -std=c11  or  -std=c18
+                 Choose the ISO C language standard used: C99, C11 or C18.
   -flongdouble   Treat 'long double' as 'double' [off]
   -fstruct-passing  Support passing structs and unions by value as function
                     results or function arguments [off]
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" ]