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

Module Gnu_ext_section_header_tableSource

The module gnu_ext_section_header_table implements function, definitions * and types relating to the GNU extensions to the standard ELF section header * table.

GNU extended section types

Sourceval sht_gnu_hash : Nat_big_num.num

GNU_HASH does not appear to be defined in the LSB but is present in * several ELF binaries collected in the wild... * * TODO: find out where this comes from? * ANSW: a mailing list apparently! See here: * https://sourceware.org/ml/binutils/2006-10/msg00377.html

The following are all defined in Section 10.2.2.2 of the LSB as additional * section types over the ones defined in the SCO ELF spec.

Sourceval sht_gnu_verdef : Nat_big_num.num

sht_gnu_verdef contains the symbol versions that are provided.

sht_gnu_verneed contains the symbol versions that are required.

Sourceval sht_gnu_verneed : Nat_big_num.num

sht_gnu_verneed contains the symbol versions that are required.

sht_gnu_versym contains the symbol version table.

Sourceval sht_gnu_versym : Nat_big_num.num

sht_gnu_versym contains the symbol version table.

sht_gnu_liblist appears to be undocumented but appears in PowerPC 64 ELF * binaries in "the wild".

Sourceval sht_gnu_liblist : Nat_big_num.num

sht_gnu_liblist appears to be undocumented but appears in PowerPC 64 ELF * binaries in "the wild".

Sourceval string_of_gnu_ext_section_type : Nat_big_num.num -> string

string_of_gnu_ext_section_type m produces a string based representation of * GNU extension section type m.

Sourceval gnu_ext_additional_special_sections : (string, Nat_big_num.num * Nat_big_num.num) Pmap.map

gnu_ext_additionall_special_sections records additional section names that * map appear in GNU ELF binaries and their required associated types and * attributes. See Section 10.3.1.1 of the LSB and the related map * elf_special_sections in Elf_section_header_table which records section * names and their required types and attributes that all ELF binaries share.

Sourceval is_valid_gnu_ext_elf32_section_header_table_entry : Elf_interpreted_section.elf32_interpreted_section -> String_table.string_table -> bool

is_valid_gnu_ext_elf32_section_header_table_entry scts stbl checks whether * sections scts conforms with the contents of the special sections table. * Fails otherwise.

Sourceval is_valid_gnu_ext_elf32_section_header_table : Elf_interpreted_section.elf32_interpreted_section list -> String_table.string_table -> bool

is_valid_gnu_ext_elf32_section_header_table sht stbl checks whether every * member of the section header table sht conforms with the special sections * table.

Sourceval is_valid_gnu_ext_elf64_section_header_table_entry : Elf_interpreted_section.elf64_interpreted_section -> String_table.string_table -> bool

is_valid_gnu_ext_elf64_section_header_table_entry scts stbl checks whether * sections scts conforms with the contents of the special sections table. * Fails otherwise.

Sourceval is_valid_gnu_ext_elf64_section_header_table : Elf_interpreted_section.elf64_interpreted_section list -> String_table.string_table -> bool

is_valid_gnu_ext_elf64_section_header_table sht stbl checks whether every * member of the section header table sht conforms with the special sections * table.