package linksem

You can search for identifiers within the package.

in-package search v0.2.0

linksem_zarith

Legend:
Library
Module
Module type
Parameter
Class
Class type

abi_amd64_relocation contains types and definitions relating to ABI * specific relocation functionality for the AMD64 ABI.

x86-64 relocation types.

val r_x86_64_none : Nat_big_num.num

val r_x86_64_64 : Nat_big_num.num

val r_x86_64_pc32 : Nat_big_num.num

val r_x86_64_got32 : Nat_big_num.num

val r_x86_64_plt32 : Nat_big_num.num

val r_x86_64_copy : Nat_big_num.num

val r_x86_64_glob_dat : Nat_big_num.num

val r_x86_64_jump_slot : Nat_big_num.num

val r_x86_64_relative : Nat_big_num.num

val r_x86_64_gotpcrel : Nat_big_num.num

val r_x86_64_32 : Nat_big_num.num

val r_x86_64_32s : Nat_big_num.num

val r_x86_64_16 : Nat_big_num.num

val r_x86_64_pc16 : Nat_big_num.num

val r_x86_64_8 : Nat_big_num.num

val r_x86_64_pc8 : Nat_big_num.num

val r_x86_64_dtpmod64 : Nat_big_num.num

val r_x86_64_dtpoff64 : Nat_big_num.num

val r_x86_64_tpoff64 : Nat_big_num.num

val r_x86_64_tlsgd : Nat_big_num.num

val r_x86_64_tlsld : Nat_big_num.num

val r_x86_64_dtpoff32 : Nat_big_num.num

val r_x86_64_gottpoff : Nat_big_num.num

val r_x86_64_tpoff32 : Nat_big_num.num

val r_x86_64_pc64 : Nat_big_num.num

val r_x86_64_gotoff64 : Nat_big_num.num

val r_x86_64_gotpc32 : Nat_big_num.num

val r_x86_64_size32 : Nat_big_num.num

val r_x86_64_size64 : Nat_big_num.num

val r_x86_64_gotpc32_tlsdesc : Nat_big_num.num

val r_x86_64_tlsdesc_call : Nat_big_num.num

val r_x86_64_tlsdesc : Nat_big_num.num

val r_x86_64_irelative : Nat_big_num.num

val string_of_amd64_relocation_type : Nat_big_num.num -> string

string_of_x86_64_relocation_type m produces a string representation of the * relocation type m.

val abi_amd64_apply_relocation : 
  Elf_relocation.elf64_relocation_a ->
  (string, Nat_big_num.num) Pmap.map ->
  Elf_file.elf64_file ->
  (Uint64_wrapper.uint64, Nat_big_num.num) Abi_utilities.relocation_frame
    Error.error

abi_amd64_apply_relocation rel val_map ef * calculates the effect of a relocation of type rel using relevant addresses, * offsets and fields represented by b_val, g_val, got_val, l_val, p_val, * s_val and z_val, stored in val_map with "B", "G", and so on as string * keys, which are: * * - B : Base address at which a shared-object has been loaded into memory * during execution. * - G : Represents the offset into the GOT at which the relocation's entry * will reside during execution. * - GOT: Address of the GOT. * - L : Represents the address or offset of the PLT entry for a symbol. * - P : Represents the address or offset of the storage unit being * relocated. * - S : Represents the value of the symbol whose index resides in the * relocation entry. * - Z : Represents the size of the symbol whose index resides in the * relocation entry. * * More details of the above can be found in the AMD64 ABI document's chapter * on relocations. * * The abi_amd64_apply_relocation function returns a relocation frame, either * indicating that the relocation is a copy relocation, or that some calculation * must be carried out at a certain location. See the comment above the * relocation_frame type in Abi_utilities.lem for more details.