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_program_header_table.ml.html
Source file abi_amd64_program_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(*Generated by Lem from abis/amd64/abi_amd64_program_header_table.lem.*) (** [abi_amd64_program_header_table], program header table specific definitions * for the AMD64 ABI. *) open Lem_basic_classes open Lem_bool open Lem_num open Lem_string (** New segment types. *) (** The segment contains the stack unwind tables *) let abi_amd64_pt_gnu_eh_frame : Nat_big_num.num= (Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 842691240))) (* 0x6474e550 *) let abi_amd64_pt_sunw_eh_frame : Nat_big_num.num= (Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 842691240))) (* 0x6474e550 *) let abi_amd64_pt_sunw_unwind : Nat_big_num.num= (Nat_big_num.mul( (Nat_big_num.of_int 2))( (Nat_big_num.of_int 842691240))) (* 0x6474e550 *) (** [string_of_abi_amd64_elf_segment_type m] produces a string based representation * of AMD64 segment type [m]. *) (*val string_of_abi_amd64_elf_segment_type : natural -> string*) let string_of_abi_amd64_elf_segment_type m:string= (if Nat_big_num.equal m abi_amd64_pt_gnu_eh_frame then "GNU_EH_FRAME" else if Nat_big_num.equal m abi_amd64_pt_sunw_eh_frame then "SUNW_EH_FRAME" else if Nat_big_num.equal m abi_amd64_pt_sunw_unwind then "SUNW_UNWIND" else "Invalid AMD64 segment type") (** [abi_amd64_is_valid_program_interpreter s] checks whether the program interpreter * string is valid for AMD64 ABI. * See Section 5.2.1 *) (*val abi_amd64_is_valid_program_interpreter : string -> bool*) let abi_amd64_is_valid_program_interpreter s:bool= ((s = "/lib/ld64.so.1") || (s = "/lib64/ld-linux-x86-64.so.2"))