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_ctypes/index.html

Module Dwarf_ctypesSource

Sourcetype sym = string
Sourcetype cabs_identifier = string
Sourcetype integer_value_base = int
Sourcetype integerBaseType =
  1. | Ichar
  2. | Short
  3. | Int_
  4. | Long
  5. | LongLong
  6. | IntN_t of int
  7. | Int_leastN_t of int
  8. | Int_fastN_t of int
  9. | Intmax_t
  10. | Intptr_t
Sourcetype integerType =
  1. | Char
  2. | Bool
  3. | Signed of integerBaseType
  4. | Unsigned of integerBaseType
  5. | Enum of sym
  6. | Wchar_t
  7. | Wint_t
  8. | Size_t
  9. | Ptrdiff_t
Sourcetype realFloatingType =
  1. | Float
  2. | Double
  3. | LongDouble
Sourcetype floatingType =
  1. | RealFloating of realFloatingType
Sourcetype basicType =
  1. | Integer of integerType
  2. | Floating of floatingType
Sourcetype qualifiers = {
  1. const : bool;
  2. restrict : bool;
  3. volatile : bool;
}
Sourcetype ctype_ =
  1. | Void
  2. | Basic of basicType
  3. | Array of ctype * Nat_big_num.num option
  4. | Function of bool * qualifiers * ctype * (qualifiers * ctype * bool) list * bool
  5. | Pointer of qualifiers * ctype
  6. | Atomic of ctype
  7. | Struct of sym
  8. | Union of sym
Sourceand ctype =
  1. | Ctype of ctype_ list
Sourcetype struct_tag = sym
Sourcetype union_tag = sym
Sourcetype member_id = sym
Sourcetype tag_definition =
  1. | StructDef of (cabs_identifier * (qualifiers * ctype)) list
  2. | UnionDef of (cabs_identifier * (qualifiers * ctype)) list
Sourcetype shift_path_element =
  1. | SPE_array of ctype * integer_value_base
  2. | SPE_member of sym * cabs_identifier