package linksem

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

Install 

dune-project
 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/Abi_power64_relocation/index.html

Module Abi_power64_relocationSource

abi_power64_relocation contains types and definitions specific to * relocations in the Power64 ABI

Power64 relocation types

Sourceval r_ppc64_none : Nat_big_num.num
Sourceval r_ppc64_addr32 : Nat_big_num.num
Sourceval r_ppc64_addr24 : Nat_big_num.num
Sourceval r_ppc64_addr16 : Nat_big_num.num
Sourceval r_ppc64_addr16_lo : Nat_big_num.num
Sourceval r_ppc64_addr16_hi : Nat_big_num.num
Sourceval r_ppc64_addr16_ha : Nat_big_num.num
Sourceval r_ppc64_addr14 : Nat_big_num.num
Sourceval r_ppc64_addr14_brtaken : Nat_big_num.num
Sourceval r_ppc64_addr14_brntaken : Nat_big_num.num
Sourceval r_ppc64_rel24 : Nat_big_num.num
Sourceval r_ppc64_rel14 : Nat_big_num.num
Sourceval r_ppc64_rel14_brtaken : Nat_big_num.num
Sourceval r_ppc64_rel14_brntaken : Nat_big_num.num
Sourceval r_ppc64_got16 : Nat_big_num.num
Sourceval r_ppc64_got16_lo : Nat_big_num.num
Sourceval r_ppc64_got16_hi : Nat_big_num.num
Sourceval r_ppc64_got16_ha : Nat_big_num.num
Sourceval r_ppc64_copy : Nat_big_num.num
Sourceval r_ppc64_glob_dat : Nat_big_num.num
Sourceval r_ppc64_jmp_slot : Nat_big_num.num
Sourceval r_ppc64_relative : Nat_big_num.num
Sourceval r_ppc64_uaddr32 : Nat_big_num.num
Sourceval r_ppc64_uaddr16 : Nat_big_num.num
Sourceval r_ppc64_rel32 : Nat_big_num.num
Sourceval r_ppc64_plt32 : Nat_big_num.num
Sourceval r_ppc64_pltrel32 : Nat_big_num.num
Sourceval r_ppc64_plt16_lo : Nat_big_num.num
Sourceval r_ppc64_plt16_hi : Nat_big_num.num
Sourceval r_ppc64_plt16_ha : Nat_big_num.num
Sourceval r_ppc64_sectoff : Nat_big_num.num
Sourceval r_ppc64_sectoff_lo : Nat_big_num.num
Sourceval r_ppc64_sectoff_hi : Nat_big_num.num
Sourceval r_ppc64_sectoff_ha : Nat_big_num.num
Sourceval r_ppc64_addr30 : Nat_big_num.num
Sourceval r_ppc64_addr64 : Nat_big_num.num
Sourceval r_ppc64_addr16_higher : Nat_big_num.num
Sourceval r_ppc64_addr16_highera : Nat_big_num.num
Sourceval r_ppc64_addr16_highest : Nat_big_num.num
Sourceval r_ppc64_addr16_highesta : Nat_big_num.num
Sourceval r_ppc64_uaddr64 : Nat_big_num.num
Sourceval r_ppc64_rel64 : Nat_big_num.num
Sourceval r_ppc64_plt64 : Nat_big_num.num
Sourceval r_ppc64_pltrel64 : Nat_big_num.num
Sourceval r_ppc64_toc16 : Nat_big_num.num
Sourceval r_ppc64_toc16_lo : Nat_big_num.num
Sourceval r_ppc64_toc16_hi : Nat_big_num.num
Sourceval r_ppc64_toc16_ha : Nat_big_num.num
Sourceval r_ppc64_toc : Nat_big_num.num
Sourceval r_ppc64_pltgot16 : Nat_big_num.num
Sourceval r_ppc64_pltgot16_lo : Nat_big_num.num
Sourceval r_ppc64_pltgot16_hi : Nat_big_num.num
Sourceval r_ppc64_pltgot16_ha : Nat_big_num.num
Sourceval r_ppc64_addr16_ds : Nat_big_num.num
Sourceval r_ppc64_addr16_lo_ds : Nat_big_num.num
Sourceval r_ppc64_got16_ds : Nat_big_num.num
Sourceval r_ppc64_got16_lo_ds : Nat_big_num.num
Sourceval r_ppc64_plt16_lo_ds : Nat_big_num.num
Sourceval r_ppc64_sectoff_ds : Nat_big_num.num
Sourceval r_ppc64_sectoff_lo_ds : Nat_big_num.num
Sourceval r_ppc64_toc16_ds : Nat_big_num.num
Sourceval r_ppc64_toc16_lo_ds : Nat_big_num.num
Sourceval r_ppc64_pltgot16_ds : Nat_big_num.num
Sourceval r_ppc64_pltgot16_lo_ds : Nat_big_num.num
Sourceval r_ppc64_tls : Nat_big_num.num
Sourceval r_ppc64_dtpmod64 : Nat_big_num.num
Sourceval r_ppc64_tprel16 : Nat_big_num.num
Sourceval r_ppc64_tprel16_lo : Nat_big_num.num
Sourceval r_ppc64_tprel16_hi : Nat_big_num.num
Sourceval r_ppc64_tprel16_ha : Nat_big_num.num
Sourceval r_ppc64_tprel64 : Nat_big_num.num
Sourceval r_ppc64_dtprel16 : Nat_big_num.num
Sourceval r_ppc64_dtprel16_lo : Nat_big_num.num
Sourceval r_ppc64_dtprel16_hi : Nat_big_num.num
Sourceval r_ppc64_dtprel16_ha : Nat_big_num.num
Sourceval r_ppc64_dtprel64 : Nat_big_num.num
Sourceval r_ppc64_got_tlsgd16 : Nat_big_num.num
Sourceval r_ppc64_got_tlsgd16_lo : Nat_big_num.num
Sourceval r_ppc64_got_tlsgd16_hi : Nat_big_num.num
Sourceval r_ppc64_got_tlsgd16_ha : Nat_big_num.num
Sourceval r_ppc64_got_tlsld16 : Nat_big_num.num
Sourceval r_ppc64_got_tlsld16_lo : Nat_big_num.num
Sourceval r_ppc64_got_tlsld16_hi : Nat_big_num.num
Sourceval r_ppc64_got_tlsld16_ha : Nat_big_num.num
Sourceval r_ppc64_got_tprel16_ds : Nat_big_num.num
Sourceval r_ppc64_got_tprel16_lo_ds : Nat_big_num.num
Sourceval r_ppc64_got_tprel16_hi : Nat_big_num.num
Sourceval r_ppc64_got_tprel16_ha : Nat_big_num.num
Sourceval r_ppc64_got_dtprel16_ds : Nat_big_num.num
Sourceval r_ppc64_got_dtprel16_lo_ds : Nat_big_num.num
Sourceval r_ppc64_got_dtprel16_hi : Nat_big_num.num
Sourceval r_ppc64_got_dtprel16_ha : Nat_big_num.num
Sourceval r_ppc64_tprel16_ds : Nat_big_num.num
Sourceval r_ppc64_tprel16_lo_ds : Nat_big_num.num
Sourceval r_ppc64_tprel16_higher : Nat_big_num.num
Sourceval r_ppc64_tprel16_highera : Nat_big_num.num
Sourceval r_ppc64_tprel16_highest : Nat_big_num.num
Sourceval r_ppc64_tprel16_highesta : Nat_big_num.num
Sourceval r_ppc64_dtprel16_ds : Nat_big_num.num
Sourceval r_ppc64_dtprel16_lo_ds : Nat_big_num.num
Sourceval r_ppc64_dtprel16_higher : Nat_big_num.num
Sourceval r_ppc64_dtprel16_highera : Nat_big_num.num
Sourceval r_ppc64_dtprel16_highest : Nat_big_num.num
Sourceval r_ppc64_dtprel16_highesta : Nat_big_num.num
Sourceval string_of_ppc64_relocation_type : Nat_big_num.num -> string

string_of_ppc64_relocation_type rel_type produces a string representation * of relocation type rel_type.

Sourceval abi_ppc64_apply_relocation : Elf_relocation.elf64_relocation_a -> 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 -> Nat_big_num.num -> 'a -> Nat_big_num.num -> Nat_big_num.num -> Elf_file.elf64_file -> (Uint64_wrapper.uint64, Nat_big_num.num Abi_utilities.relocation_operator_expression * Abi_utilities.integer_bit_width * Nat_big_num.num Abi_utilities.can_fail) Pmap.map Error.error