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.mli | |
| 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.mli')
| -rw-r--r-- | debug/Debug.mli | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/debug/Debug.mli b/debug/Debug.mli index 145927f4..83d5703b 100644 --- a/debug/Debug.mli +++ b/debug/Debug.mli @@ -15,6 +15,7 @@ open C open Camlcoq open DwarfTypes open BinNums +open Sections (* Record used for stroring references to the actual implementation functions *) @@ -41,14 +42,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; } val default_implem: implem @@ -76,11 +77,11 @@ val stack_variable: (atom * atom) -> int * int builtin_arg -> unit val add_label: atom -> positive -> int -> unit val generate_debug_info: (atom -> string) -> string -> debug_entries option val atom_parameter: ident -> ident -> atom -> unit -val add_compilation_section_start: string -> int -> unit -val add_compilation_section_end: string -> int -> unit -val compute_diab_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit +val add_compilation_section_start: section_name -> int -> unit +val add_compilation_section_end: section_name -> int -> unit +val compute_diab_file_enum: (section_name -> int) -> (string-> int) -> (unit -> unit) -> unit val compute_gnu_file_enum: (string -> unit) -> unit -val exists_section: string -> bool +val exists_section: section_name -> bool val remove_unused: ident -> unit val variable_printed: string -> unit -val add_diab_info: string -> (int * int * string) -> unit +val add_diab_info: section_name -> int -> int -> unit |