diff --git a/configure b/configure index d67a316a38..891cbfe7df 100755 --- a/configure +++ b/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,7 +311,7 @@ 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) @@ -319,7 +319,7 @@ 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__ '-D__attribute__(x)=' -E" + cprepro_options="-m32 -U__GNUC__ '-D__attribute__(x)=' -E" system="cygwin" ;; linux) @@ -327,7 +327,7 @@ 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="linux" ;; *) @@ -348,7 +348,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__ -E" + cprepro_options="-m64 -U__GNUC__ -U__SIZEOF_INT128__ -E" system="bsd" ;; linux) @@ -356,7 +356,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__ -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" ;; diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli index 1210353f81..118a1bbc83 100644 --- a/cparser/Diagnostics.mli +++ b/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 *) + diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml index 9f99f08c2e..cfe9a6d438 100644 --- a/debug/DebugInit.ml +++ b/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 Control generation of debugging information - (=0: none, =1: only-globals, =2: globals + locals - without locations, =3: full;) + (=0: none, =1: only globals, + =2: globals + locals without locations, =3: full) |} ^ (if Configuration.gnu_toolchain then gnu_debugging_help else "") diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 25c3e1dd61..8fbda7380e 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 9da1e5339f..2a3bd740f5 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- to turn off -f) : + -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 6133291e39..56e7726a50 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" ] diff --git a/lib/Commandline.ml b/lib/Commandline.ml index 2f0d7cc1db..3030eab590 100644 --- a/lib/Commandline.ml +++ b/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)) diff --git a/lib/Commandline.mli b/lib/Commandline.mli index cb9a7513f6..350a48ea6a 100644 --- a/lib/Commandline.mli +++ b/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=] 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=] and calls [fn] with the integer argument diff --git a/test/export/Makefile b/test/export/Makefile index d1228bf9c1..5cad730dc8 100644 --- a/test/export/Makefile +++ b/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