diff options
| -rw-r--r-- | debug/DebugInit.ml | 38 | ||||
| -rw-r--r-- | driver/Clflags.ml | 2 | ||||
| -rw-r--r-- | driver/Driver.ml | 33 |
3 files changed, 42 insertions, 31 deletions
diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml index b3fedb00..ed22f7c2 100644 --- a/debug/DebugInit.ml +++ b/debug/DebugInit.ml @@ -10,7 +10,10 @@ (* *) (* *********************************************************************) +open Clflags +open Commandline open Debug +open Driveraux let default_debug = { @@ -48,7 +51,6 @@ let init_debug () = implem := if Configuration.system = "diab" then let gen = (fun a b -> Some (Dwarfgen.gen_diab_debug_info a b)) in - Clflags.option_gdwarf := 2; (* Dwarf 2 is the only supported target *) {default_debug with generate_debug_info = gen; add_diab_info = DebugInformation.add_diab_info; add_fun_addr = DebugInformation.diab_add_fun_addr;} @@ -60,7 +62,39 @@ let init_none () = implem := default_implem let init () = - if !Clflags.option_g then + if !option_g then init_debug () else init_none () + +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\ +\ -g<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 "") + +let gnu_debugging_actions = + let version version () = + option_g:=true; + option_gdwarf:=version + in + [Exact "-gdwarf-2", Unit (version 2); + Exact "-gdwarf-3", Unit (version 3);] + +let debugging_actions = + let depth depth () = + option_g:=true; + option_gdepth := depth + in + [Exact "-g", Unit (depth 3); + Exact "-g0", Unset option_g; + Exact "-g1", Unit (depth 1); + Exact "-g2", Unit (depth 2); + Exact "-g3", Unit (depth 3);] + @ + (if gnu_system then gnu_debugging_actions else []) diff --git a/driver/Clflags.ml b/driver/Clflags.ml index f8c38a54..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 diff --git a/driver/Driver.ml b/driver/Driver.ml index 25d80524..739ba9b4 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -255,17 +255,6 @@ let version_string = else "The CompCert C verified compiler, version "^ Version.version ^ "\n" -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 "") - let target_help = if Configuration.arch = "arm" then "Target processor options:\n\ \ -mthumb Use Thumb2 instruction encoding\n\ @@ -302,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\ @@ -377,9 +366,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; @@ -398,20 +384,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 "-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); |