diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-02-15 11:46:17 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-02-15 11:46:17 +0100 |
commit | 1aee802bf438fff7a83dec4607cabefdc398c3de (patch) | |
tree | e8e341b656c5e8ea6f61226878ad5dd1ee0e5082 /debug | |
parent | 53479577c06db853f48cf9927b5039507436be45 (diff) | |
parent | 5c0c02e51a76183eb43b5ed80d925f3c2ce88dfb (diff) | |
download | compcert-1aee802bf438fff7a83dec4607cabefdc398c3de.tar.gz compcert-1aee802bf438fff7a83dec4607cabefdc398c3de.zip |
Merge pull request #167 from AbsInt/pipe_prerequisite
Introduced configuration variable for gnu systems.
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 []) |