linksem 0.7 · OCaml Package

type elf32_interpreted_section = {

elf32_section_name : Nat_big_num.num;
elf32_section_type : Nat_big_num.num;
elf32_section_flags : Nat_big_num.num;
elf32_section_addr : Nat_big_num.num;
elf32_section_offset : Nat_big_num.num;
elf32_section_size : Nat_big_num.num;
elf32_section_link : Nat_big_num.num;
elf32_section_info : Nat_big_num.num;
elf32_section_align : Nat_big_num.num;
elf32_section_entsize : Nat_big_num.num;
elf32_section_body : Byte_sequence.byte_sequence0;
elf32_section_name_as_string : string;

}

val elf32_interpreted_section_equal : 
  elf32_interpreted_section ->
  elf32_interpreted_section ->
  bool

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;
elf64_section_type : Nat_big_num.num;
elf64_section_flags : Nat_big_num.num;
elf64_section_addr : Nat_big_num.num;
elf64_section_offset : Nat_big_num.num;
elf64_section_size : Nat_big_num.num;
elf64_section_link : Nat_big_num.num;
elf64_section_info : Nat_big_num.num;
elf64_section_align : Nat_big_num.num;
elf64_section_entsize : Nat_big_num.num;
elf64_section_body : Byte_sequence.byte_sequence0;
elf64_section_name_as_string : string;

}

val compare_elf64_interpreted_section : 
  elf64_interpreted_section ->
  elf64_interpreted_section ->
  int

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

val null_elf32_interpreted_section : elf32_interpreted_section

val null_elf64_interpreted_section : elf64_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

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

val string_of_elf64_interpreted_section : elf64_interpreted_section -> string

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

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

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

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

package linksem