package linksem

You can search for identifiers within the package.

in-package search v0.2.0

linksem_zarith

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 = {

elf32_segment_body : Byte_sequence.byte_sequence0;
(*
Body of the segment
*)
elf32_segment_type : Nat_big_num.num;
(*
Type of the segment
*)
elf32_segment_size : Nat_big_num.num;
(*
Size of the segment in bytes
*)
elf32_segment_memsz : Nat_big_num.num;
(*
Size of the segment in memory in bytes
*)
elf32_segment_base : Nat_big_num.num;
(*
Base address of the segment
*)
elf32_segment_paddr : Nat_big_num.num;
(*
Physical address of segment
*)
elf32_segment_align : Nat_big_num.num;
(*
Alignment of the segment
*)
elf32_segment_offset : Nat_big_num.num;
(*
Offset of the segment
*)
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 = {

elf64_segment_body : Byte_sequence.byte_sequence0;
(*
Body of the segment
*)
elf64_segment_type : Nat_big_num.num;
(*
Type of the segment
*)
elf64_segment_size : Nat_big_num.num;
(*
Size of the segment in bytes
*)
elf64_segment_memsz : Nat_big_num.num;
(*
Size of the segment in memory in bytes
*)
elf64_segment_base : Nat_big_num.num;
(*
Base address of the segment
*)
elf64_segment_paddr : Nat_big_num.num;
(*
Physical address of segment
*)
elf64_segment_align : Nat_big_num.num;
(*
Alignment of the segment
*)
elf64_segment_offset : Nat_big_num.num;
(*
Offset of the segment
*)
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.