package linksem
A formalisation of the core ELF and DWARF file formats written in Lem
Install
Dune Dependency
Authors
Maintainers
Sources
0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/src/linksem_zarith/dwarf_ctypes.ml.html
Source file dwarf_ctypes.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124
(*Generated by Lem from dwarf_ctypes.lem.*) open Lem_basic_classes open Lem_bool open Lem_function open Lem_maybe open Lem_num open Lem_string open Lem_list (* TODO: check why this is not imported in ELF *) (* these are Lem types of C source type names, based on Cerberus frontend/model/ctype.lem (see the types "ctype_" and "tag_definition") and pointer arithmetic, based on frontend/model/defacto_memory_types.lem (see "shift_path_element"). They will need to be adapted significantly to exactly match the DWARF notion of C source types, at least for those we use. *) (* (C) Justus Matthiesen * Kayvan Memarian * Victor Gomes *) type sym = string (* in cerberus this is Symbol.sym; here we maight want a unique die tag *) type cabs_identifier = string (* in cerberus this is Cabs.cabs_identifier *) type integer_value_base = int (* in cerberus this is more complex...*) type (* name = "^\\(\\|\\([a-z A-Z]+_\\)\\)ibty[0-9]*'?$"*) integerBaseType = | Ichar | Short | Int_ | Long | LongLong (* Things defined in the standard libraries *) | IntN_t of int | Int_leastN_t of int | Int_fastN_t of int | Intmax_t | Intptr_t (* STD §6.2.5#17, sentence 1 *) type integerType (* [name = "^\\(\\|\\([a-z A-Z]+_\\)\\)ity[0-9]*'?$"] *) = | Char | Bool | Signed of integerBaseType | Unsigned of integerBaseType | Enum of sym (* Things defined in the standard libraries *) | Wchar_t | Wint_t | Size_t | Ptrdiff_t (* STD §6.2.5#10, sentence 1 *) type realFloatingType = | Float | Double | LongDouble (* STD §6.2.5#11, sentence 2 *) type floatingType = | RealFloating of realFloatingType (* | Complex of floatingType (* STD §6.2.5#11, sentence 1 *) *) (* STD §6.2.5#14, sentence 1 *) type (* name = "^\\(\\|\\([a-z A-Z]+_\\)\\)bty[0-9]*'?$"*) basicType = | Integer of integerType | Floating of floatingType (* STD §6.2.5#26, sentence 1-2 *) type qualifiers (*[name = "^\\(\\|\\([a-z A-Z]+_\\)\\)qs[0-9]*'?$"]*) = { const : bool; restrict : bool; volatile : bool; (* NOTE: the desugaring collapse _Atomic qualifiers and specifiers *) } type ctype_ (*[name = "^\\([a-z A-Z]*_\\)?ty[0-9]*'?$"]*) = | Void | Basic of basicType (* INVARIANT if the element ctype is an array, the qualifiers must be empty *) (* the qualifiers are that of the element type (§6.7.3#9) *) (* STD §6.2.5#20, bullet 1 *) | Array of ctype * ( Nat_big_num.num option) (* NOTE: the qualifiers associated to a ctype in the list of parameters is that of the parameter lvalue. For example if we have a parameter with type "restrict pointer to a const char", the qualifiers in the tuple will be: {no_qualifiers with restrict=true} *) (* STD §6.2.5#20, bullet 4 *) | Function of (* has_proto *)bool * (qualifiers * ctype) * (qualifiers * ctype * (* is_register *)bool) list * (* is_variadic *)bool (* STD §6.2.5#20, bullet 5 *) (* NOTE: the qualifiers are that of the referenced type *) | Pointer of qualifiers * ctype (* STD §6.2.5#20, bullet 6 *) | Atomic of ctype | Struct of sym | Union of sym and ctype = Ctype of ctype_ list type struct_tag = sym type union_tag = sym type member_id = sym type tag_definition = | StructDef of (cabs_identifier * (qualifiers * ctype)) list | UnionDef of (cabs_identifier * (qualifiers * ctype)) list type shift_path_element = | SPE_array of ctype * integer_value_base | SPE_member of sym (*struct/union tag*) * cabs_identifier (*member*)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>