package linksem

You can search for identifiers within the package.

in-package search v0.2.0

A formalisation of the core ELF and DWARF file formats written in Lem

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

Maintainers

L

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

Sources

md5=2075c56715539b3b8f54ae65cc808b8c

sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2

doc/linksem_zarith/Gnu_ext_symbol_versioning/index.html

Module `Gnu_ext_symbol_versioning`Source

The gnu_ext_symbol_versioning defines constants, types and functions * relating to the GNU symbol versioning extensions (i.e. contents of * GNU_VERSYM sections). * * TODO: work out what is going on with symbol versioning. The specification * is completely opaque.

Sourceval gnu_ext_ver_def_none : Nat_big_num.num

No version

Sourceval gnu_ext_ver_def_current : Nat_big_num.num

No version

Current version

Sourceval gnu_ext_ver_flg_base : Nat_big_num.num

Version definition of file itself

Sourceval gnu_ext_ver_flg_weak : Nat_big_num.num

Version definition of file itself

Weak version identifier

Sourceval gnu_ext_ver_ndx_local : Nat_big_num.num

Symbol is local

Sourceval gnu_ext_ver_ndx_global : Nat_big_num.num

Symbol is local

Symbol is global

Sourceval gnu_ext_ver_ndx_loreserve : Nat_big_num.num

Symbol is global

Beginning of reserved entries

Sourceval gnu_ext_ver_ndx_eliminate : Nat_big_num.num

Beginning of reserved entries

Symbol is to be eliminated

Sourceval gnu_ext_ver_need_none : Nat_big_num.num

No version

Sourceval gnu_ext_ver_need_current : Nat_big_num.num

No version

Current version

Sourcetype gnu_ext_elf32_symbol_version_table = Uint32_wrapper.uint32 list

gnu_ext_elf32_symbol_version_table is an array (linked list, here) of * elf32_half entries. It has as many entries as the dynamic symbol table * (DT_SYMTAB). I.e., each symbol table entry has its associated entry in the * symbol version table.

Sourcetype gnu_ext_elf64_symbol_version_table = Uint32_wrapper.uint32 list

val read_gnu_ext_elf64_versym_table : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  Uint32_wrapper.uint32 list Error.error

Sourcetype gnu_ext_elf32_verdef = {

gnu_ext_elf32_vd_version : Uint32_wrapper.uint32;
gnu_ext_elf32_vd_flags : Uint32_wrapper.uint32;
gnu_ext_elf32_vd_ndx : Uint32_wrapper.uint32;
gnu_ext_elf32_vd_cnt : Uint32_wrapper.uint32;
gnu_ext_elf32_vd_hash : Uint32_wrapper.uint32;
gnu_ext_elf32_vd_aux : Uint32_wrapper.uint32;
gnu_ext_elf32_vd_next : Uint32_wrapper.uint32;

}

Sourcetype gnu_ext_elf64_verdef = {

gnu_ext_elf64_vd_version : Uint32_wrapper.uint32;
gnu_ext_elf64_vd_flags : Uint32_wrapper.uint32;
gnu_ext_elf64_vd_ndx : Uint32_wrapper.uint32;
gnu_ext_elf64_vd_cnt : Uint32_wrapper.uint32;
gnu_ext_elf64_vd_hash : Uint32_wrapper.uint32;
gnu_ext_elf64_vd_aux : Uint32_wrapper.uint32;
gnu_ext_elf64_vd_next : Uint32_wrapper.uint32;

}

Sourceval string_of_gnu_ext_elf32_verdef : gnu_ext_elf32_verdef -> string

Sourceval string_of_gnu_ext_elf64_verdef : gnu_ext_elf64_verdef -> string

val read_gnu_ext_elf32_verdef : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  (gnu_ext_elf32_verdef * Byte_sequence_wrapper.byte_sequence) Error.error

val read_gnu_ext_elf64_verdef : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  (gnu_ext_elf64_verdef * Byte_sequence_wrapper.byte_sequence) Error.error

Sourceval gnu_ext_elf32_verdef_size : Nat_big_num.num

Sourceval gnu_ext_elf64_verdef_size : Nat_big_num.num

Sourcetype gnu_ext_elf32_veraux = {

gnu_ext_elf32_vda_name : Uint32_wrapper.uint32;
gnu_ext_elf32_vda_next : Uint32_wrapper.uint32;

}

Sourcetype gnu_ext_elf64_veraux = {

gnu_ext_elf64_vda_name : Uint32_wrapper.uint32;
gnu_ext_elf64_vda_next : Uint32_wrapper.uint32;

}

Sourceval gnu_ext_elf32_veraux_size : Nat_big_num.num

Sourceval gnu_ext_elf64_veraux_size : Nat_big_num.num

val read_gnu_ext_elf32_veraux : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  (gnu_ext_elf32_veraux * Byte_sequence_wrapper.byte_sequence) Error.error

val read_gnu_ext_elf64_veraux : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  (gnu_ext_elf64_veraux * Byte_sequence_wrapper.byte_sequence) Error.error

val read_gnu_ext_elf64_veraux_table : 
  Endianness.endianness ->
  Nat_big_num.num ->
  Byte_sequence_wrapper.byte_sequence ->
  (gnu_ext_elf64_veraux list * Byte_sequence_wrapper.byte_sequence) Error.error

val read_gnu_ext_elf64_verdef_table : 
  Endianness.endianness ->
  Nat_big_num.num ->
  Byte_sequence_wrapper.byte_sequence ->
  ((gnu_ext_elf64_verdef * gnu_ext_elf64_veraux list) list
   * Byte_sequence_wrapper.byte_sequence)
    Error.error

Sourcetype gnu_ext_elf32_verneed = {

gnu_ext_elf32_vn_version : Uint32_wrapper.uint32;
gnu_ext_elf32_vn_cnt : Uint32_wrapper.uint32;
gnu_ext_elf32_vn_file : Uint32_wrapper.uint32;
gnu_ext_elf32_vn_aux : Uint32_wrapper.uint32;
gnu_ext_elf32_vn_next : Uint32_wrapper.uint32;

}

Sourcetype gnu_ext_elf64_verneed = {

gnu_ext_elf64_vn_version : Uint32_wrapper.uint32;
gnu_ext_elf64_vn_cnt : Uint32_wrapper.uint32;
gnu_ext_elf64_vn_file : Uint32_wrapper.uint32;
gnu_ext_elf64_vn_aux : Uint32_wrapper.uint32;
gnu_ext_elf64_vn_next : Uint32_wrapper.uint32;

}

Sourceval gnu_ext_elf32_verneed_size : Nat_big_num.num

Sourceval gnu_ext_elf64_verneed_size : Nat_big_num.num

val read_gnu_ext_elf32_verneed : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  (gnu_ext_elf32_verneed * Byte_sequence_wrapper.byte_sequence) Error.error

val read_gnu_ext_elf64_verneed : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  (gnu_ext_elf64_verneed * Byte_sequence_wrapper.byte_sequence) Error.error

Sourcetype gnu_ext_elf32_vernaux = {

gnu_ext_elf32_vna_hash : Uint32_wrapper.uint32;
gnu_ext_elf32_vna_flags : Uint32_wrapper.uint32;
gnu_ext_elf32_vna_other : Uint32_wrapper.uint32;
gnu_ext_elf32_vna_name : Uint32_wrapper.uint32;
gnu_ext_elf32_vna_next : Uint32_wrapper.uint32;

}

Sourcetype gnu_ext_elf64_vernaux = {

gnu_ext_elf64_vna_hash : Uint32_wrapper.uint32;
gnu_ext_elf64_vna_flags : Uint32_wrapper.uint32;
gnu_ext_elf64_vna_other : Uint32_wrapper.uint32;
gnu_ext_elf64_vna_name : Uint32_wrapper.uint32;
gnu_ext_elf64_vna_next : Uint32_wrapper.uint32;

}

Sourceval string_of_gnu_ext_elf32_vernaux : gnu_ext_elf32_vernaux -> string

Sourceval string_of_gnu_ext_elf64_vernaux : gnu_ext_elf64_vernaux -> string

Sourceval gnu_ext_elf32_vernaux_size : Nat_big_num.num

Sourceval gnu_ext_elf64_vernaux_size : Nat_big_num.num

val read_gnu_ext_elf32_vernaux : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  (gnu_ext_elf32_vernaux * Byte_sequence_wrapper.byte_sequence) Error.error

val read_gnu_ext_elf64_vernaux : 
  Endianness.endianness ->
  Byte_sequence_wrapper.byte_sequence ->
  (gnu_ext_elf64_vernaux * Byte_sequence_wrapper.byte_sequence) Error.error

val read_gnu_ext_elf64_vernaux_table : 
  Endianness.endianness ->
  Nat_big_num.num ->
  Byte_sequence_wrapper.byte_sequence ->
  (gnu_ext_elf64_vernaux list * Byte_sequence_wrapper.byte_sequence)
    Error.error

val read_gnu_ext_elf64_verneed_table : 
  Endianness.endianness ->
  Nat_big_num.num ->
  Byte_sequence_wrapper.byte_sequence ->
  ((gnu_ext_elf64_verneed * gnu_ext_elf64_vernaux list) list
   * Byte_sequence_wrapper.byte_sequence)
    Error.error

Sourcetype gnu_ext_interpreted_verdef = {

gnu_ext_interpreted_verdef_version : Nat_big_num.num;
gnu_ext_interpreted_verdef_flags : Nat_big_num.num;
gnu_ext_interpreted_verdef_ndx : Nat_big_num.num;
gnu_ext_interpreted_verdef_hash : Nat_big_num.num;
gnu_ext_interpreted_verdef_name : string;
gnu_ext_interpreted_verdef_parents : string list;

}

Sourcetype gnu_ext_interpreted_verneed = {

gnu_ext_interpreted_verneed_version : Nat_big_num.num;
gnu_ext_interpreted_verneed_file : string;

}

Sourcetype gnu_ext_interpreted_vernaux = {

gnu_ext_interpreted_vernaux_hash : Nat_big_num.num;
gnu_ext_interpreted_vernaux_flags : Nat_big_num.num;
gnu_ext_interpreted_vernaux_other : Nat_big_num.num;
gnu_ext_interpreted_vernaux_name : string;
gnu_ext_interpreted_vernaux_verneed : gnu_ext_interpreted_verneed;

}

Sourcetype gnu_ext_interpreted_versym_entry = {

gnu_ext_interpreted_versym_entry_value : Nat_big_num.num;
gnu_ext_interpreted_versym_entry_hidden : bool;

}

Sourcetype gnu_ext_interpreted_versym_table = {

gnu_ext_interpreted_versym_table_entries : gnu_ext_interpreted_versym_entry list;
gnu_ext_interpreted_versym_table_verdef : gnu_ext_interpreted_verdef list;
gnu_ext_interpreted_versym_table_verneed : gnu_ext_interpreted_vernaux list;

}

Sourceval gnu_ext_verdef_base_unspecified : Nat_big_num.num

The unspecified name for the base definition.

The name given later to the baseline of symbols once the library started using symbol versioning.

Sourceval gnu_ext_verdef_base_versioned : Nat_big_num.num

The name given later to the baseline of symbols once the library started using symbol versioning.

val obtain_gnu_ext_elf64_interpreted_versym_table_symbols : 
  Endianness.endianness ->
  Elf_file.elf64_file ->
  (Nat_big_num.num * (Nat_big_num.num, 'a) Elf_dynamic.dyn_value) list ->
  gnu_ext_interpreted_versym_entry list option Error.error

val obtain_gnu_ext_elf64_interpreted_verdef_table : 
  Endianness.endianness ->
  Elf_file.elf64_file ->
  (Nat_big_num.num * (Nat_big_num.num, 'a) Elf_dynamic.dyn_value) list ->
  gnu_ext_interpreted_verdef list option Error.error

val obtain_gnu_ext_elf64_interpreted_verneed_table : 
  Endianness.endianness ->
  Elf_file.elf64_file ->
  (Nat_big_num.num * (Nat_big_num.num, 'a) Elf_dynamic.dyn_value) list ->
  gnu_ext_interpreted_vernaux list option Error.error

val obtain_gnu_ext_elf64_interpreted_versym_table : 
  Elf_file.elf64_file ->
  (Nat_big_num.num * (Nat_big_num.num, 'a) Elf_dynamic.dyn_value) list ->
  gnu_ext_interpreted_versym_table option Error.error

Sourcetype gnu_ext_interpreted_verdef_lookup =

| GnuExtInterpretedVerdefLocal
| GnuExtInterpretedVerdefGlobal
| GnuExtInterpretedVerdefVersion of gnu_ext_interpreted_verdef
| GnuExtInterpretedVerdefHidden of gnu_ext_interpreted_verdef

val get_gnu_ext_interpreted_verdef : 
  gnu_ext_interpreted_versym_table ->
  Nat_big_num.num ->
  gnu_ext_interpreted_verdef_lookup Error.error

val get_gnu_ext_interpreted_verneed : 
  gnu_ext_interpreted_versym_table ->
  Nat_big_num.num ->
  gnu_ext_interpreted_vernaux option Error.error