package linksem

  1. Overview
  2. Docs
package linksem
Legend:
Library
Module
Module type
Parameter
Class
Class type

Module elf_interpreted_section provides a record of "interpreted" sections, * i.e. the data stored in the section header table converted to more amenable * infinite precision types, and operation on those records.

type elf32_interpreted_section = {
  1. elf32_section_name : Nat_big_num.num;
    (*

    Name of the section

    *)
  2. elf32_section_type : Nat_big_num.num;
    (*

    Type of the section

    *)
  3. elf32_section_flags : Nat_big_num.num;
    (*

    Flags associated with the section

    *)
  4. elf32_section_addr : Nat_big_num.num;
    (*

    Base address of the section in memory

    *)
  5. elf32_section_offset : Nat_big_num.num;
    (*

    Offset from beginning of file

    *)
  6. elf32_section_size : Nat_big_num.num;
    (*

    Section size in bytes

    *)
  7. elf32_section_info : Nat_big_num.num;
    (*

    Extra information, depends on section type

    *)
  8. elf32_section_align : Nat_big_num.num;
    (*

    Alignment constraints for section

    *)
  9. elf32_section_entsize : Nat_big_num.num;
    (*

    Size of each entry in table, if section is one

    *)
  10. elf32_section_body : Byte_sequence.byte_sequence0;
    (*

    Body of section

    *)
  11. elf32_section_name_as_string : string;
    (*

    Name of the section, as a string; "" for no name (name = 0)

    *)
}

elf32_interpreted_section exactly mirrors the structure of a section header * table entry, barring the conversion of all fields to more amenable types.

val elf32_interpreted_section_equal : elf32_interpreted_section -> elf32_interpreted_section -> bool

elf32_interpreted_section_equal s1 s2 is an equality test on interpreted * sections s1 and s2.

val instance_Basic_classes_Eq_Elf_interpreted_section_elf32_interpreted_section_dict : elf32_interpreted_section Lem_basic_classes.eq_class
type elf64_interpreted_section = {
  1. elf64_section_name : Nat_big_num.num;
    (*

    Name of the section

    *)
  2. elf64_section_type : Nat_big_num.num;
    (*

    Type of the section

    *)
  3. elf64_section_flags : Nat_big_num.num;
    (*

    Flags associated with the section

    *)
  4. elf64_section_addr : Nat_big_num.num;
    (*

    Base address of the section in memory

    *)
  5. elf64_section_offset : Nat_big_num.num;
    (*

    Offset from beginning of file

    *)
  6. elf64_section_size : Nat_big_num.num;
    (*

    Section size in bytes

    *)
  7. elf64_section_info : Nat_big_num.num;
    (*

    Extra information, depends on section type

    *)
  8. elf64_section_align : Nat_big_num.num;
    (*

    Alignment constraints for section

    *)
  9. elf64_section_entsize : Nat_big_num.num;
    (*

    Size of each entry in table, if section is one

    *)
  10. elf64_section_body : Byte_sequence.byte_sequence0;
    (*

    Body of section

    *)
  11. elf64_section_name_as_string : string;
    (*

    Name of the section, as a string; "" for no name (name = 0)

    *)
}

elf64_interpreted_section exactly mirrors the structure of a section header * table entry, barring the conversion of all fields to more amenable types.

val compare_elf64_interpreted_section : elf64_interpreted_section -> elf64_interpreted_section -> int

compare_elf64_interpreted_section s1 s2 is an ordering comparison function * on interpreted sections suitable for use in sets, finite maps and other * ordered structures.

val instance_Basic_classes_Ord_Elf_interpreted_section_elf64_interpreted_section_dict : elf64_interpreted_section Lem_basic_classes.ord_class
val elf64_interpreted_section_equal : elf64_interpreted_section -> elf64_interpreted_section -> bool

elf64_interpreted_section_equal s1 s2 is an equality test on interpreted * sections s1 and s2.

val null_elf32_interpreted_section : elf32_interpreted_section

null_elf32_interpreted_section --- the null interpreted section.

val null_elf64_interpreted_section : elf64_interpreted_section

null_elf64_interpreted_section --- the null interpreted section.

val instance_Basic_classes_Eq_Elf_interpreted_section_elf64_interpreted_section_dict : elf64_interpreted_section Lem_basic_classes.eq_class
val elf64_interpreted_section_matches_section_header : elf64_interpreted_section -> Elf_section_header_table.elf64_section_header_table_entry -> bool

elf64_interpreted_section_matches_section_header sect ent checks whether * the interpreted section and the corresponding section header table entry * match.

type elf32_interpreted_sections = elf32_interpreted_section list
type elf64_interpreted_sections = elf64_interpreted_section list
val string_of_elf32_interpreted_section : elf32_interpreted_section -> string

string_of_elf32_interpreted_section sect returns a string-based representation * of interpreted section, sect.

val string_of_elf64_interpreted_section : elf64_interpreted_section -> string

string_of_elf64_interpreted_section sect returns a string-based representation * of interpreted section, sect.

val is_valid_elf32_section_header_table_entry : elf32_interpreted_section -> String_table.string_table -> bool

is_valid_elf32_section_header_table_entry sect stab checks whether a * interpreted section conforms with the prescribed flags and types declared * in the "special sections" table of the ELF specification. * TODO: some of these entries in the table are overridden by ABI supplements. * Make sure it is these that are passed in rather than the default table * declared in the spec?

val is_valid_elf64_section_header_table_entry : elf64_interpreted_section -> String_table.string_table -> bool

is_valid_elf64_section_header_table_entry sect stab checks whether a * interpreted section conforms with the prescribed flags and types declared * in the "special sections" table of the ELF specification. * TODO: some of these entries in the table are overridden by ABI supplements. * Make sure it is these that are passed in rather than the default table * declared in the spec?

val is_valid_elf32_section_header_table0 : elf32_interpreted_section list -> String_table.string_table -> bool

is_valid_elf32_section_header_table sects checks whether all entries in * sect are valid.

val is_valid_elf64_section_header_table0 : elf64_interpreted_section list -> String_table.string_table -> bool

is_valid_elf64_section_header_table sects checks whether all entries in * sect are valid.