package linksem

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

elf_interpreted_segment defines interpreted segments, i.e. the contents of * a program header table entry converted to more amenable types, and operations * built on top of them.

type elf32_interpreted_segment = {
  1. elf32_segment_body : Byte_sequence.byte_sequence0;
    (*

    Body of the segment

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

    Type of the segment

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

    Size of the segment in bytes

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

    Size of the segment in memory in bytes

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

    Base address of the segment

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

    Physical address of segment

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

    Alignment of the segment

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

    Offset of the segment

    *)
  9. elf32_segment_flags : bool * bool * bool;
    (*

    READ, WRITE, EXECUTE flags.

    *)
}

elf32_interpreted_segment represents an ELF32 interpreted segment, i.e. the * contents of an ELF program header table entry converted into more amenable * (infinite precision) types, for manipulation. * Invariant: the nth entry of the program header table corresponds to the nth * entry of the list of interpreted segments in an elf32_file record. The * lengths of the two lists are exactly the same.

type elf64_interpreted_segment = {
  1. elf64_segment_body : Byte_sequence.byte_sequence0;
    (*

    Body of the segment

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

    Type of the segment

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

    Size of the segment in bytes

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

    Size of the segment in memory in bytes

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

    Base address of the segment

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

    Physical address of segment

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

    Alignment of the segment

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

    Offset of the segment

    *)
  9. elf64_segment_flags : bool * bool * bool;
    (*

    READ, WRITE, EXECUTE flags.

    *)
}

elf64_interpreted_segment represents an ELF64 interpreted segment, i.e. the * contents of an ELF program header table entry converted into more amenable * (infinite precision) types, for manipulation. * Invariant: the nth entry of the program header table corresponds to the nth * entry of the list of interpreted segments in an elf64_file record. The * lengths of the two lists are exactly the same.

val compare_elf64_interpreted_segment : elf64_interpreted_segment -> elf64_interpreted_segment -> int

compare_elf64_interpreted_segment seg1 seg2 is an ordering comparison function * on interpreted segments suitable for constructing sets, finite maps and other * ordered data types out of.

val instance_Basic_classes_Ord_Elf_interpreted_segment_elf64_interpreted_segment_dict : elf64_interpreted_segment Lem_basic_classes.ord_class
type elf32_interpreted_segments = elf32_interpreted_segment list
type elf64_interpreted_segments = elf64_interpreted_segment list
val string_of_flags : (bool * bool * bool) -> string

string_of_flags bs produces a string-based representation of an interpreted * segments flags (represented as a boolean triple).

val string_of_elf32_interpreted_segment : elf32_interpreted_segment -> string

string_of_elf32_interpreted_segment seg produces a string-based representation * of interpreted segment seg.

val string_of_elf64_interpreted_segment : elf64_interpreted_segment -> string

string_of_elf64_interpreted_segment seg produces a string-based representation * of interpreted segment seg.