diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-06 16:49:13 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-06 16:49:13 +0100 |
commit | 6ce117058fd38c764176ad070285db6b6a2511e4 (patch) | |
tree | fa680d60d367736365a1dff6ddf6de0144dc53a9 /debug/DebugInit.ml | |
parent | 9d4bb7ec914566b3920cca3c6823515448fb65c1 (diff) | |
download | compcert-6ce117058fd38c764176ad070285db6b6a2511e4.tar.gz compcert-6ce117058fd38c764176ad070285db6b6a2511e4.zip |
Simplified DebugInformation interface.
Instead of exporting and setting all functions we just fill the
struct already in DebugInformation with the correct functions.
Diffstat (limited to 'debug/DebugInit.ml')
-rw-r--r-- | debug/DebugInit.ml | 35 |
1 files changed, 2 insertions, 33 deletions
diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml index 94a8cf02..f35d7128 100644 --- a/debug/DebugInit.ml +++ b/debug/DebugInit.ml @@ -15,47 +15,16 @@ open Commandline open Debug open Driveraux -let default_debug = - { - init = DebugInformation.init; - atom_global = DebugInformation.atom_global; - set_composite_size = DebugInformation.set_composite_size; - set_member_offset = DebugInformation.set_member_offset; - set_bitfield_offset = DebugInformation.set_bitfield_offset; - insert_global_declaration = DebugInformation.insert_global_declaration; - add_fun_addr = (fun _ _ _ -> ()); - generate_debug_info = (fun _ _ -> None); - all_files_iter = DebugInformation.all_files_iter; - insert_local_declaration = DebugInformation.insert_local_declaration; - atom_local_variable = DebugInformation.atom_local_variable; - enter_scope = DebugInformation.enter_scope; - enter_function_scope = DebugInformation.enter_function_scope; - add_lvar_scope = DebugInformation.add_lvar_scope; - open_scope = DebugInformation.open_scope; - close_scope = DebugInformation.close_scope; - start_live_range = DebugInformation.start_live_range; - end_live_range = DebugInformation.end_live_range; - stack_variable = DebugInformation.stack_variable; - add_label = DebugInformation.add_label; - atom_parameter = DebugInformation.atom_parameter; - compute_diab_file_enum = DebugInformation.compute_diab_file_enum; - compute_gnu_file_enum = DebugInformation.compute_gnu_file_enum; - exists_section = DebugInformation.exists_section; - remove_unused = DebugInformation.remove_unused; - remove_unused_function = DebugInformation.remove_unused_function; - variable_printed = DebugInformation.variable_printed; - add_diab_info = (fun _ _ _ _ -> ()); - } let init_debug () = implem := if Configuration.system = "diab" then let gen = (fun a b -> Some (Dwarfgen.gen_diab_debug_info a b)) in - {default_debug with generate_debug_info = gen; + {DebugInformation.default_debug with generate_debug_info = gen; add_diab_info = DebugInformation.add_diab_info; add_fun_addr = DebugInformation.diab_add_fun_addr;} else - {default_debug with generate_debug_info = (fun a b -> Some (Dwarfgen.gen_gnu_debug_info a b)); + {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 () = |