package linksem

  1. Overview
  2. Docs
A formalisation of the core ELF and DWARF file formats written in Lem

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

  1. S
    Stephen Kell
  2. D
    Dominic Mulligan
  3. P
    Peter Sewell

Maintainers

  1. L
    Linksem Devs <cl-linksem-dev@lists.cam.ac.uk>

Sources

0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2

doc/linksem_zarith/Harness_interface/index.html

Module Harness_interfaceSource

Sourceval concatS' : string list -> string -> string
Sourceval concatS : string list -> string
Sourceval harness_string_of_elf32_file_header : Elf_header.elf32_header -> string
Sourceval harness_string_of_elf64_file_header : Elf_header.elf64_header -> string
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval harness_sht32_flag_legend : string
Sourceval harness_sht64_flag_legend : Nat_big_num.num -> string
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval harness_string_of_elf32_relocs : Elf_file.elf32_file -> (Nat_big_num.num -> string) -> Byte_sequence_wrapper.byte_sequence -> string
Sourceval harness_string_of_elf64_relocs : Elf_file.elf64_file -> (Nat_big_num.num -> string) -> Byte_sequence_wrapper.byte_sequence -> string
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval string_of_dyn_value : ('a, 'b) Elf_dynamic.dyn_value -> ('a -> string) -> ('b -> string) -> string
Sourceval string_of_elf32_dyn_value : (Uint32_wrapper.uint32, Nat_big_num.num) Elf_dynamic.dyn_value -> string
Sourceval string_of_elf64_dyn_value : (Nat_big_num.num, Nat_big_num.num) Elf_dynamic.dyn_value -> string
Sourceval 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
Sourceval 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct