diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-14 10:10:19 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-14 15:45:54 +0200 |
commit | ccfc5ced6a09ce2c8a1ebce81050c328c17c9bec (patch) | |
tree | 3412177948c85f853aef3996bebedc83c8100309 /debug/Debug.ml | |
parent | f5bb397acd12292f6b41438778f2df7391d6f2fe (diff) | |
download | compcert-kvx-ccfc5ced6a09ce2c8a1ebce81050c328c17c9bec.tar.gz compcert-kvx-ccfc5ced6a09ce2c8a1ebce81050c328c17c9bec.zip |
Reworked the section interface for the debug information.
Instead of pushing strings around use the actual section. However
the string is still used in the Hashtbl.
Bug 17392.
Diffstat (limited to 'debug/Debug.ml')
-rw-r--r-- | debug/Debug.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/debug/Debug.ml b/debug/Debug.ml index 806ebb08..14176d3b 100644 --- a/debug/Debug.ml +++ b/debug/Debug.ml @@ -16,6 +16,7 @@ open C open Camlcoq open Dwarfgen open DwarfTypes +open Sections (* Interface for generating and printing debug information *) @@ -43,14 +44,14 @@ type implem = stack_variable: (atom * atom) -> int * int builtin_arg -> unit; add_label: atom -> positive -> int -> unit; atom_parameter: ident -> ident -> atom -> unit; - add_compilation_section_start: string -> int -> unit; - add_compilation_section_end: string -> int -> unit; - compute_diab_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit; + add_compilation_section_start: section_name -> int -> unit; + add_compilation_section_end: section_name -> int -> unit; + compute_diab_file_enum: (section_name -> int) -> (string-> int) -> (unit -> unit) -> unit; compute_gnu_file_enum: (string -> unit) -> unit; - exists_section: string -> bool; + exists_section: section_name -> bool; remove_unused: ident -> unit; variable_printed: string -> unit; - add_diab_info: string -> (int * int * string) -> unit; + add_diab_info: section_name -> int -> int -> unit; } let default_implem = @@ -83,7 +84,7 @@ let default_implem = exists_section = (fun _ -> true); remove_unused = (fun _ -> ()); variable_printed = (fun _ -> ()); - add_diab_info = (fun _ _ -> ()); + add_diab_info = (fun _ _ _ -> ()); } let implem = ref default_implem |