package linksem

  1. Overview
  2. Docs
package linksem
Legend:
Library
Module
Module type
Parameter
Class
Class type
type elf32_interpreted_section = {
  1. elf32_section_name : Nat_big_num.num;
  2. elf32_section_type : Nat_big_num.num;
  3. elf32_section_flags : Nat_big_num.num;
  4. elf32_section_addr : Nat_big_num.num;
  5. elf32_section_offset : Nat_big_num.num;
  6. elf32_section_size : Nat_big_num.num;
  7. elf32_section_info : Nat_big_num.num;
  8. elf32_section_align : Nat_big_num.num;
  9. elf32_section_entsize : Nat_big_num.num;
  10. elf32_section_body : Byte_sequence.byte_sequence0;
  11. 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 = {
  1. elf64_section_name : Nat_big_num.num;
  2. elf64_section_type : Nat_big_num.num;
  3. elf64_section_flags : Nat_big_num.num;
  4. elf64_section_addr : Nat_big_num.num;
  5. elf64_section_offset : Nat_big_num.num;
  6. elf64_section_size : Nat_big_num.num;
  7. elf64_section_info : Nat_big_num.num;
  8. elf64_section_align : Nat_big_num.num;
  9. elf64_section_entsize : Nat_big_num.num;
  10. elf64_section_body : Byte_sequence.byte_sequence0;
  11. 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