package linksem

  1. Overview
  2. Docs
A formalisation of the core ELF and DWARF file formats written in Lem

Install 

dune-project
 Dependency

github.com Edit opam file Versions (2)

Authors

  1. S
    Stephen Kell
  2. D
    Dominic Mulligan
  3. P
    Peter Sewell

Maintainers

  1. L
    Linksem Devs <cl-linksem-dev@lists.cam.ac.uk>

Sources

0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2

doc/linksem_zarith/Dwarf/index.html

Module DwarfSource

***************** experimental DWARF reading ***********

debug

Sourceval my_debug : 'a -> unit
Sourceval my_debug2 : 'a -> unit
Sourceval my_debug3 : 'a -> unit
Sourceval my_debug4 : string -> unit
Sourceval my_debug5 : string -> unit

************************************************************

** dwarf representation types ****************************

************************************************************

Sourcetype dwarf_attribute_classes =
  1. | DWA_7_5_3
  2. | DWA_address
  3. | DWA_block
  4. | DWA_constant
  5. | DWA_dash
  6. | DWA_exprloc
  7. | DWA_flag
  8. | DWA_lineptr
  9. | DWA_loclistptr
  10. | DWA_macptr
  11. | DWA_rangelistptr
  12. | DWA_reference
  13. | DWA_string
Sourcetype operation_argument_type =
  1. | OAT_addr
  2. | OAT_dwarf_format_t
  3. | OAT_uint8
  4. | OAT_uint16
  5. | OAT_uint32
  6. | OAT_uint64
  7. | OAT_sint8
  8. | OAT_sint16
  9. | OAT_sint32
  10. | OAT_sint64
  11. | OAT_ULEB128
  12. | OAT_SLEB128
  13. | OAT_block
Sourcetype operation_argument_value =
  1. | OAV_natural of Nat_big_num.num
  2. | OAV_integer of Nat_big_num.num
  3. | OAV_block of Nat_big_num.num * Byte_sequence.byte_sequence0
Sourcetype operation_stack = Nat_big_num.num list
Sourcetype arithmetic_context = {
  1. ac_bitwidth : Nat_big_num.num;
  2. ac_half : Nat_big_num.num;
  3. ac_all : Nat_big_num.num;
  4. ac_max : Nat_big_num.num;
}
Sourcetype operation_semantics =
  1. | OpSem_lit
  2. | OpSem_deref
  3. | OpSem_stack of arithmetic_context -> operation_stack -> operation_argument_value list -> operation_stack option
  4. | OpSem_not_supported
  5. | OpSem_binary of arithmetic_context -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num option
  6. | OpSem_unary of arithmetic_context -> Nat_big_num.num -> Nat_big_num.num option
  7. | OpSem_opcode_lit of Nat_big_num.num
  8. | OpSem_reg
  9. | OpSem_breg
  10. | OpSem_bregx
  11. | OpSem_fbreg
  12. | OpSem_deref_size
  13. | OpSem_nop
  14. | OpSem_piece
  15. | OpSem_bit_piece
  16. | OpSem_implicit_value
  17. | OpSem_stack_value
  18. | OpSem_call_frame_cfa
Sourcetype operation = {
  1. op_code : Nat_big_num.num;
  2. op_string : string;
  3. op_argument_values : operation_argument_value list;
  4. op_semantics : operation_semantics;
}
Sourcetype simple_location =
  1. | SL_memory_address of Nat_big_num.num
  2. | SL_register of Nat_big_num.num
  3. | SL_implicit of Byte_sequence.byte_sequence0
  4. | SL_empty
Sourcetype composite_location_piece =
  1. | CLP_piece of Nat_big_num.num * simple_location
  2. | CLP_bit_piece of Nat_big_num.num * Nat_big_num.num * simple_location
Sourcetype single_location =
  1. | SL_simple of simple_location
  2. | SL_composite of composite_location_piece list
Sourcetype state = {
  1. s_stack : operation_stack;
  2. s_value : simple_location;
  3. s_location_pieces : composite_location_piece list;
}
Sourcetype 'a register_read_result =
  1. | RRR_result of Nat_big_num.num
  2. | RRR_not_currently_available
  3. | RRR_bad_register_number
Sourcetype 'a memory_read_result =
  1. | MRR_result of Nat_big_num.num
  2. | MRR_not_currently_available
  3. | MRR_bad_address
Sourcetype evaluation_context = {
  1. read_register : Nat_big_num.num -> Nat_big_num.num register_read_result;
  2. read_memory : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num memory_read_result;
}
Sourcetype dwarf_format =
  1. | Dwarf32
  2. | Dwarf64
Sourcetype abbreviation_declaration = {
  1. ad_abbreviation_code : Nat_big_num.num;
  2. ad_tag : Nat_big_num.num;
  3. ad_has_children : bool;
  4. ad_attribute_specifications : (Nat_big_num.num * Nat_big_num.num) list;
}
Sourcetype abbreviations_table = {
  1. at_offset : Nat_big_num.num;
  2. at_table : abbreviation_declaration list;
}
Sourcetype attribute_value =
  1. | AV_addr of Nat_big_num.num
  2. | AV_block of Nat_big_num.num * Byte_sequence.byte_sequence0
  3. | AV_constantN of Nat_big_num.num * Byte_sequence.byte_sequence0
  4. | AV_constant_SLEB128 of Nat_big_num.num
  5. | AV_constant_ULEB128 of Nat_big_num.num
  6. | AV_exprloc of Nat_big_num.num * Byte_sequence.byte_sequence0
  7. | AV_flag of bool
  8. | AV_ref of Nat_big_num.num
  9. | AV_ref_addr of Nat_big_num.num
  10. | AV_ref_sig8 of Nat_big_num.num
  11. | AV_sec_offset of Nat_big_num.num
  12. | AV_string of Byte_sequence.byte_sequence0
  13. | AV_strp of Nat_big_num.num
Sourcetype die = {
  1. die_offset : Nat_big_num.num;
  2. die_abbreviation_code : Nat_big_num.num;
  3. die_abbreviation_declaration : abbreviation_declaration;
  4. die_attribute_values : (Nat_big_num.num * attribute_value) list;
  5. die_children : die list;
}
Sourcetype die_index = (Nat_big_num.num, die list * die) Pmap.map
Sourcetype compilation_unit_header = {
  1. cuh_offset : Nat_big_num.num;
  2. cuh_dwarf_format : dwarf_format;
  3. cuh_unit_length : Nat_big_num.num;
  4. cuh_version : Nat_big_num.num;
  5. cuh_debug_abbrev_offset : Nat_big_num.num;
  6. cuh_address_size : Nat_big_num.num;
}
Sourcetype compilation_unit = {
  1. cu_header : compilation_unit_header;
  2. cu_abbreviations_table : abbreviations_table;
  3. cu_die : die;
  4. cu_index : die_index;
}
Sourcetype compilation_units = compilation_unit list
Sourcetype type_unit_header = {
  1. tuh_cuh : compilation_unit_header;
  2. tuh_type_signature : Nat_big_num.num;
  3. tuh_type_offset : Nat_big_num.num;
}
Sourcetype type_unit = {
  1. tu_header : type_unit_header;
  2. tu_abbreviations_table : abbreviations_table;
  3. tu_die : die;
}
Sourcetype type_units = type_unit list
Sourcetype single_location_description = Byte_sequence.byte_sequence0
Sourcetype location_list_entry = {
  1. lle_beginning_address_offset : Nat_big_num.num;
  2. lle_ending_address_offset : Nat_big_num.num;
  3. lle_single_location_description : single_location_description;
}
Sourcetype base_address_selection_entry = {
  1. base_address : Nat_big_num.num;
}
Sourcetype location_list_item =
  1. | LLI_lle of location_list_entry
  2. | LLI_base of base_address_selection_entry
Sourcetype location_list = Nat_big_num.num * location_list_item list
Sourcetype location_list_list = location_list list
Sourcetype range_list_entry = {
  1. rle_beginning_address_offset : Nat_big_num.num;
  2. rle_ending_address_offset : Nat_big_num.num;
}
Sourcetype range_list_item =
  1. | RLI_rle of range_list_entry
  2. | RLI_base of base_address_selection_entry
Sourcetype range_list = Nat_big_num.num * range_list_item list
Sourcetype range_list_list = range_list list
Sourcetype cfa_address = Nat_big_num.num
Sourcetype cfa_delta = Nat_big_num.num
Sourcetype cfa_offset = Nat_big_num.num
Sourcetype cfa_register = Nat_big_num.num
Sourcetype cfa_sfoffset = Nat_big_num.num
Sourcetype call_frame_argument_type =
  1. | CFAT_address
  2. | CFAT_delta1
  3. | CFAT_delta2
  4. | CFAT_delta4
  5. | CFAT_delta_ULEB128
  6. | CFAT_offset
  7. | CFAT_sfoffset
  8. | CFAT_register
  9. | CFAT_block
Sourcetype call_frame_argument_value =
  1. | CFAV_address of cfa_address
  2. | CFAV_block of cfa_block
  3. | CFAV_delta of cfa_delta
  4. | CFAV_offset of cfa_offset
  5. | CFAV_register of cfa_register
  6. | CFAV_sfoffset of cfa_sfoffset
Sourcetype call_frame_instruction =
  1. | DW_CFA_advance_loc of cfa_delta
  2. | DW_CFA_offset of cfa_register * cfa_offset
  3. | DW_CFA_restore of cfa_register
  4. | DW_CFA_nop
  5. | DW_CFA_set_loc of cfa_address
  6. | DW_CFA_advance_loc1 of cfa_delta
  7. | DW_CFA_advance_loc2 of cfa_delta
  8. | DW_CFA_advance_loc4 of cfa_delta
  9. | DW_CFA_offset_extended of cfa_register * cfa_offset
  10. | DW_CFA_restore_extended of cfa_register
  11. | DW_CFA_undefined of cfa_register
  12. | DW_CFA_same_value of cfa_register
  13. | DW_CFA_register of cfa_register * cfa_register
  14. | DW_CFA_remember_state
  15. | DW_CFA_restore_state
  16. | DW_CFA_def_cfa of cfa_register * cfa_offset
  17. | DW_CFA_def_cfa_register of cfa_register
  18. | DW_CFA_def_cfa_offset of cfa_offset
  19. | DW_CFA_def_cfa_expression of cfa_block
  20. | DW_CFA_expression of cfa_register * cfa_block
  21. | DW_CFA_offset_extended_sf of cfa_register * cfa_sfoffset
  22. | DW_CFA_def_cfa_sf of cfa_register * cfa_sfoffset
  23. | DW_CFA_def_cfa_offset_sf of cfa_sfoffset
  24. | DW_CFA_val_offset of cfa_register * cfa_offset
  25. | DW_CFA_val_offset_sf of cfa_register * cfa_sfoffset
  26. | DW_CFA_val_expression of cfa_register * cfa_block
  27. | DW_CFA_AARCH64_negate_ra_state
  28. | DW_CFA_unknown of char
Sourcetype cie = {
  1. cie_offset : Nat_big_num.num;
  2. cie_length : Nat_big_num.num;
  3. cie_id : Nat_big_num.num;
  4. cie_version : Nat_big_num.num;
  5. cie_augmentation : Byte_sequence.byte_sequence0;
  6. cie_address_size : Nat_big_num.num option;
  7. cie_segment_size : Nat_big_num.num option;
  8. cie_code_alignment_factor : Nat_big_num.num;
  9. cie_data_alignment_factor : Nat_big_num.num;
  10. cie_return_address_register : cfa_register;
  11. cie_initial_instructions_bytes : Byte_sequence.byte_sequence0;
  12. cie_initial_instructions : call_frame_instruction list;
}
Sourcetype fde = {
  1. fde_offset : Nat_big_num.num;
  2. fde_length : Nat_big_num.num;
  3. fde_cie_pointer : Nat_big_num.num;
  4. fde_initial_location_segment_selector : Nat_big_num.num option;
  5. fde_initial_location_address : Nat_big_num.num;
  6. fde_address_range : Nat_big_num.num;
  7. fde_instructions_bytes : Byte_sequence.byte_sequence0;
  8. fde_instructions : call_frame_instruction list;
}
Sourcetype frame_info_element =
  1. | FIE_cie of cie
  2. | FIE_fde of fde
Sourcetype frame_info = frame_info_element list
Sourcetype cfa_rule =
  1. | CR_undefined
  2. | CR_register of cfa_register * Nat_big_num.num
  3. | CR_expression of single_location_description
Sourcetype register_rule =
  1. | RR_undefined
  2. | RR_same_value
  3. | RR_offset of Nat_big_num.num
  4. | RR_val_offset of Nat_big_num.num
  5. | RR_register of Nat_big_num.num
  6. | RR_expression of single_location_description
  7. | RR_val_expression of single_location_description
  8. | RR_architectural
Sourcetype register_rule_map = (cfa_register * register_rule) list
Sourcetype cfa_table_row = {
  1. ctr_loc : Nat_big_num.num;
  2. ctr_cfa : cfa_rule;
  3. ctr_regs : register_rule_map;
}
Sourcetype cfa_state = {
  1. cs_current_row : cfa_table_row;
  2. cs_previous_rows : cfa_table_row list;
  3. cs_initial_instructions_row : cfa_table_row;
  4. cs_row_stack : cfa_table_row list;
}
Sourcetype evaluated_frame_info = (fde * cfa_table_row list) list
Sourcetype line_number_argument_type =
  1. | LNAT_address
  2. | LNAT_ULEB128
  3. | LNAT_SLEB128
  4. | LNAT_uint16
  5. | LNAT_string
Sourcetype line_number_argument_value =
  1. | LNAV_address of Nat_big_num.num
  2. | LNAV_ULEB128 of Nat_big_num.num
  3. | LNAV_SLEB128 of Nat_big_num.num
  4. | LNAV_uint16 of Nat_big_num.num
  5. | LNAV_string of Byte_sequence.byte_sequence0
Sourcetype line_number_operation =
  1. | DW_LNS_copy
  2. | DW_LNS_advance_pc of Nat_big_num.num
  3. | DW_LNS_advance_line of Nat_big_num.num
  4. | DW_LNS_set_file of Nat_big_num.num
  5. | DW_LNS_set_column of Nat_big_num.num
  6. | DW_LNS_negate_stmt
  7. | DW_LNS_set_basic_block
  8. | DW_LNS_const_add_pc
  9. | DW_LNS_fixed_advance_pc of Nat_big_num.num
  10. | DW_LNS_set_prologue_end
  11. | DW_LNS_set_epilogue_begin
  12. | DW_LNS_set_isa of Nat_big_num.num
  13. | DW_LNE_end_sequence
  14. | DW_LNE_set_address of Nat_big_num.num
  15. | DW_LNE_define_file of Byte_sequence.byte_sequence0 * Nat_big_num.num * Nat_big_num.num * Nat_big_num.num
  16. | DW_LNE_set_discriminator of Nat_big_num.num
  17. | DW_LN_special of Nat_big_num.num
Sourcetype line_number_file_entry = {
  1. lnfe_path : Byte_sequence.byte_sequence0;
  2. lnfe_directory_index : Nat_big_num.num;
  3. lnfe_last_modification : Nat_big_num.num;
  4. lnfe_length : Nat_big_num.num;
}
Sourcetype line_number_header = {
  1. lnh_offset : Nat_big_num.num;
  2. lnh_dwarf_format : dwarf_format;
  3. lnh_unit_length : Nat_big_num.num;
  4. lnh_version : Nat_big_num.num;
  5. lnh_header_length : Nat_big_num.num;
  6. lnh_minimum_instruction_length : Nat_big_num.num;
  7. lnh_maximum_operations_per_instruction : Nat_big_num.num;
  8. lnh_default_is_stmt : bool;
  9. lnh_line_base : Nat_big_num.num;
  10. lnh_line_range : Nat_big_num.num;
  11. lnh_opcode_base : Nat_big_num.num;
  12. lnh_standard_opcode_lengths : Nat_big_num.num list;
  13. lnh_include_directories : Byte_sequence.byte_sequence0 list;
  14. lnh_file_entries : line_number_file_entry list;
  15. lnh_comp_dir : string option;
}
Sourcetype line_number_program = {
  1. lnp_header : line_number_header;
  2. lnp_operations : line_number_operation list;
}
Sourcetype line_number_registers = {
  1. lnr_address : Nat_big_num.num;
  2. lnr_op_index : Nat_big_num.num;
  3. lnr_file : Nat_big_num.num;
  4. lnr_line : Nat_big_num.num;
  5. lnr_column : Nat_big_num.num;
  6. lnr_is_stmt : bool;
  7. lnr_basic_block : bool;
  8. lnr_end_sequence : bool;
  9. lnr_prologue_end : bool;
  10. lnr_epilogue_begin : bool;
  11. lnr_isa : Nat_big_num.num;
  12. lnr_discriminator : Nat_big_num.num;
}
Sourcetype unpacked_file_entry = string option * string option * string
Sourcetype unpacked_decl = unpacked_file_entry * int * string
Sourcetype dwarf = {
  1. d_endianness : Endianness.endianness;
  2. d_str : Byte_sequence.byte_sequence0;
  3. d_compilation_units : compilation_units;
  4. d_type_units : type_units;
  5. d_loc : location_list_list;
  6. d_ranges : range_list_list;
  7. d_frame_info : frame_info;
  8. d_line_info : line_number_program list;
}
Sourcetype analysed_location_data = ((compilation_unit * die list * die) * (Nat_big_num.num * Nat_big_num.num * single_location_description) list option) list
Sourcetype analysed_location_data_at_pc = ((compilation_unit * die list * die) * (Nat_big_num.num * Nat_big_num.num * single_location_description * single_location Error.error)) list
Sourcetype evaluated_line_info = (line_number_header * line_number_registers list) list
Sourcetype dwarf_static = {
  1. ds_dwarf : dwarf;
  2. ds_analysed_location_data : analysed_location_data;
  3. ds_evaluated_frame_info : evaluated_frame_info;
  4. ds_evaluated_line_info : evaluated_line_info;
  5. ds_subprogram_line_extents : (unpacked_file_entry * (string * unpacked_file_entry * Nat_big_num.num) list) list;
}
Sourcetype dwarf_dynamic_at_pc = analysed_location_data_at_pc

context for parsing and pp functions

Sourcetype p_context = {
  1. endianness : Endianness.endianness;
}
Sourcetype cupdie = compilation_unit * die list * die
Sourcetype decl = {
  1. decl_file : string option;
  2. decl_line : Nat_big_num.num option;
}
Sourcetype 't array_dimension = Nat_big_num.num option * 't option
Sourcetype 't struct_union_member = cupdie * string option * 't * Nat_big_num.num option
Sourcetype struct_union_type_kind =
  1. | Atk_structure
  2. | Atk_union
Sourcetype enumeration_member = cupdie * string option * Nat_big_num.num
Sourcetype 't c_type_top =
  1. | CT_missing of cupdie
  2. | CT_base of cupdie * string * Nat_big_num.num * Nat_big_num.num option
  3. | CT_pointer of cupdie * 't option
  4. | CT_const of cupdie * 't option
  5. | CT_volatile of cupdie * 't
  6. | CT_restrict of cupdie * 't
  7. | CT_typedef of cupdie * string * 't * decl
  8. | CT_array of cupdie * 't * 't array_dimension list
  9. | CT_struct_union of cupdie * struct_union_type_kind * string option * Nat_big_num.num option * decl * 't struct_union_member list option
  10. | CT_enumeration of cupdie * string option * 't option * Nat_big_num.num option * decl * enumeration_member list option
  11. | CT_subroutine of cupdie * bool * 't option * 't list * bool
Sourcetype c_type =
  1. | CT of c_type c_type_top
Sourcetype variable_or_formal_parameter_kind =
  1. | SVPK_var
  2. | SVPK_param
Sourcetype sdt_unspecified_parameter = unit
Sourcetype sdt_variable_or_formal_parameter = {
  1. svfp_cupdie : cupdie;
  2. svfp_name : string;
  3. svfp_kind : variable_or_formal_parameter_kind;
  4. svfp_type : c_type option;
  5. svfp_abstract_origin : sdt_variable_or_formal_parameter option;
  6. svfp_const_value : Nat_big_num.num option;
  7. svfp_external : bool;
  8. svfp_declaration : bool;
  9. svfp_locations : (Nat_big_num.num * Nat_big_num.num * operation list) list option;
  10. svfp_decl : unpacked_decl option;
}
Sourcetype sdt_subroutine_kind =
  1. | SSK_subprogram
  2. | SSK_inlined_subroutine
Sourcetype sdt_subroutine = {
  1. ss_cupdie : cupdie;
  2. ss_name : string option;
  3. ss_kind : sdt_subroutine_kind;
  4. ss_call_site : unpacked_decl option;
  5. ss_abstract_origin : sdt_subroutine option;
  6. ss_type : c_type option;
  7. ss_vars : sdt_variable_or_formal_parameter list;
  8. ss_pc_ranges : (Nat_big_num.num * Nat_big_num.num) list option;
  9. ss_entry_address : Nat_big_num.num option;
  10. ss_unspecified_parameters : sdt_unspecified_parameter list;
  11. ss_subroutines : sdt_subroutine list;
  12. ss_lexical_blocks : sdt_lexical_block list;
  13. ss_decl : unpacked_decl option;
  14. ss_noreturn : bool;
  15. ss_external : bool;
}
Sourceand sdt_lexical_block = {
  1. slb_cupdie : cupdie;
  2. slb_vars : sdt_variable_or_formal_parameter list;
  3. slb_pc_ranges : (Nat_big_num.num * Nat_big_num.num) list option;
  4. slb_subroutines : sdt_subroutine list;
  5. slb_lexical_blocks : sdt_lexical_block list;
}
Sourcetype sdt_compilation_unit = {
  1. scu_cupdie : cupdie;
  2. scu_name : string;
  3. scu_subroutines : sdt_subroutine list;
  4. scu_vars : sdt_variable_or_formal_parameter list;
  5. scu_pc_ranges : (Nat_big_num.num * Nat_big_num.num) list option;
}
Sourcetype sdt_dwarf = {
  1. sd_compilation_units : sdt_compilation_unit list;
}
Sourcetype inlined_subroutine_const_param = {
  1. iscp_abstract_origin : compilation_unit * die list * die;
  2. iscp_value : Nat_big_num.num;
}
Sourcetype inlined_subroutine = {
  1. is_inlined_subroutine : compilation_unit * die list * die;
  2. is_abstract_origin : compilation_unit * die list * die;
  3. is_inlined_subroutine_sdt : sdt_subroutine;
  4. is_inlined_subroutine_sdt_parents : sdt_subroutine list;
  5. is_name : string;
  6. is_call_file : unpacked_file_entry;
  7. is_call_line : Nat_big_num.num;
  8. is_pc_ranges : (Nat_big_num.num * Nat_big_num.num) list;
  9. is_const_params : inlined_subroutine_const_param list;
}
Sourcetype inlined_subroutine_data = inlined_subroutine list
Sourcetype inlined_subroutine_data_by_range_entry = (Nat_big_num.num * Nat_big_num.num) * (Nat_big_num.num * Nat_big_num.num) * inlined_subroutine
Sourcetype inlined_subroutine_data_by_range = inlined_subroutine_data_by_range_entry list

************************************************************

** missing pervasives ************************************

************************************************************

Sourceval index_natural : 'a list -> Nat_big_num.num -> 'a option
Sourceval partialNaturalFromInteger : Nat_big_num.num -> Nat_big_num.num

************************************************************

** endianness ***************************************

************************************************************

Sourceval p_context_of_d : dwarf -> p_context

************************************************************

** dwarf encodings ***************************************

************************************************************

Sourceval tag_encodings : (string * Nat_big_num.num) list
Sourceval vDW_CHILDREN_no : Nat_big_num.num
Sourceval vDW_CHILDREN_yes : Nat_big_num.num
Sourceval attribute_encodings : (string * Nat_big_num.num * dwarf_attribute_classes list) list
Sourceval attribute_form_encodings : (string * Nat_big_num.num * dwarf_attribute_classes list) list
Sourceval operation_encodings : (string * Nat_big_num.num * operation_argument_type list * operation_semantics) list
Sourceval vDW_OP_reg0 : Nat_big_num.num
Sourceval vDW_OP_breg0 : Nat_big_num.num
Sourceval call_frame_instruction_encoding : (string * Nat_big_num.num * Nat_big_num.num * call_frame_argument_type list * (call_frame_argument_value list -> call_frame_instruction option)) list
Sourceval line_number_standard_encodings : (string * Nat_big_num.num * line_number_argument_type list * (line_number_argument_value list -> line_number_operation option)) list
Sourceval line_number_extended_encodings : (string * Nat_big_num.num * line_number_argument_type list * (line_number_argument_value list -> line_number_operation option)) list
Sourceval base_type_attribute_encodings : (string * Nat_big_num.num) list

************************************************************

** more missing pervasives and bits ***********************

************************************************************

Sourceval myconcat : string -> string list -> string
Sourceval myhead : 'a list -> 'a
Sourceval myfindNonPure : ('a -> bool) -> 'a list -> 'a
Sourceval myfindmaybe : ('a -> 'b option) -> 'a list -> 'b option
Sourceval myfind : ('a -> bool) -> 'a list -> 'a option
Sourceval myfiltermaybe : ('a -> 'b option) -> 'a list -> 'b list
Sourceval bytes_of_natural : Endianness.endianness -> Nat_big_num.num -> Nat_big_num.num -> Byte_sequence_wrapper.byte_sequence
Sourceval natural_of_bytes_little : Byte_sequence_wrapper.byte_sequence -> Nat_big_num.num
Sourceval natural_of_bytes_big : Nat_big_num.num -> Byte_sequence_wrapper.byte_sequence -> Nat_big_num.num
Sourceval natural_of_bytes : Endianness.endianness -> Byte_sequence_wrapper.byte_sequence -> Nat_big_num.num
Sourceval bigunionListMap : 'b Lem_basic_classes.setType_class -> ('a -> 'b Pset.set) -> 'a list -> 'b Pset.set
Sourceval mytake' : Nat_big_num.num -> 'a list -> 'a list -> ('a list * 'a list) option
Sourceval mytake : Nat_big_num.num -> 'a list -> ('a list * 'a list) option
Sourceval mynth : Nat_big_num.num -> 'a list -> 'a option

basic pretty printing

Sourceval pphexplain : Nat_big_num.num -> string
Sourceval pphex : Nat_big_num.num -> string
Sourceval pphex_integer : Nat_big_num.num -> string
Sourceval ppbytes2 : Nat_big_num.num -> Byte_sequence_wrapper.byte_sequence -> string
Sourceval ppbytesplain : p_context -> Nat_big_num.num -> Byte_sequence_wrapper.byte_sequence -> string
Sourceval string_of_bytes : char list -> string
Sourceval just_one : string -> 'a list -> 'a
Sourceval max_address : Nat_big_num.num -> Nat_big_num.num

lookup of encodings

Sourceval lookup_Ab_b : 'a Lem_basic_classes.eq_class -> 'a -> ('a * 'b) list -> 'b option
Sourceval lookup_aB_a : 'b Lem_basic_classes.eq_class -> 'b -> ('a * 'b) list -> 'a option
Sourceval lookup_aBc_a : 'b Lem_basic_classes.eq_class -> 'b -> ('a * 'b * 'c) list -> 'a option
Sourceval lookup_aBc_ac : 'b Lem_basic_classes.eq_class -> 'b -> ('a * 'b * 'c) list -> ('a * 'c) option
Sourceval lookup_Abc_b : 'a Lem_basic_classes.eq_class -> 'a -> ('a * 'b * 'c) list -> 'b option
Sourceval lookup_aBcd_a : 'b Lem_basic_classes.eq_class -> 'b -> ('a * 'b * 'c * 'd) list -> 'a option
Sourceval lookup_aBcd_acd : 'b Lem_basic_classes.eq_class -> 'b -> ('a * 'b * 'c * 'd) list -> ('a * 'c * 'd) option
Sourceval lookup_abCde_de : 'a Lem_basic_classes.eq_class -> 'a -> ('b * 'c * 'a * 'd * 'e) list -> ('d * 'e) option
Sourceval pp_maybe : (Nat_big_num.num -> string option) -> Nat_big_num.num -> string
Sourceval pp_tag_encoding : Nat_big_num.num -> string
Sourceval pp_attribute_encoding : Nat_big_num.num -> string
Sourceval pp_attribute_form_encoding : Nat_big_num.num -> string
Sourceval pp_operation_encoding : Nat_big_num.num -> string
Sourceval tag_encode : string -> Nat_big_num.num
Sourceval attribute_encode : string -> Nat_big_num.num
Sourceval attribute_form_encode : string -> Nat_big_num.num
Sourceval base_type_attribute_encode : string -> Nat_big_num.num

************************************************************

** parser combinators and primitives *********************

************************************************************

Sourcetype parse_context = {
  1. pc_bytes : Byte_sequence.byte_sequence0;
  2. pc_offset : Nat_big_num.num;
}
Sourcetype 'a parse_result =
  1. | PR_success of 'a * parse_context
  2. | PR_fail of string * parse_context
Sourcetype 'a parser = parse_context -> 'a parse_result
Sourceval pp_parse_context : parse_context -> string
Sourceval pp_parse_fail : string -> parse_context -> string
Sourceval pp_parse_result : ('a -> string) -> 'a parse_result -> string
Sourceval pr_bind : 'a parse_result -> ('a -> parse_context -> 'b parse_result) -> 'b parse_result
Sourceval pr_return : 'a -> parse_context -> 'a parse_result
Sourceval pr_map : ('a -> 'b) -> 'a parse_result -> 'b parse_result
Sourceval pr_map2 : ('a -> 'b) -> (parse_context -> 'a parse_result) -> parse_context -> 'b parse_result
Sourceval pr_post_map1 : 'a parse_result -> ('a -> 'b) -> 'b parse_result
Sourceval pr_post_map : (parse_context -> 'a parse_result) -> ('a -> 'b) -> parse_context -> 'b parse_result
Sourceval pr_with_pos : (parse_context -> 'a parse_result) -> parse_context -> (Nat_big_num.num * 'a) parse_result
Sourceval parse_pair : (parse_context -> 'a parse_result) -> (parse_context -> 'b parse_result) -> parse_context -> ('a * 'b) parse_result
Sourceval parse_triple : (parse_context -> 'a parse_result) -> (parse_context -> 'b parse_result) -> (parse_context -> 'c parse_result) -> parse_context -> ('a * ('b * 'c)) parse_result
Sourceval parse_quadruple : (parse_context -> 'a parse_result) -> (parse_context -> 'b parse_result) -> (parse_context -> 'c parse_result) -> (parse_context -> 'd parse_result) -> parse_context -> ('a * ('b * ('c * 'd))) parse_result
Sourceval parse_pentuple : (parse_context -> 'a parse_result) -> (parse_context -> 'b parse_result) -> (parse_context -> 'c parse_result) -> (parse_context -> 'd parse_result) -> (parse_context -> 'e parse_result) -> parse_context -> ('a * ('b * ('c * ('d * 'e)))) parse_result
Sourceval parse_sextuple : (parse_context -> 'a parse_result) -> (parse_context -> 'b parse_result) -> (parse_context -> 'c parse_result) -> (parse_context -> 'd parse_result) -> (parse_context -> 'e parse_result) -> (parse_context -> 'f parse_result) -> parse_context -> ('a * ('b * ('c * ('d * ('e * 'f))))) parse_result
Sourceval parse_dependent_pair : (parse_context -> 'a parse_result) -> ('a -> parse_context -> 'b parse_result) -> parse_context -> ('a * 'b) parse_result
Sourceval parse_dependent : (parse_context -> 'a parse_result) -> ('a -> parse_context -> 'b parse_result) -> parse_context -> 'b parse_result
Sourceval parse_list' : (parse_context -> 'a option parse_result) -> 'a list -> parse_context -> 'a list parse_result
Sourceval parse_list : (parse_context -> 'a option parse_result) -> parse_context -> 'a list parse_result
Sourceval parse_parser_list : (parse_context -> 'a parse_result) list -> parse_context -> 'a list parse_result
Sourceval parse_maybe : (parse_context -> 'a parse_result) -> parse_context -> 'a option parse_result
Sourceval parse_demaybe : string -> (parse_context -> 'a option parse_result) -> parse_context -> 'a parse_result
Sourceval parse_restrict_length : Nat_big_num.num -> (parse_context -> 'a parse_result) -> parse_context -> 'a parse_result
Sourceval parse_byte : char parser
Sourceval parse_n_bytes : Nat_big_num.num -> Byte_sequence.byte_sequence0 parser
Sourceval bzero : char
Sourceval parse_non_empty_string : Byte_sequence.byte_sequence0 option parser
Sourceval parse_uint8 : Nat_big_num.num parser
Sourceval parse_uint8_constant : Nat_big_num.num -> Nat_big_num.num parser
Sourceval parse_uint16 : p_context -> Nat_big_num.num parser
Sourceval parse_uint32 : p_context -> Nat_big_num.num parser
Sourceval parse_uint64 : p_context -> Nat_big_num.num parser
Sourceval integerFromTwosComplementNatural : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
Sourceval partialTwosComplementNaturalFromInteger : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
Sourceval parse_sint8 : Nat_big_num.num parser
Sourceval parse_sint16 : p_context -> Nat_big_num.num parser
Sourceval parse_sint32 : p_context -> Nat_big_num.num parser
Sourceval parse_sint64 : p_context -> Nat_big_num.num parser
Sourceval parse_ULEB128' : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num parser
Sourceval parse_ULEB128 : Nat_big_num.num parser
Sourceval parse_SLEB128' : Nat_big_num.num -> Nat_big_num.num -> (bool * Nat_big_num.num * Nat_big_num.num) parser
Sourceval parse_SLEB128 : Nat_big_num.num parser
Sourceval parse_nonzero_ULEB128_pair : (Nat_big_num.num * Nat_big_num.num) option parser
Sourceval parse_zero_terminated_ULEB128_pair_list : (Nat_big_num.num * Nat_big_num.num) list parser
Sourceval parse_uintDwarfN : p_context -> dwarf_format -> Nat_big_num.num parser
Sourceval parse_uint_address_size : p_context -> Nat_big_num.num -> Nat_big_num.num parser
Sourceval parse_uint_segment_selector_size : p_context -> Nat_big_num.num -> Nat_big_num.num option parser

************************************************************

** parsing and pretty printing of .debug_* sections ******

************************************************************

abbreviations table: pp and parsing

Sourceval pp_abbreviation_declaration : abbreviation_declaration -> string
Sourceval pp_abbreviations_table : abbreviations_table -> string
Sourceval remove_duplicates : 'a Lem_basic_classes.eq_class -> ('a * 'b) list -> ('a * 'b) list -> ('a * 'b) list
Sourceval pp_abbreviations_tables : dwarf -> string
Sourceval parse_abbreviation_declaration : 'a -> abbreviation_declaration option parser
Sourceval parse_abbreviations_table : 'a -> parse_context -> abbreviation_declaration list parse_result

debug_str entry

Sourceval pp_debug_str_entry : Byte_sequence.byte_sequence0 -> Nat_big_num.num -> string

operations: pp and parsing

Sourceval pp_operation_argument_value : operation_argument_value -> string
Sourceval pp_operation_semantics : operation_semantics -> string
Sourceval pp_operation_semantics_brief : operation_semantics -> string
Sourceval pp_operation : operation -> string
Sourceval pp_operations : operation list -> string
Sourceval parse_and_pp_operations : p_context -> compilation_unit_header -> Byte_sequence.byte_sequence0 -> string

attribute values: pp and parsing

Sourceval pp_attribute_value_plain : attribute_value -> string
Sourceval pp_attribute_value : p_context -> compilation_unit_header -> Byte_sequence.byte_sequence0 -> Nat_big_num.num -> attribute_value -> string
Sourceval pp_attribute_value_like_objdump : p_context -> compilation_unit_header -> Byte_sequence.byte_sequence0 -> Nat_big_num.num -> attribute_value -> string
Sourceval parser_of_attribute_form_non_indirect : p_context -> compilation_unit_header -> Nat_big_num.num -> parse_context -> attribute_value parse_result
Sourceval parser_of_attribute_form : p_context -> compilation_unit_header -> Nat_big_num.num -> parse_context -> attribute_value parse_result
Sourceval pp_pos : Nat_big_num.num -> string
Sourceval pp_cupdie : (compilation_unit * 'a * die) -> string
Sourceval pp_cupdie3 : (compilation_unit * die list * die) -> string

************************************************************

** finding things in the die tree

************************************************************

Sourceval find_maybe : ('a -> 'b option) -> 'a list -> 'b option
Sourceval find_die_by_offset_in_cu : Nat_big_num.num -> compilation_unit -> cupdie option
Sourceval find_die_by_offset_in_all : Nat_big_num.num -> dwarf -> cupdie option
Sourceval find_dies_in_die : (die -> bool) -> compilation_unit -> die list -> die -> (compilation_unit * die list * die) list
Sourceval find_dies : (die -> bool) -> dwarf -> cupdie list

convert attribute values to usable Lem types

Sourceval string_of_string_attribute_value : Byte_sequence.byte_sequence0 -> attribute_value -> string
Sourceval maybe_natural_of_constant_attribute_value : 'a -> p_context -> attribute_value -> Nat_big_num.num option
Sourceval natural_of_constant_attribute_value : die -> p_context -> attribute_value -> Nat_big_num.num
Sourceval integer_of_constant_attribute_value : p_context -> attribute_value -> Nat_big_num.num
Sourceval bool_of_flag_attribute_value : attribute_value -> bool
Sourceval reference_of_reference_attribute_value : 'a -> dwarf -> compilation_unit -> 'b -> attribute_value -> (compilation_unit * die list * die) option

attribute find

Sourceval find_attribute_value : string -> die -> attribute_value option
Sourceval find_string_attribute_value_of_die : string -> Byte_sequence.byte_sequence0 -> die -> string option
Sourceval find_natural_attribute_value_of_die : p_context -> string -> die -> Nat_big_num.num option
Sourceval find_integer_attribute_value_of_die : p_context -> string -> die -> Nat_big_num.num option
Sourceval find_flag_attribute_value_of_die : string -> die -> bool option
Sourceval find_flag_attribute_value_of_die_default_false : string -> die -> bool
Sourceval find_name_of_die : Byte_sequence.byte_sequence0 -> die -> string option
Sourceval find_reference_attribute_of_die : 'a -> dwarf -> compilation_unit -> 'b -> string -> die -> (compilation_unit * die list * die) option
Sourceval find_DW_AT_type_of_die : 'a -> dwarf -> compilation_unit -> 'b -> die -> (compilation_unit * die list * die) option
Sourceval find_attribute_value_using_abstract_origin : 'a -> dwarf -> compilation_unit -> 'b -> string -> die -> (compilation_unit * attribute_value) option
Sourceval find_name_of_die_using_abstract_origin : 'a -> dwarf -> compilation_unit -> Byte_sequence.byte_sequence0 -> die -> string option
Sourceval find_name_of_die_using_abstract_origin_and_spec : 'a -> dwarf -> compilation_unit -> Byte_sequence.byte_sequence0 -> die -> (compilation_unit * 'b * die) option -> string option
Sourceval find_reference_attribute_using_abstract_origin : 'a -> dwarf -> compilation_unit -> 'b -> string -> die -> (compilation_unit * die list * die) option
Sourceval find_DW_AT_type_of_die_using_abstract_origin : 'a -> dwarf -> compilation_unit -> 'b -> die -> (compilation_unit * die list * die) option
Sourceval find_flag_attribute_value_of_die_using_abstract_origin : dwarf -> string -> cupdie -> bool option

compilation unit header: pp and parsing

Sourceval pp_dwarf_format : dwarf_format -> string
Sourceval pp_unit_header : string -> compilation_unit_header -> string
Sourceval pp_compilation_unit_header : compilation_unit_header -> string
Sourceval parse_unit_length : p_context -> (dwarf_format * Nat_big_num.num) parser
Sourceval parse_compilation_unit_header : p_context -> compilation_unit_header parser

type unit header: pp and parsing

Sourceval pp_type_unit_header : type_unit_header -> string
Sourceval parse_type_unit_header : p_context -> type_unit_header parser

debugging information entries: pp and parsing

debugging information entries: pp and parsing

Sourceval indent_level : bool -> Nat_big_num.num -> string
Sourceval indent_level_plus_one : bool -> Nat_big_num.num -> string
Sourceval pp_die_attribute : p_context -> compilation_unit_header -> Byte_sequence.byte_sequence0 -> bool -> Nat_big_num.num -> ((Nat_big_num.num * Nat_big_num.num) * (Nat_big_num.num * attribute_value)) -> string
Sourceval pp_die : p_context -> compilation_unit_header -> Byte_sequence.byte_sequence0 -> bool -> Nat_big_num.num -> bool -> die -> string
Sourceval pp_die_abbrev : 'a -> 'b -> Byte_sequence.byte_sequence0 -> Nat_big_num.num -> bool -> die list -> die -> string
Sourceval pp_die_abbrev_var : 'a -> dwarf -> compilation_unit -> Byte_sequence.byte_sequence0 -> bool -> 'b -> die -> string * string * string
Sourceval pp_die_abbrev_var_parent : 'a -> dwarf -> compilation_unit -> Byte_sequence.byte_sequence0 -> die -> string
Sourceval pp_die_abbrev_var_parents : 'a -> dwarf -> compilation_unit -> Byte_sequence.byte_sequence0 -> die list -> string
Sourceval has_attribute : string -> die -> bool

compilation units: pp and parsing

Sourceval pp_compilation_unit : p_context -> bool -> Byte_sequence.byte_sequence0 -> compilation_unit -> string
Sourceval pp_compilation_units : p_context -> bool -> Byte_sequence.byte_sequence0 -> compilation_unit list -> string
Sourceval pp_compilation_unit_abbrev : 'a -> Byte_sequence.byte_sequence0 -> compilation_unit -> string
Sourceval pp_compilation_units_abbrev : 'a -> Byte_sequence.byte_sequence0 -> compilation_unit list -> string
Sourceval add_die_to_index : die_index -> die list -> die -> die_index

type units: pp and parsing

Sourceval pp_type_unit : p_context -> Byte_sequence.byte_sequence0 -> type_unit -> string
Sourceval pp_type_units : p_context -> Byte_sequence.byte_sequence0 -> type_unit list -> string

location lists, pp and parsing

Sourceval pp_location_list_entry : p_context -> compilation_unit_header -> Nat_big_num.num -> location_list_entry -> string
Sourceval pp_base_address_selection_entry : 'a -> compilation_unit_header -> Nat_big_num.num -> base_address_selection_entry -> string
Sourceval pp_location_list_item : p_context -> compilation_unit_header -> Nat_big_num.num -> location_list_item -> string
Sourceval pp_location_list : p_context -> compilation_unit_header -> (Nat_big_num.num * location_list_item list) -> string
Sourceval pp_loc : p_context -> compilation_unit_header -> location_list list -> string
Sourceval parse_location_list_item : p_context -> compilation_unit_header -> location_list_item option parser
Sourceval parse_location_list : p_context -> compilation_unit_header -> location_list option parser
Sourceval find_location_list : location_list list -> Nat_big_num.num -> location_list
Sourceval interpret_location_list : Nat_big_num.num -> location_list_item list -> (Nat_big_num.num * Nat_big_num.num * single_location_description) list

range lists, pp and parsing

Sourceval pp_range_list_entry : 'a -> compilation_unit_header -> Nat_big_num.num -> range_list_entry -> string
Sourceval pp_range_list_item : 'a -> compilation_unit_header -> Nat_big_num.num -> range_list_item -> string
Sourceval pp_range_list : 'a -> compilation_unit_header -> (Nat_big_num.num * range_list_item list) -> string
Sourceval pp_ranges : 'a -> compilation_unit_header -> range_list list -> string
Sourceval parse_range_list_item : p_context -> compilation_unit_header -> range_list_item option parser
Sourceval expand_range_list_suffixes : compilation_unit_header -> (Nat_big_num.num * range_list_item list) -> range_list list
Sourceval parse_range_list : p_context -> compilation_unit_header -> range_list list option parser
Sourceval find_range_list : range_list list -> Nat_big_num.num -> range_list option
Sourceval interpret_range_list : Nat_big_num.num -> range_list_item list -> (Nat_big_num.num * Nat_big_num.num) list

frame information, pp and parsing

Sourceval pp_cfa_address : Nat_big_num.num -> string
Sourceval pp_cfa_block : Byte_sequence_wrapper.byte_sequence -> string
Sourceval pp_cfa_delta : Nat_big_num.num -> string
Sourceval pp_cfa_sfoffset : 'a Show.show_class -> 'a -> string
Sourceval pp_cfa_register : 'a Show.show_class -> 'a -> string
Sourceval pp_cfa_offset : Nat_big_num.num -> string
Sourceval pp_cfa_rule : cfa_rule -> string
Sourceval pp_register_rule : register_rule -> string
Sourceval pp_call_frame_instruction : call_frame_instruction -> string
Sourceval pp_call_frame_instructions : call_frame_instruction list -> string
Sourceval parse_call_frame_instruction : p_context -> compilation_unit_header -> call_frame_instruction option parser
Sourceval parse_call_frame_instructions : p_context -> compilation_unit_header -> call_frame_instruction list parser
Sourceval parse_and_pp_call_frame_instructions : p_context -> compilation_unit_header -> Byte_sequence.byte_sequence0 -> string
Sourceval pp_call_frame_instructions' : p_context -> compilation_unit_header -> Byte_sequence.byte_sequence0 -> string
Sourceval pp_cie : 'a -> 'b -> cie -> string
Sourceval pp_fde : 'a -> 'b -> fde -> string
Sourceval pp_frame_info_element : 'a -> 'b -> frame_info_element -> string
Sourceval pp_frame_info : 'a -> 'b -> frame_info_element list -> string
Sourceval find_cie : frame_info_element list -> Nat_big_num.num -> cie
Sourceval parse_initial_location : p_context -> compilation_unit_header -> Nat_big_num.num option -> Nat_big_num.num option -> (Nat_big_num.num option * Nat_big_num.num) parser
Sourceval parse_call_frame_instruction_bytes : Nat_big_num.num -> Nat_big_num.num -> parse_context -> Byte_sequence_wrapper.byte_sequence parse_result
Sourceval parse_dependent_list' : ('a list -> parse_context -> 'a parse_result) -> 'a list -> parse_context -> 'a list parse_result
Sourceval parse_dependent_list : ('a list -> parse_context -> 'a parse_result) -> parse_context -> 'a list parse_result

line numbers .debug_line, pp and parsing

Sourceval pp_line_number_file_entry : line_number_file_entry -> string
Sourceval pp_line_number_header : line_number_header -> string
Sourceval pp_line_number_operation : line_number_operation -> string
Sourceval pp_line_number_program : line_number_program -> string
Sourceval parse_line_number_file_entry : line_number_file_entry option parser
Sourceval parse_line_number_header : p_context -> string option -> line_number_header parser
Sourceval parse_line_number_program : p_context -> compilation_unit_header -> string option -> line_number_program parser
Sourceval line_number_offset_of_compilation_unit : p_context -> compilation_unit -> Nat_big_num.num
Sourceval line_number_program_of_compilation_unit : dwarf -> compilation_unit -> line_number_program
Sourceval filename : dwarf -> compilation_unit -> Nat_big_num.num -> string option
Sourceval unpack_file_entry : line_number_header -> Nat_big_num.num -> unpacked_file_entry
Sourceval pp_ufe : unpacked_file_entry -> string
Sourceval pp_ud : unpacked_decl -> string
Sourceval pp_ufe_brief : unpacked_file_entry -> string
Sourceval pp_line_info : line_number_program list -> string

all dwarf info: pp and parsing

Sourceval pp_dwarf_like_objdump : dwarf -> string
Sourceval pp_dwarf : dwarf -> string
Sourceval extract_section_body : Elf_file.elf_file -> string -> bool -> p_context * Nat_big_num.num * Byte_sequence_wrapper.byte_sequence
Sourceval extract_dwarf : Elf_file.elf_file -> dwarf option
Sourceval extract_text : Elf_file.elf_file -> p_context * Nat_big_num.num * Byte_sequence.byte_sequence0

************************************************************

****** location evaluation ********************************

************************************************************

pp of locations

Sourceval pp_simple_location : simple_location -> string
Sourceval pp_composite_location_piece : composite_location_piece -> string
Sourceval pp_single_location : single_location -> string

evaluation of location expressions

Sourceval initial_state : state
Sourceval arithmetic_context_of_cuh : compilation_unit_header -> arithmetic_context
Sourceval find_cfa_table_row_for_pc : evaluated_frame_info -> Nat_big_num.num -> cfa_table_row

************************************************************

**** evaluation of frame information **********************

************************************************************

register maps

Sourceval rrp_update : (Nat_big_num.num * register_rule) list -> Nat_big_num.num -> register_rule -> (Nat_big_num.num * register_rule) list
Sourceval rrp_lookup : Nat_big_num.num -> (Nat_big_num.num * register_rule) list -> register_rule
Sourceval rrp_empty : (cfa_register * register_rule) list

pp of evaluated cfa information from .debug_frame

Sourceval register_footprint_rrp : register_rule_map -> cfa_register Pset.set
Sourceval register_footprint : cfa_table_row list -> cfa_register list
Sourceval max_lengths : string list list -> Nat_big_num.num list
Sourceval pad_row : string list -> Nat_big_num.num list -> string list
Sourceval pad_rows : string list list -> string
Sourceval pp_evaluated_fde : ('a * cfa_table_row list) -> string
Sourceval semi_pp_evaluated_fde : ('a * cfa_table_row list) -> (Nat_big_num.num * string * (string * string) list) list
Sourceval semi_pp_evaluated_frame_info : ('a * cfa_table_row list) list -> (Nat_big_num.num * string * (string * string) list) list

evaluation of cfa information from .debug_frame

Sourceval evaluate_call_frame_instruction : frame_info -> cie -> cfa_state -> call_frame_instruction -> cfa_state
Sourceval evaluate_call_frame_instructions : frame_info -> cie -> cfa_state -> call_frame_instruction list -> cfa_state
Sourceval evaluate_fde : frame_info -> fde -> cfa_table_row list
Sourceval evaluate_frame_info : dwarf -> evaluated_frame_info
Sourceval pp_evaluated_frame_info : evaluated_frame_info -> string

************************************************************

** pp of type info

************************************************************

Sourceval strict : (unit -> string) -> 'a option -> 'a
Sourceval analyse_type_info_top : p_context -> dwarf -> bool -> cupdie -> cupdie c_type_top
Sourceval analyse_type_info_deep : dwarf -> bool -> cupdie -> c_type
Sourceval find_DW_AT_type_of_die_deep : dwarf -> (compilation_unit * 'a * die) -> c_type option
Sourceval find_DW_AT_type_of_die_deep_using_abstract_origin : dwarf -> (compilation_unit * 'a * die) -> c_type option
Sourceval pp_struct_union_type_kind : struct_union_type_kind -> string
Sourceval pp_mbyte_size : 'a Show.show_class -> 'a option -> string
Sourceval pp_type_info_top : ('a -> string) -> 'a c_type_top -> string
Sourceval pp_type_info_deep : c_type -> string
Sourceval pp_type_info_die : p_context -> dwarf -> cupdie -> string
Sourceval pp_struct_union_type_member : p_context -> dwarf -> cupdie struct_union_member -> string list
Sourceval pp_struct_union_type_defn : p_context -> dwarf -> cupdie -> string
Sourceval pp_struct_union_type_member' : c_type struct_union_member -> string list
Sourceval pp_enum_type_member' : enumeration_member -> string list
Sourceval pp_struct_union_type_defn' : c_type -> string
Sourceval pp_type_info_die_DW_AT_type : p_context -> dwarf -> compilation_unit -> 'a -> die -> string
Sourceval struct_union_enum_types : dwarf -> c_type list
Sourceval pp_all_struct_union_enum_types' : dwarf -> string

************************************************************

** analysis of location and frame data for reverse mapping

************************************************************

analysis

simple-minded analysis of location

Sourceval analyse_locations_raw : p_context -> dwarf -> string

more proper analysis of locations

Sourceval cu_base_address : compilation_unit -> Nat_big_num.num
Sourceval range_of_die : p_context -> compilation_unit_header -> Byte_sequence.byte_sequence0 -> range_list_list -> Nat_big_num.num -> die -> (Nat_big_num.num * Nat_big_num.num) list option
Sourceval range_of_die_d : dwarf -> compilation_unit -> die -> (Nat_big_num.num * Nat_big_num.num) list option
Sourceval entry_address : die -> Nat_big_num.num option
Sourceval closest_enclosing_range : p_context -> compilation_unit_header -> Byte_sequence.byte_sequence0 -> range_list_list -> Nat_big_num.num -> die list -> (Nat_big_num.num * Nat_big_num.num) list option
Sourceval closest_enclosing_frame_base : 'a -> Nat_big_num.num -> die list -> attribute_value option
Sourceval interpreted_location_of_die : p_context -> compilation_unit_header -> Byte_sequence.byte_sequence0 -> location_list_list -> range_list_list -> Nat_big_num.num -> die list -> die -> (Nat_big_num.num * Nat_big_num.num * single_location_description) list option
Sourceval analyse_locations : dwarf -> analysed_location_data
Sourceval pp_analysed_locations1 : p_context -> compilation_unit_header -> (Nat_big_num.num * Nat_big_num.num * single_location_description) list -> string
Sourceval pp_analysed_locations2 : p_context -> compilation_unit_header -> (Nat_big_num.num * Nat_big_num.num * single_location_description) list option -> string
Sourceval pp_analysed_locations3 : p_context -> dwarf -> Byte_sequence.byte_sequence0 -> bool -> analysed_location_data -> (bool * (string * string * string) * (unit -> string) * string * (unit -> string)) list
Sourceval pp_analysed_locations3_diff : p_context -> dwarf -> Byte_sequence.byte_sequence0 -> analysed_location_data -> analysed_location_data -> (bool * (string * string * string) * (unit -> string) * string * (unit -> string)) list
Sourceval pp_analysed_location_format : (bool * (string * string * string) * (unit -> string) * string * (unit -> string)) list -> string
Sourceval pp_analysed_location_data : dwarf -> analysed_location_data -> string
Sourceval pp_analysed_location_data_diff : dwarf -> analysed_location_data -> analysed_location_data -> string
Sourceval pp_analysed_location_data_at_pc : dwarf -> analysed_location_data_at_pc -> string
Sourceval analysed_locations_at_pc : evaluation_context -> dwarf_static -> Nat_big_num.num -> analysed_location_data_at_pc
Sourceval names_of_address : dwarf -> analysed_location_data_at_pc -> Nat_big_num.num -> string list
Sourceval filtered_analysed_location_data : dwarf_static -> Nat_big_num.num -> ((compilation_unit * die list * die) * (Nat_big_num.num * Nat_big_num.num * Byte_sequence_wrapper.byte_sequence) list option) list

**********************************************************************

** estimate source-file line extents of each (non-inlined) subprogram

**********************************************************************

Sourceval subprogram_line_extents_compilation_unit : dwarf -> compilation_unit -> (string * unpacked_file_entry * Nat_big_num.num) list
Sourceval extract : 'b Lem_basic_classes.eq_class -> 'b -> ('b * 'c) list -> 'c option * ('b * 'c) list
Sourceval partitionby : 'a Lem_basic_classes.eq_class -> 'b Lem_basic_classes.eq_class -> ('a -> 'b) -> ('a -> 'a -> bool) -> 'a list -> ('b * 'a list) list -> ('b * 'a list) list
Sourceval subprogram_line_extents : dwarf -> (unpacked_file_entry * (string * unpacked_file_entry * Nat_big_num.num) list) list
Sourceval pp_subprograms : 'a Show.show_class -> (unpacked_file_entry * (string * 'b * 'a) list) list -> string
Sourceval find_by_line : 'b Lem_basic_classes.ord_class -> 'b -> ('a * 'c * 'b) list -> 'b -> 'a -> 'a
Sourceval subprogram_at_line : ((string option * string option * string) * (string * 'a * Nat_big_num.num) list) list -> unpacked_file_entry -> Nat_big_num.num -> string

************************************************************

** pull out subprograms

************************************************************

************************************************************

** evaluation of line-number info

************************************************************

Sourceval initial_line_number_registers : line_number_header -> line_number_registers
Sourceval evaluate_line_number_program : line_number_program -> line_number_registers list
Sourceval evaluated_line_info_of_compilation_unit : dwarf -> compilation_unit -> (line_number_header * 'a) list -> 'a
Sourceval pp_line_number_registers : line_number_registers -> string
Sourceval pp_line_number_registers_tight : line_number_registers -> string list
Sourceval pp_line_number_registerss : line_number_registers list -> string
Sourceval pp_evaluated_line_info : evaluated_line_info -> string
Sourceval source_lines_of_address : dwarf_static -> Nat_big_num.num -> (unpacked_file_entry * Nat_big_num.num * line_number_registers * string) list

************************************************************

** collecting all the statically calculated analysis info

************************************************************

Sourceval extract_dwarf_static : Elf_file.elf_file -> dwarf_static option

************************************************************

** collect simple die tree view

************************************************************

Sourceval decl_of_die : dwarf -> ((string option * string option * string) * (string * 'a * Nat_big_num.num) list) list -> compilation_unit -> die -> (unpacked_file_entry * int * string) option
Sourceval call_site_of_die : dwarf -> ((string option * string option * string) * (string * 'a * Nat_big_num.num) list) list -> compilation_unit -> die -> (unpacked_file_entry * int * string) option
Sourceval mk_sdt_unspecified_parameter : dwarf -> 'a -> 'b -> 'c -> die -> sdt_unspecified_parameter option
Sourceval mk_sdt_variable_or_formal_parameter : dwarf -> ((string option * string option * string) * (string * 'a * Nat_big_num.num) list) list -> compilation_unit -> die list -> die -> sdt_variable_or_formal_parameter option
Sourceval strict_mss : 'a option -> string -> ('b -> string) -> 'b -> 'a
Sourceval mk_sdt_subroutine : dwarf -> ((string option * string option * string) * (string * 'a * Nat_big_num.num) list) list -> compilation_unit -> die list -> die -> sdt_subroutine option
Sourceval mk_sdt_lexical_block : dwarf -> ((string option * string option * string) * (string * 'a * Nat_big_num.num) list) list -> compilation_unit -> die list -> die -> sdt_lexical_block option
Sourceval strict_mscu : 'a option -> string -> ('b -> string) -> 'b -> 'a
Sourceval mk_sdt_compilation_unit : dwarf -> ((string option * string option * string) * (string * 'a * Nat_big_num.num) list) list -> compilation_unit -> sdt_compilation_unit
Sourceval mk_sdt_dwarf : dwarf -> ((string option * string option * string) * (string * 'a * Nat_big_num.num) list) list -> sdt_dwarf
Sourceval pp_sdt_unspecified_parameter : Nat_big_num.num -> sdt_unspecified_parameter -> string
Sourceval pp_parsed_single_location_description : Nat_big_num.num -> (Nat_big_num.num * Nat_big_num.num * operation list) -> string
Sourceval pp_pc_ranges : Nat_big_num.num -> (Nat_big_num.num * Nat_big_num.num) list option -> string
Sourceval pp_sdt_maybe : 'a option -> ('a -> string) -> string
Sourceval pp_sdt_maybe' : ('a -> string) -> 'a option -> string
Sourceval pp_sdt_list : 'a list -> ('a -> string) -> string
Sourceval pp_sdt_variable_or_formal_parameter : Nat_big_num.num -> sdt_variable_or_formal_parameter -> string
Sourceval pp_sdt_subroutine : Nat_big_num.num -> sdt_subroutine -> string
Sourceval pp_sdt_lexical_block : Nat_big_num.num -> sdt_lexical_block -> string
Sourceval pp_sdt_compilation_unit : Nat_big_num.num -> sdt_compilation_unit -> string
Sourceval pp_sdt_dwarf : sdt_dwarf -> string
Sourceval pp_sdt_concise_variable_or_formal_parameter : Nat_big_num.num -> sdt_variable_or_formal_parameter -> string
Sourceval pp_sdt_globals_compilation_unit : Nat_big_num.num -> sdt_compilation_unit -> string
Sourceval pp_sdt_globals_dwarf : sdt_dwarf -> string
Sourceval pp_sdt_locals_subroutine : Nat_big_num.num -> sdt_subroutine -> string
Sourceval pp_sdt_locals_lexical_block : Nat_big_num.num -> sdt_lexical_block -> string
Sourceval pp_sdt_locals_compilation_unit : Nat_big_num.num -> sdt_compilation_unit -> string
Sourceval pp_sdt_locals_dwarf : sdt_dwarf -> string

************************************************************

** analysis of inlined_subroutine data

************************************************************

Sourceval analyse_inlined_subroutines_sdt_const_param : sdt_variable_or_formal_parameter -> inlined_subroutine_const_param option
Sourceval analyse_inlined_subroutines_sdt_subroutine : sdt_subroutine list -> sdt_subroutine -> inlined_subroutine list
Sourceval analyse_inlined_subroutines_sdt_lexical_block : sdt_subroutine list -> sdt_lexical_block -> inlined_subroutine list
Sourceval analyse_inlined_subroutines_sdt_compilation_unit : sdt_compilation_unit -> inlined_subroutine list
Sourceval analyse_inlined_subroutines_sdt_dwarf : sdt_dwarf -> inlined_subroutine list
Sourceval analyse_inlined_subroutine_by_range : inlined_subroutine -> inlined_subroutine_data_by_range
Sourceval is_lt : 'a Lem_basic_classes.eq_class -> 'b Lem_basic_classes.ord_class -> 'a Lem_basic_classes.ord_class -> (('a * 'b) * ('c * 'd) * 'e) -> (('a * 'b) * ('f * 'g) * 'h) -> bool
Sourceval analyse_inlined_subroutines_by_range : inlined_subroutine_data -> inlined_subroutine_data_by_range
Sourceval pp_inlined_subroutine_parents : die list -> string
Sourceval pp_inlined_subroutine_header : dwarf_static -> inlined_subroutine -> string
Sourceval pp_inlined_subroutine_const_params : dwarf -> inlined_subroutine -> string
Sourceval pp_inlined_subroutine : dwarf_static -> inlined_subroutine -> string
Sourceval pp_inlined_subroutines : dwarf_static -> inlined_subroutine list -> string
Sourceval pp_inlined_subroutine_by_range : dwarf_static -> ((Nat_big_num.num * Nat_big_num.num) * (Nat_big_num.num * Nat_big_num.num) * inlined_subroutine) -> string
Sourceval pp_inlined_subroutines_by_range : dwarf_static -> ((Nat_big_num.num * Nat_big_num.num) * (Nat_big_num.num * Nat_big_num.num) * inlined_subroutine) list -> string

************************************************************

** pp of text section

************************************************************

Sourceval words_of_byte_sequence : Nat_big_num.num -> Byte_sequence.byte_sequence0 -> (Nat_big_num.num * Nat_big_num.num) list -> (Nat_big_num.num * Nat_big_num.num) list
Sourceval pp_instruction : (Nat_big_num.num * Nat_big_num.num) -> string
Sourceval pp_text_section : Elf_file.elf_file -> string

************************************************************

** top level for main_elf ********************************

************************************************************

Sourceval harness_string_of_elf_like_objdump : Elf_file.elf_file -> 'a -> string
Sourceval harness_string_of_elf : Elf_file.elf_file -> 'a -> string
Sourceval harness_string_of_elf64_debug_info_section : Elf_file.elf64_file -> 'a -> string
Sourceval harness_string_of_elf32_debug_info_section : Elf_file.elf32_file -> 'a -> string
Sourceval harness_string_of_elf64_like_objdump : Elf_file.elf64_file -> 'a -> string
Sourceval harness_string_of_elf32_like_objdump : Elf_file.elf32_file -> 'a -> string