package linksem
Install
Dune Dependency
Authors
Maintainers
Sources
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/linksem_zarith/Elf_interpreted_segment/index.html
Module Elf_interpreted_segment
Source
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
string_of_flags bs
produces a string-based representation of an interpreted * segments flags (represented as a boolean triple).
string_of_elf32_interpreted_segment seg
produces a string-based representation * of interpreted segment seg
.
string_of_elf64_interpreted_segment seg
produces a string-based representation * of interpreted segment seg
.