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_amd64_section_header_table.ml.html
Source file abi_amd64_section_header_table.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(*Generated by Lem from abis/amd64/abi_amd64_section_header_table.lem.*) (** [abi_amd64_section_header_table] module contains section header table * specific definitions for the AMD64 ABI. *) open Lem_basic_classes open Lem_map open Lem_num open Elf_section_header_table (** AMD64 specific flags. See Section 4.2.1. *) let shf_abi_amd64_large : Nat_big_num.num= (Nat_big_num.mul( (Nat_big_num.of_int 67108864))( (Nat_big_num.of_int 4))) (* 0x10000000 *) (** AMD64 specific section types. See Section 4.2.2 *) let sht_abi_amd64_unwind : Nat_big_num.num= (Nat_big_num.add ( Nat_big_num.mul( (Nat_big_num.of_int 939524096))( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1))) (* 0x70000001 *) (** [string_of_abi_amd64_section_type m] produces a string based representation * of AMD64 section type [m]. *) (*val string_of_abi_amd64_section_type : natural -> string*) let string_of_abi_amd64_section_type m:string= (if Nat_big_num.equal m sht_abi_amd64_unwind then "X86_64_UNWIND" else "Invalid AMD64 section type") (** Special sections *) (*val abi_amd64_special_sections : Map.map string (natural * natural)*) let abi_amg64_special_sections:((string),(Nat_big_num.num*Nat_big_num.num))Pmap.map= (Lem_map.fromList (instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) [ (".got", (sht_progbits, Nat_big_num.add shf_alloc shf_write)) ; (".plt", (sht_progbits, Nat_big_num.add shf_alloc shf_execinstr)) ; (".eh_frame", (sht_abi_amd64_unwind, shf_alloc)) ]) (*val abi_amd64_special_sections_large_code_model : Map.map string (natural * natural)*) let abi_amd64_special_sections_large_code_model:((string),(Nat_big_num.num*Nat_big_num.num))Pmap.map= (Lem_map.fromList (instance_Map_MapKeyType_var_dict instance_Basic_classes_SetType_var_dict) [ (".lbss", (sht_nobits, Nat_big_num.add (Nat_big_num.add shf_alloc shf_write) shf_abi_amd64_large)) ; (".ldata", (sht_progbits, Nat_big_num.add (Nat_big_num.add shf_alloc shf_write) shf_abi_amd64_large)) ; (".ldata1", (sht_progbits, Nat_big_num.add (Nat_big_num.add shf_alloc shf_write) shf_abi_amd64_large)) ; (".lgot", (sht_progbits, Nat_big_num.add (Nat_big_num.add shf_alloc shf_write) shf_abi_amd64_large)) ; (".lplt", (sht_progbits, Nat_big_num.add (Nat_big_num.add shf_alloc shf_execinstr) shf_abi_amd64_large)) ; (".lrodata", (sht_progbits, Nat_big_num.add shf_alloc shf_abi_amd64_large)) ; (".lrodata1", (sht_progbits, Nat_big_num.add shf_alloc shf_abi_amd64_large)) ; (".ltext", (sht_progbits, Nat_big_num.add (Nat_big_num.add shf_alloc shf_execinstr) shf_abi_amd64_large)) ])