Support the -std=<standard> command-line option

configure

@@ -248,7 +248,7 @@ if test "$arch" = "arm"; then
         exit 2;;
   esac
 
-  cprepro_options="-std=c99 -U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E"
+  cprepro_options="-U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E"
   system="linux"
 fi
 
@@ -293,7 +293,7 @@ if test "$arch" = "powerpc"; then
         ;;
     *)
         casmruntime="${toolprefix}gcc -c -Wa,-mregnames"
-        cprepro_options="-std=c99 -U__GNUC__ -E"
+        cprepro_options="-U__GNUC__ -E"
         system="linux"
         ;;
   esac
@@ -311,23 +311,23 @@ if test "$arch" = "x86" -a "$bitsize" = "32"; then
         cc_options="-m32"
         casm_options="-m32 -c"
         clinker_options="-m32"
-        cprepro_options="-std=c99 -m32 -U__GNUC__ -E"
+        cprepro_options="-m32 -U__GNUC__ -E"
         system="bsd"
         ;;
     cygwin)
         abi="standard"
         cc_options="-m32"
         casm_options="-m32 -c"
         clinker_options="-m32"
-        cprepro_options="-std=c99 -m32 -U__GNUC__ '-D__attribute__(x)=' -E"
+        cprepro_options="-m32 -U__GNUC__ '-D__attribute__(x)=' -E"
         system="cygwin"
         ;;
     linux)
         abi="standard"
         cc_options="-m32"
         casm_options="-m32 -c"
         clinker_options="-m32"
-        cprepro_options="-std=c99 -m32 -U__GNUC__ -E"
+        cprepro_options="-m32 -U__GNUC__ -E"
         system="linux"
         ;;
     *)
@@ -348,15 +348,15 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
         cc_options="-m64"
         casm_options="-m64 -c"
         clinker_options="-m64"
-        cprepro_options="-std=c99 -m64 -U__GNUC__ -U__SIZEOF_INT128__ -E"
+        cprepro_options="-m64 -U__GNUC__ -U__SIZEOF_INT128__ -E"
         system="bsd"
         ;;
     linux)
         abi="standard"
         cc_options="-m64"
         casm_options="-m64 -c"
         clinker_options="-m64"
-        cprepro_options="-std=c99 -m64 -U__GNUC__ -U__SIZEOF_INT128__ -E"
+        cprepro_options="-m64 -U__GNUC__ -U__SIZEOF_INT128__ -E"
         system="linux"
         ;;
     macos|macosx)
@@ -365,7 +365,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
         casm_options="-arch x86_64 -c"
         clinker_options="-arch x86_64"
         clinker_needs_no_pie=false
-        cprepro_options="-std=c99 -arch x86_64 -U__GNUC__ -U__SIZEOF_INT128__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E"
+        cprepro_options="-arch x86_64 -U__GNUC__ -U__SIZEOF_INT128__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E"
         libmath=""
         system="macos"
         ;;
@@ -374,7 +374,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
         cc_options="-m64"
         casm_options="-m64 -c"
         clinker_options="-m64"
-        cprepro_options="-std=c99 -m64 -U__GNUC__ -U__SIZEOF_INT128__ '-D__attribute__(x)=' -E"
+        cprepro_options="-m64 -U__GNUC__ -U__SIZEOF_INT128__ '-D__attribute__(x)=' -E"
         system="cygwin"
         ;;
     *)
@@ -398,7 +398,7 @@ if test "$arch" = "riscV"; then
   cc_options="$model_options"
   casm_options="$model_options -c"
   clinker_options="$model_options"
-  cprepro_options="$model_options -std=c99 -U__GNUC__ -E"
+  cprepro_options="$model_options -U__GNUC__ -E"
   system="linux"
 fi
 
@@ -409,7 +409,7 @@ if test "$arch" = "aarch64"; then
   case "$target" in
     linux)
         abi="standard"
-        cprepro_options="-std=c99 -U__GNUC__ -E"
+        cprepro_options="-U__GNUC__ -E"
         system="linux";;
     macos|macosx)
         abi="apple"
@@ -419,7 +419,7 @@ if test "$arch" = "aarch64"; then
         clinker="${toolprefix}cc"
         clinker_needs_no_pie=false
         cprepro="${toolprefix}cc"
-        cprepro_options="-std=c99 -arch arm64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E"
+        cprepro_options="-arch arm64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E"
         libmath=""
         system="macos"
         ;;

cparser/Diagnostics.mli

@@ -100,3 +100,16 @@ val error_summary : unit -> unit
 
 val active_warning : warning_type -> bool
 (** Test whether a warning is active to avoid costly checks *)
+
+val activate_warning : warning_type -> unit -> unit
+(** Turn the given warning on *)
+
+val deactivate_warning : warning_type -> unit -> unit
+(** Turn the given warning off *)
+
+val warning_as_error : warning_type -> unit -> unit
+(** Turn the given warning on and report it as an error *)
+
+val warning_not_as_error : warning_type -> unit -> unit
+(** Do not report the given warning as an error *)
+

debug/DebugInit.ml

@@ -36,14 +36,16 @@ let init () =
     init_none ()
 
 let gnu_debugging_help =
-"  -gdwarf-       Generate debug information in DWARF v2 or DWARF v3\n"
+{|  -gdwarf-2     Generate debug information in DWARF v2 format
+  -gdwarf-3     Generate debug information in DWARF v3 format
+|}
 
 let debugging_help =
 {|Debugging options:
   -g             Generate debugging information
   -g<n>          Control generation of debugging information
-                 (<n>=0: none, <n>=1: only-globals, <n>=2: globals + locals
-                 without locations, <n>=3: full;)
+                 (<n>=0: none, <n>=1: only globals,
+                  <n>=2: globals + locals without locations, <n>=3: full)
 |}
 ^ (if Configuration.gnu_toolchain then gnu_debugging_help else "")
 

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"

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]

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" ]

lib/Commandline.ml

@@ -91,14 +91,11 @@ let parse_array spec argv first last =
           end
       | Some(Integer fn) ->
           if i + 1 <= last then begin
-            let n =
-              try
-                int_of_string argv.(i+1)
-              with Failure _ ->
+            match int_of_string_opt argv.(i+1) with
+            | Some n -> fn n; parse (i+2)
+            | None ->
                 let msg = sprintf "argument to option `%s' must be an integer" s in
                 raise (CmdError msg)
-            in
-            fn n; parse (i+2)
           end else begin
             let msg = sprintf  "option `%s' expects an argument" s in
             raise (CmdError msg)
@@ -124,19 +121,15 @@ let argv =
 let parse_cmdline spec =
   parse_array spec argv 1 (Array.length argv - 1)
 
-let long_int_action key s =
-  let ls = String.length s
-  and lkey = String.length key in
-  assert (ls > lkey);
-  let s = String.sub s (lkey + 1) (ls - lkey - 1) in
-  try
-    int_of_string s
-  with Failure _ ->
-    let msg =  sprintf "argument to option `%s' must be an integer" key in
-    raise (CmdError msg)
+let longopt key f =
+  let lkey = String.length key + 1 in
+  let act s = f (String.sub s lkey (String.length s - lkey)) in
+  (Prefix (key ^ "="), Self act)
 
 let longopt_int key f =
-  let act s =
-    let n = long_int_action key s in
-    f n in
-  Prefix (key ^ "="),Self act
+  longopt key (fun s ->
+    match int_of_string_opt s with
+    | Some n -> f n
+    | None ->
+        let msg =  sprintf "argument to option `%s' must be an integer" key in
+        raise (CmdError msg))

lib/Commandline.mli

@@ -47,6 +47,11 @@ val parse_cmdline: (pattern * action) list -> unit
     and performs all [actions].  Raises [CmdError] if an error occurred.
 *)
 
+val longopt: string -> (string -> unit) -> pattern * action
+(** [longopt_int key fn] generates a pattern and an action for
+    options of the form [key=<text>] and calls [fn] with the string argument
+*)
+
 val longopt_int: string -> (int -> unit) -> pattern * action
 (** [longopt_int key fn] generates a pattern and an action for
     options of the form [key=<n>] and calls [fn] with the integer argument

test/export/Makefile

@@ -13,7 +13,7 @@ endif
 COQINCLUDES += -R ./clight compcert.test.clight
 COQINCLUDES += -R ./csyntax compcert.test.csyntax
 
-CLIGHTGEN=../../clightgen
+CLIGHTGEN=../../clightgen -stdlib ../../runtime
 COQC=coqc
 
 # Regression tests in the current directory