diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-13 15:39:07 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-13 15:39:07 +0100 |
| commit | 5c0c02e51a76183eb43b5ed80d925f3c2ce88dfb (patch) | |
| tree | 13266f8767648ee5433f30b16ec503144c67d003 /debug | |
| parent | 236d8a48288ea5845466408cf9d0be2ccd68f9a8 (diff) | |
| download | compcert-kvx-5c0c02e51a76183eb43b5ed80d925f3c2ce88dfb.tar.gz compcert-kvx-5c0c02e51a76183eb43b5ed80d925f3c2ce88dfb.zip | |
Introduced configuration variable for gnu systems.
The variable gnu_toolchain is true if a gnu toolchain is used and
false in all other cases. The variable avoids the explicit test
whether the system string is diab and should be easier to change.
Bug 20521.
Diffstat (limited to 'debug')
| -rw-r--r-- | debug/DebugInit.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml index f35d7128..9f99f08c 100644 --- a/debug/DebugInit.ml +++ b/debug/DebugInit.ml @@ -13,19 +13,18 @@ open Clflags open Commandline open Debug -open Driveraux let init_debug () = implem := - if Configuration.system = "diab" then + if Configuration.gnu_toolchain then + {DebugInformation.default_debug with generate_debug_info = (fun a b -> Some (Dwarfgen.gen_gnu_debug_info a b)); + add_fun_addr = DebugInformation.gnu_add_fun_addr} + else let gen = (fun a b -> Some (Dwarfgen.gen_diab_debug_info a b)) in {DebugInformation.default_debug with generate_debug_info = gen; add_diab_info = DebugInformation.add_diab_info; add_fun_addr = DebugInformation.diab_add_fun_addr;} - else - {DebugInformation.default_debug with generate_debug_info = (fun a b -> Some (Dwarfgen.gen_gnu_debug_info a b)); - add_fun_addr = DebugInformation.gnu_add_fun_addr} let init_none () = implem := default_implem @@ -46,7 +45,7 @@ let debugging_help = (<n>=0: none, <n>=1: only-globals, <n>=2: globals + locals without locations, <n>=3: full;) |} -^ (if gnu_system then gnu_debugging_help else "") +^ (if Configuration.gnu_toolchain then gnu_debugging_help else "") let gnu_debugging_actions = let version version () = @@ -67,4 +66,4 @@ let debugging_actions = Exact "-g2", Unit (depth 2); Exact "-g3", Unit (depth 3);] @ - (if gnu_system then gnu_debugging_actions else []) + (if Configuration.gnu_toolchain then gnu_debugging_actions else []) |