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

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

elf32_section_name : Nat_big_num.num;
(*
Name of the section
*)
elf32_section_type : Nat_big_num.num;
(*
Type of the section
*)
elf32_section_flags : Nat_big_num.num;
(*
Flags associated with the section
*)
elf32_section_addr : Nat_big_num.num;
(*
Base address of the section in memory
*)
elf32_section_offset : Nat_big_num.num;
(*
Offset from beginning of file
*)
elf32_section_size : Nat_big_num.num;
(*
Section size in bytes
*)
elf32_section_link : Nat_big_num.num;
(*
Section header table index link
*)
elf32_section_info : Nat_big_num.num;
(*
Extra information, depends on section type
*)
elf32_section_align : Nat_big_num.num;
(*
Alignment constraints for section
*)
elf32_section_entsize : Nat_big_num.num;
(*
Size of each entry in table, if section is one
*)
elf32_section_body : Byte_sequence.byte_sequence0;
(*
Body of section
*)
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 = {

elf64_section_name : Nat_big_num.num;
(*
Name of the section
*)
elf64_section_type : Nat_big_num.num;
(*
Type of the section
*)
elf64_section_flags : Nat_big_num.num;
(*
Flags associated with the section
*)
elf64_section_addr : Nat_big_num.num;
(*
Base address of the section in memory
*)
elf64_section_offset : Nat_big_num.num;
(*
Offset from beginning of file
*)
elf64_section_size : Nat_big_num.num;
(*
Section size in bytes
*)
elf64_section_link : Nat_big_num.num;
(*
Section header table index link
*)
elf64_section_info : Nat_big_num.num;
(*
Extra information, depends on section type
*)
elf64_section_align : Nat_big_num.num;
(*
Alignment constraints for section
*)
elf64_section_entsize : Nat_big_num.num;
(*
Size of each entry in table, if section is one
*)
elf64_section_body : Byte_sequence.byte_sequence0;
(*
Body of section
*)
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.