package linksem

  1. Overview
  2. Docs
package linksem
Legend:
Library
Module
Module type
Parameter
Class
Class type

unsigned char type and bindings

string_of_unsigned_char uc provides a string representation of unsigned * char uc (in base 10).

natural_of_unsigned_char uc converts an unsigned char uc into a natural.

unsigned_char_of_natural i converts a natural into an unsigned char, wrapping * around if the size of the nat exceeds the storage capacity of an unsigned * char.

unsigned_char_land uc0 uc1 bitwise ANDs two unsigned chars, uc0 and uc1 * together.

unsigned_char_lor uc0 uc1 bitwise OR two unsigned chars, uc0 and uc1 * together.

unsigned_char_lshift uc n performs a left bitshift of n places on unsigned * char uc.

unsigned_char_rshift uc n performs a right bitshift of n places on unsigned * char uc.

unsigned_char_plus uc0 uc1 adds two unsigned chars, uc0 and uc1.

val natural_of_byte : char -> Nat_big_num.num

read_unsigned_char end bs0 reads an unsigned char from byte_sequence bs0 * assuming endianness end. Returns the unsigned char and the remainder of * the byte_sequence. Fails if an unsigned char cannot be read from the byte_sequence, * e.g. if bs0 is too small.

val bytes_of_unsigned_char : Nat_big_num.num -> char list
val instance_Basic_classes_Eq_Elf_types_native_uint_unsigned_char_dict : Uint32_wrapper.uint32 Lem_basic_classes.eq_class
val instance_Show_Show_Elf_types_native_uint_unsigned_char_dict : Uint32_wrapper.uint32 Show.show_class

ELF address type: * 4 byte unsigned type on 32-bit architectures. * 8 byte unsigned type on 64-bit architectures.

val bytes_of_elf32_addr : Endianness.endianness -> Nat_big_num.num -> char list
val instance_Basic_classes_Eq_Elf_types_native_uint_elf32_addr_dict : Uint32_wrapper.uint32 Lem_basic_classes.eq_class
val instance_Show_Show_Elf_types_native_uint_elf32_addr_dict : Uint32_wrapper.uint32 Show.show_class

elf64_addr type and bindings

val bytes_of_elf64_addr : Endianness.endianness -> Nat_big_num.num -> char list
val instance_Basic_classes_Eq_Elf_types_native_uint_elf64_addr_dict : Uint64_wrapper.uint64 Lem_basic_classes.eq_class
val instance_Show_Show_Elf_types_native_uint_elf64_addr_dict : Uint64_wrapper.uint64 Show.show_class

ELF half word type: * 2 byte unsigned type on 32-bit architectures. * 2 byte unsigned type on 64-bit architectures.

val bytes_of_elf32_half : Endianness.endianness -> Nat_big_num.num -> char list
val instance_Basic_classes_Eq_Elf_types_native_uint_elf32_half_dict : Uint32_wrapper.uint32 Lem_basic_classes.eq_class
val instance_Show_Show_Elf_types_native_uint_elf32_half_dict : Uint32_wrapper.uint32 Show.show_class

elf64_half type and bindings

val bytes_of_elf64_half : Endianness.endianness -> Nat_big_num.num -> char list
val instance_Basic_classes_Eq_Elf_types_native_uint_elf64_half_dict : Uint32_wrapper.uint32 Lem_basic_classes.eq_class
val instance_Show_Show_Elf_types_native_uint_elf64_half_dict : Uint32_wrapper.uint32 Show.show_class

ELF offset type: * 4 byte unsigned type on 32-bit architectures. * 8 byte unsigned type on 64-bit architectures.

val bytes_of_elf32_off : Endianness.endianness -> Nat_big_num.num -> char list
val instance_Basic_classes_Eq_Elf_types_native_uint_elf32_off_dict : Uint32_wrapper.uint32 Lem_basic_classes.eq_class
val instance_Show_Show_Elf_types_native_uint_elf32_off_dict : Uint32_wrapper.uint32 Show.show_class

elf64_off type and bindings

val bytes_of_elf64_off : Endianness.endianness -> Nat_big_num.num -> char list
val instance_Basic_classes_Eq_Elf_types_native_uint_elf64_off_dict : Uint64_wrapper.uint64 Lem_basic_classes.eq_class
val instance_Show_Show_Elf_types_native_uint_elf64_off_dict : Uint64_wrapper.uint64 Show.show_class

ELF word type: * 4 byte unsigned type on 32-bit architectures. * 4 byte unsigned type on 64-bit architectures.

val bytes_of_elf32_word : Endianness.endianness -> Nat_big_num.num -> char list
val instance_Basic_classes_Eq_Elf_types_native_uint_elf32_word_dict : Uint32_wrapper.uint32 Lem_basic_classes.eq_class
val instance_Show_Show_Elf_types_native_uint_elf32_word_dict : Uint32_wrapper.uint32 Show.show_class

elf64_word type and bindings

val bytes_of_elf64_word : Endianness.endianness -> Nat_big_num.num -> char list
val instance_Basic_classes_Eq_Elf_types_native_uint_elf64_word_dict : Uint32_wrapper.uint32 Lem_basic_classes.eq_class
val instance_Show_Show_Elf_types_native_uint_elf64_word_dict : Uint32_wrapper.uint32 Show.show_class

ELF signed word type: * 4 byte signed type on 32-bit architectures. * 4 byte signed type on 64-bit architectures.

val bytes_of_elf32_sword : Endianness.endianness -> Stdlib.Int32.t -> char list
val instance_Show_Show_Elf_types_native_uint_elf32_sword_dict : Stdlib.Int32.t Show.show_class

elf64_sword type and bindings

val bytes_of_elf64_sword : Endianness.endianness -> Stdlib.Int32.t -> char list
val instance_Show_Show_Elf_types_native_uint_elf64_sword_dict : Stdlib.Int32.t Show.show_class

ELF extra wide word type: * 8 byte unsigned type on 64-bit architectures.

val bytes_of_elf64_xword : Endianness.endianness -> Nat_big_num.num -> char list
val instance_Basic_classes_Eq_Elf_types_native_uint_elf64_xword_dict : Uint64_wrapper.uint64 Lem_basic_classes.eq_class
val instance_Show_Show_Elf_types_native_uint_elf64_xword_dict : Uint64_wrapper.uint64 Show.show_class

ELF signed extra wide word type: * 8 byte signed type on 64-bit architectures.

val bytes_of_elf64_sxword : Endianness.endianness -> Stdlib.Int64.t -> char list
val instance_Show_Show_Elf_types_native_uint_elf64_sxword_dict : Stdlib.Int64.t Show.show_class