diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-10-13 18:46:22 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-10-13 18:46:22 +0200 |
commit | 6fea0ef0958b66711235659ac2cd7122afc04897 (patch) | |
tree | 8e0cb3357cb4bf581f2219d71e0a152031f83c55 /debug | |
parent | 1915258c8b2cd2e171bbce93658047a765232bc9 (diff) | |
download | compcert-6fea0ef0958b66711235659ac2cd7122afc04897.tar.gz compcert-6fea0ef0958b66711235659ac2cd7122afc04897.zip |
Added a file containing definitions for the types used to store the debug information. The types follow the Current Attributes by Tag Value in Appendix 1 of the Dwarf 2 standard.
Diffstat (limited to 'debug')
-rw-r--r-- | debug/DwarfTypes.ml | 121 |
1 files changed, 121 insertions, 0 deletions
diff --git a/debug/DwarfTypes.ml b/debug/DwarfTypes.ml new file mode 100644 index 00000000..afa29e13 --- /dev/null +++ b/debug/DwarfTypes.ml @@ -0,0 +1,121 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* Types used for writing dwarf debug information *) + +(* Basic types for the value of attributes *) + +type constant = int + +type flag = bool + +type reference = int + +type encoding = + | DW_ATE_address + | DW_ATE_boolean + | DW_ATE_complex_float + | DW_ATE_float + | DW_ATE_signed + | DW_ATE_signed_char + | DW_ATE_unsigned + | DW_ATE_unsigned_char + +type identifier_case = + | DW_ID_case_sensitive + | DW_ID_up_case + | DW_ID_down_case + | DW_ID_case_insensitive + +type address = int + +type language = + | DW_LANG_C + | DW_LANG_C89 + +type block = string (* Used as bitvector *) + +type const_value = + | String of string + | Const of constant + | Block of block + +(* Types representing the attribute information per tag value *) + +type dw_tag_array_type = + { + dw_at_byte_size: constant option; + dw_at_declaration: flag option; + dw_at_name: string option; + dw_at_sibling: reference option; + dw_at_start_scope: constant option; + dw_at_stride_size: constant option; + dw_at_type: reference option; + } + +type dw_tag_base_type = + { + dw_at_bit_offset: constant option; + dw_at_bit_size: constant option; + dw_at_byte_size: constant option; + dw_at_encoding: encoding option; + dw_at_name: string option; + dw_at_sibling: reference option; + } + +type dw_tag_compile_unit = + { + dw_at_base_types: reference option; + dw_at_comp_dir: string option; + dw_at_identifier_case: identifier_case option; + dw_at_high_pc: address option; + dw_at_language: language option; + dw_at_low_pc: address option; + dw_at_macro_info: constant option; + dw_at_name: string option; + dw_at_producer: string option; + dw_at_sibling: reference option; + dw_at_stmt_list: constant option; + } + +type dw_tag_const_type = + { + dw_at_sibling: reference option; + dw_at_type: reference option; + } + +type dw_tag_constant = + { + dw_at_const_value: constant option; + dw_at_declaration: flag option; + dw_at_external: flag option; + dw_at_name: string option; + dw_at_sibling: reference option; + dw_at_start_scope: constant option; + dw_at_type: reference option; + } + +type dw_tag_enumeration_type = + { + dw_at_byte_size: constant option; + dw_at_declaration: flag option; + dw_at_name: string option; + dw_at_sibling: reference option; + dw_at_start_scope: constant option; + } + +type dw_tag_enumerator = + { + dw_at_const_value: constant option; + dw_at_name: string option; + dw_at_sibling: reference option; + } |