package linksem
A formalisation of the core ELF and DWARF file formats written in Lem
Install
Dune Dependency
Authors
Maintainers
Sources
0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/linksem_zarith/Harness_interface/index.html
Module Harness_interface
Source
Source
val harness_string_of_elf32_program_header_table_entry :
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
Byte_sequence_wrapper.byte_sequence ->
Elf_program_header_table.elf32_program_header_table_entry ->
string
Source
val harness_string_of_elf64_program_header_table_entry :
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
Byte_sequence_wrapper.byte_sequence ->
Elf_program_header_table.elf64_program_header_table_entry ->
string
Source
val harness_string_of_elf32_pht :
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
Elf_program_header_table.elf32_program_header_table_entry list ->
Byte_sequence_wrapper.byte_sequence ->
string
Source
val harness_string_of_elf64_pht :
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
Elf_program_header_table.elf64_program_header_table_entry list ->
Byte_sequence_wrapper.byte_sequence ->
string
Source
val harness_string_of_elf32_segment_section_mappings :
Elf_header.elf32_header ->
Elf_program_header_table.elf32_program_header_table_entry list ->
Elf_section_header_table.elf32_section_header_table_entry list ->
String_table.string_table ->
string
Source
val harness_string_of_elf64_segment_section_mappings :
Elf_header.elf64_header ->
Elf_program_header_table.elf64_program_header_table_entry list ->
Elf_section_header_table.elf64_section_header_table_entry list ->
String_table.string_table ->
string
Source
val harness_string_of_elf32_program_headers :
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
Elf_header.elf32_header ->
Elf_program_header_table.elf32_program_header_table_entry list ->
Elf_section_header_table.elf32_section_header_table_entry list ->
String_table.string_table ->
Byte_sequence_wrapper.byte_sequence ->
string
Source
val harness_string_of_elf64_program_headers :
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
Elf_header.elf64_header ->
Elf_program_header_table.elf64_program_header_table_entry list ->
Elf_section_header_table.elf64_section_header_table_entry list ->
String_table.string_table ->
Byte_sequence_wrapper.byte_sequence ->
string
Source
val harness_string_of_elf32_sht :
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
Elf_section_header_table.elf32_section_header_table_entry list ->
String_table.string_table ->
string
Source
val harness_string_of_elf64_sht :
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
Elf_section_header_table.elf64_section_header_table_entry list ->
String_table.string_table ->
string
Source
val harness_string_of_elf32_section_headers :
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
Elf_header.elf32_header ->
Elf_section_header_table.elf32_section_header_table_entry list ->
String_table.string_table ->
string
Source
val harness_string_of_elf64_section_headers :
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
Elf_header.elf64_header ->
Elf_section_header_table.elf64_section_header_table_entry list ->
String_table.string_table ->
string
Source
val harness_string_of_elf32_reloc_entry :
(Nat_big_num.num -> string) ->
Elf_section_header_table.elf32_section_header_table_entry list ->
Elf_symbol_table.elf32_symbol_table_entry list ->
String_table.string_table ->
String_table.string_table ->
Elf_relocation.elf32_relocation ->
string
Source
val harness_string_of_elf64_reloc_a_entry :
(Nat_big_num.num -> string) ->
Elf_symbol_table.elf64_symbol_table_entry list ->
Elf_section_header_table.elf64_section_header_table_entry list ->
String_table.string_table ->
String_table.string_table ->
Elf_relocation.elf64_relocation_a ->
string
Source
val harness_string_of_elf32_relocs' :
Endianness.endianness ->
(Nat_big_num.num -> string) ->
Elf_file.elf32_file ->
Elf_section_header_table.elf32_section_header_table_entry list ->
Elf_section_header_table.elf32_section_header_table_entry list ->
String_table.string_table ->
String_table.string_table ->
Byte_sequence_wrapper.byte_sequence ->
string
Source
val harness_string_of_elf64_relocs' :
Endianness.endianness ->
(Nat_big_num.num -> string) ->
Elf_file.elf64_file ->
Elf_section_header_table.elf64_section_header_table_entry list ->
Elf_section_header_table.elf64_section_header_table_entry list ->
String_table.string_table ->
String_table.string_table ->
Byte_sequence_wrapper.byte_sequence ->
string
Source
val harness_string_of_elf32_relocs :
Elf_file.elf32_file ->
(Nat_big_num.num -> string) ->
Byte_sequence_wrapper.byte_sequence ->
string
Source
val harness_string_of_elf64_relocs :
Elf_file.elf64_file ->
(Nat_big_num.num -> string) ->
Byte_sequence_wrapper.byte_sequence ->
string
Source
val harness_string_of_elf32_symbol_table_entry :
int ->
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
'a ->
String_table.string_table ->
Elf_symbol_table.elf32_symbol_table_entry ->
string
Source
val harness_string_of_elf32_syms' :
Endianness.endianness ->
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
Elf_file.elf32_file ->
Elf_section_header_table.elf32_section_header_table_entry list ->
'a ->
String_table.string_table ->
Byte_sequence_wrapper.byte_sequence ->
string
Source
val harness_string_of_elf32_syms :
Elf_file.elf32_file ->
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
Byte_sequence_wrapper.byte_sequence ->
string
Source
val harness_string_of_elf64_symbol_table_entry :
int ->
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
String_table.string_table ->
Elf_symbol_table.elf64_symbol_table_entry ->
string
Source
val harness_string_of_elf64_syms' :
Endianness.endianness ->
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
Elf_file.elf64_file ->
Elf_section_header_table.elf64_section_header_table_entry list ->
'a ->
String_table.string_table ->
Byte_sequence_wrapper.byte_sequence ->
string
Source
val harness_string_of_elf64_syms :
Elf_file.elf64_file ->
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
Byte_sequence_wrapper.byte_sequence ->
string
Source
val string_of_dyn_value :
('a, 'b) Elf_dynamic.dyn_value ->
('a -> string) ->
('b -> string) ->
string
Source
val string_of_elf32_dyn_value :
(Uint32_wrapper.uint32, Nat_big_num.num) Elf_dynamic.dyn_value ->
string
Source
val string_of_elf64_dyn_value :
(Nat_big_num.num, Nat_big_num.num) Elf_dynamic.dyn_value ->
string
Source
val harness_string_of_elf32_dyn_entry :
bool ->
Elf_dynamic.elf32_dyn ->
(Nat_big_num.num -> bool) ->
(Nat_big_num.num -> string) ->
(Elf_dynamic.elf32_dyn ->
String_table.string_table ->
(Uint32_wrapper.uint32, Uint32_wrapper.uint32) Elf_dynamic.dyn_value
Error.error) ->
(Elf_dynamic.elf32_dyn ->
String_table.string_table ->
(Uint32_wrapper.uint32, Uint32_wrapper.uint32) Elf_dynamic.dyn_value
Error.error) ->
String_table.string_table ->
string
Source
val harness_string_of_elf32_dynamic_section' :
Elf_file.elf32_file ->
Elf_program_header_table.elf32_program_header_table_entry ->
Byte_sequence_wrapper.byte_sequence ->
(Nat_big_num.num -> bool) ->
(Nat_big_num.num -> Elf_dynamic.tag_correspondence Error.error) ->
(Nat_big_num.num -> Elf_dynamic.tag_correspondence Error.error) ->
(Nat_big_num.num -> string) ->
(Elf_dynamic.elf32_dyn ->
String_table.string_table ->
(Uint32_wrapper.uint32, Uint32_wrapper.uint32) Elf_dynamic.dyn_value
Error.error) ->
(Elf_dynamic.elf32_dyn ->
String_table.string_table ->
(Uint32_wrapper.uint32, Uint32_wrapper.uint32) Elf_dynamic.dyn_value
Error.error) ->
string
Source
val harness_string_of_elf32_dynamic_section :
Elf_file.elf32_file ->
Byte_sequence_wrapper.byte_sequence ->
(Nat_big_num.num -> bool) ->
(Nat_big_num.num -> Elf_dynamic.tag_correspondence Error.error) ->
(Nat_big_num.num -> Elf_dynamic.tag_correspondence Error.error) ->
(Nat_big_num.num -> string) ->
(Elf_dynamic.elf32_dyn ->
String_table.string_table ->
(Uint32_wrapper.uint32, Uint32_wrapper.uint32) Elf_dynamic.dyn_value
Error.error) ->
(Elf_dynamic.elf32_dyn ->
String_table.string_table ->
(Uint32_wrapper.uint32, Uint32_wrapper.uint32) Elf_dynamic.dyn_value
Error.error) ->
string
Source
val harness_string_of_elf64_dyn_entry :
bool ->
Elf_dynamic.elf64_dyn ->
(Nat_big_num.num -> bool) ->
(Nat_big_num.num -> string) ->
(Elf_dynamic.elf64_dyn ->
String_table.string_table ->
(Uint64_wrapper.uint64, Uint64_wrapper.uint64) Elf_dynamic.dyn_value
Error.error) ->
(Elf_dynamic.elf64_dyn ->
String_table.string_table ->
(Uint64_wrapper.uint64, Uint64_wrapper.uint64) Elf_dynamic.dyn_value
Error.error) ->
String_table.string_table ->
string
Source
val harness_string_of_elf64_dynamic_section' :
Elf_file.elf64_file ->
Elf_program_header_table.elf64_program_header_table_entry ->
Byte_sequence_wrapper.byte_sequence ->
(Nat_big_num.num -> bool) ->
(Nat_big_num.num -> Elf_dynamic.tag_correspondence Error.error) ->
(Nat_big_num.num -> Elf_dynamic.tag_correspondence Error.error) ->
(Nat_big_num.num -> string) ->
(Elf_dynamic.elf64_dyn ->
String_table.string_table ->
(Uint64_wrapper.uint64, Uint64_wrapper.uint64) Elf_dynamic.dyn_value
Error.error) ->
(Elf_dynamic.elf64_dyn ->
String_table.string_table ->
(Uint64_wrapper.uint64, Uint64_wrapper.uint64) Elf_dynamic.dyn_value
Error.error) ->
string
Source
val harness_string_of_elf64_dynamic_section :
Elf_file.elf64_file ->
Byte_sequence_wrapper.byte_sequence ->
(Nat_big_num.num -> bool) ->
(Nat_big_num.num -> Elf_dynamic.tag_correspondence Error.error) ->
(Nat_big_num.num -> Elf_dynamic.tag_correspondence Error.error) ->
(Nat_big_num.num -> string) ->
(Elf_dynamic.elf64_dyn ->
String_table.string_table ->
(Uint64_wrapper.uint64, Uint64_wrapper.uint64) Elf_dynamic.dyn_value
Error.error) ->
(Elf_dynamic.elf64_dyn ->
String_table.string_table ->
(Uint64_wrapper.uint64, Uint64_wrapper.uint64) Elf_dynamic.dyn_value
Error.error) ->
string
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>