Module Abis

val is_valid_abi_aarch64_relocation_operator : Abi_utilities.relocation_operator -> bool
val is_valid_abi_aarch64_relocation_operator2 : Abi_utilities.relocation_operator2 -> bool
val is_valid_abi_amd64_relocation_operator : Abi_utilities.relocation_operator -> bool
val is_valid_abi_amd64_relocation_operator2 : 'a -> bool
val is_valid_abi_power64_relocation_operator : 'a -> bool
val is_valid_abi_power64_relocation_operator2 : 'a -> bool
type any_abi_feature =
| Amd64AbiFeature of any_abi_feature Abi_amd64.amd64_abi_feature
| Aarch64LeAbiFeature of Abi_aarch64_le.aarch64_le_abi_feature
val anyAbiFeatureCompare : any_abi_feature -> any_abi_feature -> int
val anyAbiFeatureTagEquiv : any_abi_feature -> any_abi_feature -> bool
val instance_Basic_classes_Ord_Abis_any_abi_feature_dict : any_abi_feature Lem_basic_classes.ord_class
val instance_Abi_classes_AbiFeatureTagEquiv_Abis_any_abi_feature_dict : any_abi_feature Abi_classes.abiFeatureTagEquiv_class
val make_elf64_header : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Elf_header.elf64_header
val phdr_flags_from_section_flags : Nat_big_num.num -> 'a -> Nat_big_num.num
val phdr_is_writable : Nat_big_num.num -> bool
type can_combine_flags_fn = Nat_big_num.num Pset.set -> Nat_big_num.num option
val load_can_combine_flags : Nat_big_num.num Pset.set -> Nat_big_num.num option
val tls_can_combine_flags : Nat_big_num.num Pset.set -> Nat_big_num.num option
val maybe_extend_phdr : Elf_program_header_table.elf64_program_header_table_entry -> Elf_interpreted_section.elf64_interpreted_section -> (Nat_big_num.num Pset.set -> Nat_big_num.num option) -> Elf_program_header_table.elf64_program_header_table_entry option
val make_new_phdr : Elf_interpreted_section.elf64_interpreted_section -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Elf_program_header_table.elf64_program_header_table_entry
val make_load_phdrs : Nat_big_num.num -> Nat_big_num.num -> 'a -> Elf_interpreted_section.elf64_interpreted_section list -> Elf_program_header_table.elf64_program_header_table_entry list
val tls_extend : 'abifeature Memory_image.abi -> 'abifeature Memory_image.abi
val make_default_phdrs : Nat_big_num.num -> Nat_big_num.num -> 'a -> 'b -> Elf_interpreted_section.elf64_interpreted_section list -> Elf_program_header_table.elf64_program_header_table_entry list
val find_start_symbol_address : 'a Lem_basic_classes.ord_class -> 'a Abi_classes.abiFeatureTagEquiv_class -> 'a Memory_image.annotated_memory_image -> Nat_big_num.num option
val pad_zeroes : Nat_big_num.num -> char list
val pad_0x90 : Nat_big_num.num -> char list
val null_abi : any_abi_feature Memory_image.abi
val got_entry_ordering : ('a * 'b) -> ('a * 'c) -> int
val is_ifunc_def : Memory_image.symbol_definition option -> bool
val amd64_reloc_needs_got_slot : 'a -> Memory_image.reloc_site -> Memory_image.symbol_definition option -> bool
val amd64_reloc_needs_plt_slot : Memory_image.symbol_reference_and_reloc_site -> Memory_image.reloc_site -> Memory_image.symbol_definition option -> (Memory_image.reloc_site -> bool) -> bool
val amd64_find_got_label_and_element : any_abi_feature Memory_image.annotated_memory_image -> ((string * Memory_image.symbol_definition option) list * Memory_image.element) option
val amd64_find_plt_label_and_element : any_abi_feature Memory_image.annotated_memory_image -> ((string * Memory_image.symbol_definition option * any_abi_feature Abi_amd64.plt_entry_content_fn) list * Memory_image.element) option
val got_slot_index_for_symname : 'a Lem_basic_classes.eq_class -> 'a -> ('a * 'b) list -> int option
val amd64_get_reloc_symaddr : Memory_image.symbol_definition -> any_abi_feature Memory_image.annotated_memory_image -> (Memory_image.element_range option * Memory_image.symbol_definition) list -> 'a -> Nat_big_num.num
val amd64_generate_support : ('a * any_abi_feature Memory_image.annotated_memory_image) list -> any_abi_feature Memory_image.annotated_memory_image
val amd64_concretise_support : any_abi_feature Memory_image.annotated_memory_image -> any_abi_feature Memory_image.annotated_memory_image
val amd64_got_slot_idx : any_abi_feature Memory_image.annotated_memory_image -> Memory_image.symbol_reference_and_reloc_site -> Nat_big_num.num
val amd64_got_slot_addr : any_abi_feature Memory_image.annotated_memory_image -> Memory_image.symbol_reference_and_reloc_site -> Nat_big_num.num
val amd64_plt_slot_addr : any_abi_feature Memory_image.annotated_memory_image -> Memory_image.symbol_reference_and_reloc_site -> Nat_big_num.num -> Nat_big_num.num
val amd64_base_addr : Memory_image.symbol_reference_and_reloc_site -> Nat_big_num.num -> Nat_big_num.num
val amd64_reloc : Nat_big_num.num -> bool * (any_abi_feature Memory_image.annotated_memory_image -> Nat_big_num.num -> Memory_image.symbol_reference_and_reloc_site -> Nat_big_num.num * (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num))
val sysv_amd64_std_abi : any_abi_feature Memory_image.abi
val sysv_aarch64_le_std_abi : any_abi_feature Memory_image.abi
val sysv_mips64_std_abi : any_abi_feature Memory_image.abi
val sysv_cheri_mips64_std_abi : any_abi_feature Memory_image.abi
val all_abis : any_abi_feature Memory_image.abi list