diff options
Diffstat (limited to 'debug/Debug.mli')
| -rw-r--r-- | debug/Debug.mli | 88 |
1 files changed, 88 insertions, 0 deletions
diff --git a/debug/Debug.mli b/debug/Debug.mli new file mode 100644 index 00000000..577b0ef8 --- /dev/null +++ b/debug/Debug.mli @@ -0,0 +1,88 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +open AST +open C +open Camlcoq +open DwarfTypes +open BinNums + + +(* Record used for stroring references to the actual implementation functions *) +type implem = + { + mutable init: string -> unit; + mutable atom_function: ident -> atom -> unit; + mutable atom_global_variable: ident -> atom -> unit; + mutable set_composite_size: ident -> struct_or_union -> int option -> unit; + mutable set_member_offset: ident -> string -> int -> unit; + mutable set_bitfield_offset: ident -> string -> int -> string -> int -> unit; + mutable insert_global_declaration: Env.t -> globdecl -> unit; + mutable add_fun_addr: atom -> (int * int) -> unit; + mutable generate_debug_info: (atom -> string) -> string -> debug_entries option; + mutable all_files_iter: (string -> unit) -> unit; + mutable insert_local_declaration: storage -> ident -> typ -> location -> unit; + mutable atom_local_variable: ident -> atom -> unit; + mutable enter_scope: int -> int -> int -> unit; + mutable enter_function_scope: int -> int -> unit; + mutable add_lvar_scope: int -> ident -> int -> unit; + mutable open_scope: atom -> int -> positive -> unit; + mutable close_scope: atom -> int -> positive -> unit; + mutable start_live_range: (atom * atom) -> positive -> int * int builtin_arg -> unit; + mutable end_live_range: (atom * atom) -> positive -> unit; + mutable stack_variable: (atom * atom) -> int * int builtin_arg -> unit; + mutable function_end: atom -> positive -> unit; + mutable add_label: atom -> positive -> int -> unit; + mutable atom_parameter: ident -> ident -> atom -> unit; + mutable add_compilation_section_start: string -> int -> unit; + mutable add_compilation_section_end: string -> int -> unit; + mutable compute_diab_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit; + mutable compute_gnu_file_enum: (string -> unit) -> unit; + mutable exists_section: string -> bool; + mutable remove_unused: ident -> unit; + mutable variable_printed: string -> unit; + mutable add_diab_info: string -> (int * int * string) -> unit; + } + +val implem: implem + +val init_compile_unit: string -> unit +val atom_function: ident -> atom -> unit +val atom_global_variable: ident -> atom -> unit +val set_composite_size: ident -> struct_or_union -> int option -> unit +val set_member_offset: ident -> string -> int -> unit +val set_bitfield_offset: ident -> string -> int -> string -> int -> unit +val insert_global_declaration: Env.t -> globdecl -> unit +val add_fun_addr: atom -> (int * int) -> unit +val all_files_iter: (string -> unit) -> unit +val insert_local_declaration: storage -> ident -> typ -> location -> unit +val atom_local_variable: ident -> atom -> unit +val enter_scope: int -> int -> int -> unit +val enter_function_scope: int -> int -> unit +val add_lvar_scope: int -> ident -> int -> unit +val open_scope: atom -> int -> positive -> unit +val close_scope: atom -> int -> positive -> unit +val start_live_range: (atom * atom) -> positive -> (int * int builtin_arg) -> unit +val end_live_range: (atom * atom) -> positive -> unit +val stack_variable: (atom * atom) -> int * int builtin_arg -> unit +val function_end: atom -> positive -> 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 compute_gnu_file_enum: (string -> unit) -> unit +val exists_section: string -> bool +val remove_unused: ident -> unit +val variable_printed: string -> unit +val add_diab_info: string -> (int * int * string) -> unit |