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/src/linksem_zarith/abi_x86_relocation.ml.html
Source file abi_x86_relocation.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
(*Generated by Lem from abis/x86/abi_x86_relocation.lem.*) (** [abi_x86_relocation] contains X86 ABI specific definitions relating to * relocations. *) open Lem_basic_classes open Lem_num open Lem_string open Show (** Relocation types. *) let r_386_none : Nat_big_num.num= ( (Nat_big_num.of_int 0)) let r_386_32 : Nat_big_num.num= ( (Nat_big_num.of_int 1)) let r_386_pc32 : Nat_big_num.num= ( (Nat_big_num.of_int 2)) let r_386_got32 : Nat_big_num.num= ( (Nat_big_num.of_int 3)) let r_386_plt32 : Nat_big_num.num= ( (Nat_big_num.of_int 4)) let r_386_copy : Nat_big_num.num= ( (Nat_big_num.of_int 5)) let r_386_glob_dat : Nat_big_num.num= ( (Nat_big_num.of_int 6)) let r_386_jmp_slot : Nat_big_num.num= ( (Nat_big_num.of_int 7)) let r_386_relative : Nat_big_num.num= ( (Nat_big_num.of_int 8)) let r_386_gotoff : Nat_big_num.num= ( (Nat_big_num.of_int 9)) let r_386_gotpc : Nat_big_num.num= ( (Nat_big_num.of_int 10)) (** Found in the "wild" but not in the ABI docs: *) let r_386_tls_tpoff : Nat_big_num.num= ( (Nat_big_num.of_int 14)) let r_386_tls_dtpmod32 : Nat_big_num.num= ( (Nat_big_num.of_int 35)) let r_386_tls_dtpoff32 : Nat_big_num.num= ( (Nat_big_num.of_int 36)) let r_386_irelative : Nat_big_num.num= ( (Nat_big_num.of_int 42)) (** [string_of_x86_relocation_type m] produces a string based representation of * X86 ABI relocation type [m]. *) (*val string_of_x86_relocation_type : natural -> string*) let string_of_x86_relocation_type m:string= (if Nat_big_num.equal m r_386_none then "R_386_NONE" else if Nat_big_num.equal m r_386_32 then "R_386_32" else if Nat_big_num.equal m r_386_pc32 then "R_386_PC32" else if Nat_big_num.equal m r_386_got32 then "R_386_GOT32" else if Nat_big_num.equal m r_386_plt32 then "R_386_PLT32" else if Nat_big_num.equal m r_386_copy then "R_386_COPY" else if Nat_big_num.equal m r_386_glob_dat then "R_386_GLOB_DAT" else if Nat_big_num.equal m r_386_jmp_slot then "R_386_JUMP_SLOT" else if Nat_big_num.equal m r_386_relative then "R_386_RELATIVE" else if Nat_big_num.equal m r_386_gotoff then "R_386_GOTOFF" else if Nat_big_num.equal m r_386_gotpc then "R_386_GOTPC" else if Nat_big_num.equal m r_386_tls_tpoff then "R_386_TLS_TPOFF" else if Nat_big_num.equal m r_386_tls_dtpmod32 then "R_386_TLS_DTPMOD32" else if Nat_big_num.equal m r_386_tls_dtpoff32 then "R_386_TLS_DTPOFF32" else if Nat_big_num.equal m r_386_irelative then "R_386_IRELATIVE" else "Invalid x86 relocation")
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>