diff options
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Clflags.ml | 3 | ||||
| -rw-r--r-- | driver/Driver.ml | 41 | ||||
| -rw-r--r-- | driver/Optionsprinter.ml | 1 |
3 files changed, 9 insertions, 36 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 6a695aa4..c7a5d3bf 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -45,7 +45,7 @@ let option_dmach = ref false let option_dasm = ref false let option_sdump = ref false let option_g = ref false -let option_gdwarf = ref 2 +let option_gdwarf = ref (if Configuration.system = "diab" then 2 else 3) let option_gdepth = ref 3 let option_o = ref (None: string option) let option_E = ref false @@ -60,6 +60,5 @@ let option_small_data = then 8 else 0) let option_small_const = ref (!option_small_data) let option_timings = ref false -let option_rename_static = ref false let stdlib_path = ref Configuration.stdlib_path let use_standard_headers = ref Configuration.has_standard_headers diff --git a/driver/Driver.ml b/driver/Driver.ml index 3cc1bcad..145de6c5 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -255,20 +255,6 @@ let version_string = else "The CompCert C verified compiler, version "^ Version.version ^ "\n" -let gnu_system = Configuration.system <> "diab" - -let gnu_debugging_help = -" -gdwarf- Generate debug information in DWARF v2 or DWARF v3\n" - -let debugging_help = -"Debugging options:\n\ -\ -g Generate debugging information\n\ -\ -gdepth <n> Control generation of debugging information\n\ -\ (<n>=0: none, <n>=1: only-globals, <n>=2: globals + locals\n\ -\ without locations, <n>=3: full;)\n" -^ (if gnu_system then gnu_debugging_help else "")^ -" -frename-static Rename static functions and declarations\n" - let target_help = if Configuration.arch = "arm" then "Target processor options:\n\ \ -mthumb Use Thumb2 instruction encoding\n\ @@ -305,7 +291,7 @@ Processing options:\n\ \ -finline-asm Support inline 'asm' statements [off]\n\ \ -fall Activate all language support options above\n\ \ -fnone Turn off all language support options above\n" ^ - debugging_help ^ + DebugInit.debugging_help ^ "Optimization options: (use -fno-<opt> to turn off -f<opt>)\n\ \ -O Optimize the compiled code [on by default]\n\ \ -O0 Do not optimize the compiled code\n\ @@ -337,7 +323,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)\n\ \ -dltl Save LTL after register allocation in <file>.ltl\n\ \ -dmach Save generated Mach code in <file>.mach\n\ \ -dasm Save generated assembly in <file>.s\n\ -\ -dall Save all generated intermidate files in <file>.<ext>\n\ +\ -dall Save all generated intermediate files in <file>.<ext>\n\ \ -sdump Save info for post-linking validation in <file>.json\n\ \ -doptions Save the compiler configurations in <file>.opt.json\n\ General options:\n\ @@ -345,6 +331,8 @@ General options:\n\ \ -v Print external commands before invoking them\n\ \ -timings Show the time spent in various compiler passes\n\ \ -version Print the version string and exit\n\ +\ -target <value> Generate code for the given target\n\ +\ -conf <file> Read configuration from file\n\ \ @<file> Read command line options from <file>\n" ^ Cerrors.warning_help ^ "Interpreter mode:\n\ @@ -380,9 +368,6 @@ let num_input_files = ref 0 let cmdline_actions = let f_opt name ref = [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in - let dwarf_version version () = - option_g:=true; - option_gdwarf := version in [ (* Getting help *) Exact "-help", Unit print_usage_and_exit; @@ -401,21 +386,11 @@ let cmdline_actions = @ prepro_actions @ (* Language support options -- more below *) [ Exact "-fall", Unit (set_all language_support_options); - Exact "-fnone", Unit (unset_all language_support_options); -(* Debugging options *) - Exact "-g", Unit (dwarf_version 3);] @ - (if gnu_system then - [ Exact "-gdwarf-2", Unit (dwarf_version 2); - Exact "-gdwarf-3", Unit (dwarf_version 3);] - else []) @ - [ Exact "-frename-static", Set option_rename_static; - Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin - option_g := false - end else begin - option_g := true; - option_gdepth := if n > 3 then 3 else n - end); + Exact "-fnone", Unit (unset_all language_support_options);] + (* Debugging options *) + @ DebugInit.debugging_actions @ (* Code generation options -- more below *) + [ Exact "-O0", Unit (unset_all optimization_options); Exact "-O", Unit (set_all optimization_options); _Regexp "-O[123]$", Unit (set_all optimization_options); diff --git a/driver/Optionsprinter.ml b/driver/Optionsprinter.ml index 9dce8592..00b5f5ec 100644 --- a/driver/Optionsprinter.ml +++ b/driver/Optionsprinter.ml @@ -64,7 +64,6 @@ let print_clflags oc = p_jmember oc "small_data" p_jint !option_small_data; p_jmember oc "small_data" p_jint !option_small_const; p_jmember oc "timings" p_jbool !option_timings; - p_jmember oc "rename_static" p_jbool !option_rename_static; fprintf oc "\n}" let print_struct_passing_style oc = function |