diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-02 00:07:04 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-02 00:07:04 +0200 |
| commit | a0bef6920c64f2d0e51d4bdce2f08c927373fb66 (patch) | |
| tree | 9bdd722b483ca10c8f0d6249cd1af82d12f69f5c /debug/DebugInit.ml | |
| parent | 2d96b7927719c3b61fe564e8ab273a1b154912a5 (diff) | |
| download | compcert-kvx-a0bef6920c64f2d0e51d4bdce2f08c927373fb66.tar.gz compcert-kvx-a0bef6920c64f2d0e51d4bdce2f08c927373fb66.zip | |
Started implementation of gnu compatible debug information.
Diffstat (limited to 'debug/DebugInit.ml')
| -rw-r--r-- | debug/DebugInit.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml index d3ce8d18..bf2c23c0 100644 --- a/debug/DebugInit.ml +++ b/debug/DebugInit.ml @@ -27,7 +27,11 @@ let init_debug () = implem.set_bitfield_offset <- DebugInformation.set_bitfield_offset; implem.insert_global_declaration <- DebugInformation.insert_global_declaration; implem.add_fun_addr <- DebugInformation.add_fun_addr; - implem.generate_debug_info <- (fun a b -> Some (Dwarfgen.gen_debug_info a b)); + implem.generate_debug_info <- + if Configuration.system = "diab" then + (fun a b -> Some (Dwarfgen.gen_diab_debug_info a b)) + else + (fun a b -> Some (Dwarfgen.gen_gnu_debug_info a b)); implem.all_files_iter <- (fun f -> DebugInformation.StringSet.iter f !DebugInformation.all_files); implem.insert_local_declaration <- DebugInformation.insert_local_declaration; implem.atom_local_variable <- DebugInformation.atom_local_variable; |