package linksem
Install
Dune Dependency
Authors
Maintainers
Sources
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/linksem_zarith/Elf_header/index.html
Module Elf_headerSource
elf_header includes types, functions and other definitions for working with * ELF headers.
Special section header table indices
shn_undef: marks an undefined, missing or irrelevant section reference. * Present here instead of in elf_section_header_table.lem because a calculation * below requires this constant (i.e. forward reference in the ELF spec).
shn_xindex: an escape value. It indicates the actual section header index * is too large to fit in the containing field and is located in another * location (specific to the structure where it appears). Present here instead * of in elf_section_header_table.lem because a calculation below requires this * constant (i.e. forward reference in the ELF spec).
ELF object file types. Enumerates the ELF object file types specified in the * System V ABI. Values between elf_ft_lo_os and elf_ft_hi_os inclusive are * reserved for operating system specific values typically defined in an * addendum to the System V ABI for that operating system. Values between * elf_ft_lo_proc and elf_ft_hi_proc inclusive are processor specific and * are typically defined in an addendum to the System V ABI for that processor * series.
No file type
Relocatable file
Relocatable file
Executable file
Executable file
Shared object file
Shared object file
Core file
Core file
Operating-system specific
Operating-system specific
Operating-system specific
Operating-system specific
Processor specific
Processor specific
Processor specific
Processor specific
val string_of_elf_file_type :
(Nat_big_num.num -> string) ->
(Nat_big_num.num -> string) ->
Nat_big_num.num ->
stringstring_of_elf_file_type os proc m produces a string representation of the * numeric encoding m of the ELF file type. For values reserved for OS or * processor specific values, the higher-order functions os and proc are * used for printing, respectively.
is_operating_specific_file_type_value checks whether a numeric value is * reserved by the ABI for operating system-specific purposes.
is_processor_specific_file_type_value checks whether a numeric value is * reserved by the ABI for processor-specific purposes.
ELF machine architectures
RISC-V
AMD GPU architecture
AMD GPU architecture
Moxie processor family
Moxie processor family
FTDI Chip FT32 high performance 32-bit RISC architecture
FTDI Chip FT32 high performance 32-bit RISC architecture
Controls and Data Services VISIUMcore processor
Controls and Data Services VISIUMcore processor
Zilog Z80
Zilog Z80
CSR Kalimba architecture family
CSR Kalimba architecture family
Nanoradio optimised RISC
Nanoradio optimised RISC
iCelero CoolEngine
iCelero CoolEngine
Cognitive Smart Memory Processor
Cognitive Smart Memory Processor
Paneve CDP architecture family
Paneve CDP architecture family
KM211 KVARC processor
KM211 KVARC processor
KM211 KMX8 8-bit processor
KM211 KMX8 8-bit processor
KM211 KMX16 16-bit processor
KM211 KMX16 16-bit processor
KM211 KMX32 32-bit processor
KM211 KMX32 32-bit processor
KM211 KM32 32-bit processor
KM211 KM32 32-bit processor
Microchip 8-bit PIC(r) family
Microchip 8-bit PIC(r) family
XMOS xCORE processor family
XMOS xCORE processor family
Beyond BA2 CPU architecture
Beyond BA2 CPU architecture
Beyond BA1 CPU architecture
Beyond BA1 CPU architecture
Freescale 56800EX Digital Signal Controller (DSC)
Freescale 56800EX Digital Signal Controller (DSC)
199 Renesas 78KOR family
199 Renesas 78KOR family
Broadcom VideoCore V processor
Broadcom VideoCore V processor
Renesas RL78 family
Renesas RL78 family
Open8 8-bit RISC soft processing core
Open8 8-bit RISC soft processing core
Synopsys ARCompact V2
Synopsys ARCompact V2
KIPO_KAIST Core-A 2nd generation processor family
KIPO_KAIST Core-A 2nd generation processor family
KIPO_KAIST Core-A 1st generation processor family
KIPO_KAIST Core-A 1st generation processor family
CloudShield architecture family
CloudShield architecture family
Infineon Technologies SLE9X core
Infineon Technologies SLE9X core
Intel L10M
Intel L10M
Intel K10M
Intel K10M
ARM 64-bit architecture (AARCH64)
ARM 64-bit architecture (AARCH64)
Atmel Corporation 32-bit microprocessor family
Atmel Corporation 32-bit microprocessor family
STMicroelectronics STM8 8-bit microcontroller
STMicroelectronics STM8 8-bit microcontroller
Tilera TILE64 multicore architecture family
Tilera TILE64 multicore architecture family
Tilera TILEPro multicore architecture family
Tilera TILEPro multicore architecture family
Xilinix MicroBlaze 32-bit RISC soft processor core
Xilinix MicroBlaze 32-bit RISC soft processor core
NVIDIA CUDA architecture
NVIDIA CUDA architecture
Tilera TILE-Gx multicore architecture family
Tilera TILE-Gx multicore architecture family
Cypress M8C microprocessor
Cypress M8C microprocessor
Renesas R32C series microprocessors
Renesas R32C series microprocessors
NXP Semiconductors TriMedia architecture family
NXP Semiconductors TriMedia architecture family
QUALCOMM DSP6 processor
QUALCOMM DSP6 processor
Intel 8051 and variants
Intel 8051 and variants
STMicroelectronics STxP7x family of configurable and extensible RISC processors
STMicroelectronics STxP7x family of configurable and extensible RISC processors
Andes Technology compact code size embedded RISC processor family
Andes Technology compact code size embedded RISC processor family
Cyan Technology eCOG1X family
Cyan Technology eCOG1X family
Dallas Semiconductor MAXQ30 Core Micro-controllers
Dallas Semiconductor MAXQ30 Core Micro-controllers
New Japan Radio (NJR) 16-bit DSP Processor
New Japan Radio (NJR) 16-bit DSP Processor
M2000 Reconfigurable RISC Microprocessor
M2000 Reconfigurable RISC Microprocessor
Cray Inc. NV2 vector architecture
Cray Inc. NV2 vector architecture
Renesas RX family
Renesas RX family
Imagination Technologies META processor architecture
Imagination Technologies META processor architecture
MCST Elbrus general purpose hardware architecture
MCST Elbrus general purpose hardware architecture
Cyan Technology eCOG16 family
Cyan Technology eCOG16 family
National Semiconductor CompactRISC CR16 16-bit microprocessor
National Semiconductor CompactRISC CR16 16-bit microprocessor
Freescale Extended Time Processing Unit
Freescale Extended Time Processing Unit
Altium TSK3000 core
Altium TSK3000 core
Freescale RS08 embedded processor
Freescale RS08 embedded processor
Analog Devices SHARC family of 32-bit DSP processors
Analog Devices SHARC family of 32-bit DSP processors
Cyan Technology eCOG2 microprocessor
Cyan Technology eCOG2 microprocessor
Sunplus S+core7 RISC processor
Sunplus S+core7 RISC processor
New Japan Radio (NJR) 24-bit DSP Processor
New Japan Radio (NJR) 24-bit DSP Processor
Broadcom VideoCore III processor
Broadcom VideoCore III processor
RISC processor for Lattice FPGA architecture
RISC processor for Lattice FPGA architecture
Seiko Epson C17 family
Seiko Epson C17 family
The Texas Instruments TMS320C6000 DSP family
The Texas Instruments TMS320C6000 DSP family
The Texas Instruments TMS320C2000 DSP family
The Texas Instruments TMS320C2000 DSP family
The Texas Instruments TMS320C55x DSP family
The Texas Instruments TMS320C55x DSP family
STMicroelectronics 64bit VLIW Data Signal Processor
STMicroelectronics 64bit VLIW Data Signal Processor
LSI Logic 16-bit DSP Processor
LSI Logic 16-bit DSP Processor
Donald Knuth's educational 64-bit processor
Donald Knuth's educational 64-bit processor
Harvard University machine-independent object files
Harvard University machine-independent object files
SiTera Prism
SiTera Prism
Atmel AVR 8-bit microcontroller
Atmel AVR 8-bit microcontroller
Fujitsu FR30
Fujitsu FR30
Mitsubishi D10V
Mitsubishi D10V
Mitsubishi D30V
Mitsubishi D30V
NEC v850
NEC v850
Mitsubishi M32R
Mitsubishi M32R
Matsushita MN10300
Matsushita MN10300
Matsushita MN10200
Matsushita MN10200
picoJava
picoJava
OpenRISC 32-bit embedded processor
OpenRISC 32-bit embedded processor
ARC International ARCompact processor (old spelling/synonym: ELF_MA_ARC_A5)
ARC International ARCompact processor (old spelling/synonym: ELF_MA_ARC_A5)
Tensilica Xtensa Architecture
Tensilica Xtensa Architecture
Alphamosaic VideoCore processor
Alphamosaic VideoCore processor
Thompson Multimedia General Purpose Processor
Thompson Multimedia General Purpose Processor
National Semiconductor 32000 series
National Semiconductor 32000 series
Tenor Network TPC processor
Tenor Network TPC processor
Trebia SNP 1000 processor
Trebia SNP 1000 processor
STMicroelectronics ST200 microcontroller
STMicroelectronics ST200 microcontroller
Ubicom IP2xxx microcontroller family
Ubicom IP2xxx microcontroller family
MAX Processor
MAX Processor
National Semiconductor CompactRISC microprocessor
National Semiconductor CompactRISC microprocessor
Fujitsu F2MC16
Fujitsu F2MC16
Texas Instruments embedded microcontroller msp430
Texas Instruments embedded microcontroller msp430
Analog Devices Blackfin (DSP) processor
Analog Devices Blackfin (DSP) processor
S1C33 Family of Seiko Epson processors
S1C33 Family of Seiko Epson processors
Sharp embedded microprocessor
Sharp embedded microprocessor
Arca RISC Microprocessor
Arca RISC Microprocessor
Microprocessor series from PKU-Unity Ltd. and MPRC of Peking University
Microprocessor series from PKU-Unity Ltd. and MPRC of Peking University
eXcess: 16/32/64-bit configurable embedded CPU
eXcess: 16/32/64-bit configurable embedded CPU
Icera Semiconductor Inc. Deep Execution Processor
Icera Semiconductor Inc. Deep Execution Processor
Altera Nios II soft-core processor
Altera Nios II soft-core processor
National Semiconductor CompactRISC CRX microprocessor
National Semiconductor CompactRISC CRX microprocessor
Motorola XGATE embedded processor
Motorola XGATE embedded processor
Infineon C16x/XC16x processor
Infineon C16x/XC16x processor
Renesas M16C series microprocessors
Renesas M16C series microprocessors
Microchip Technology dsPIC30F Digital Signal Controller
Microchip Technology dsPIC30F Digital Signal Controller
Freescale Communication Engine RISC core
Freescale Communication Engine RISC core
Renesas M32C series microprocessors
Renesas M32C series microprocessors
No machine
No machine
AT&T WE 32100
AT&T WE 32100
SPARC
SPARC
Intel 80386
Intel 80386
Motorola 68000
Motorola 68000
Motorola 88000
Motorola 88000
Intel 80860
Intel 80860
MIPS I Architecture
MIPS I Architecture
IBM System/370 Processor
IBM System/370 Processor
MIPS RS3000 Little-endian
MIPS RS3000 Little-endian
Hewlett-Packard PA-RISC
Hewlett-Packard PA-RISC
Fujitsu VPP500
Fujitsu VPP500
Enhanced instruction set SPARC
Enhanced instruction set SPARC
Intel 80960
Intel 80960
PowerPC
PowerPC
64-bit PowerPC
64-bit PowerPC
IBM System/390 Processor
IBM System/390 Processor
IBM SPU/SPC
IBM SPU/SPC
NEC V800
NEC V800
Fujitsu FR20
Fujitsu FR20
TRW RH-32
TRW RH-32
Motorola RCE
Motorola RCE
ARM 32-bit architecture (AARCH32)
ARM 32-bit architecture (AARCH32)
Digital Alpha
Digital Alpha
Hitachi SH
Hitachi SH
SPARC Version 9
SPARC Version 9
Siemens TriCore embedded processor
Siemens TriCore embedded processor
Argonaut RISC Core, Argonaut Technologies Inc.
Argonaut RISC Core, Argonaut Technologies Inc.
Hitachi H8/300
Hitachi H8/300
Hitachi H8/300H
Hitachi H8/300H
Hitachi H8S
Hitachi H8S
Hitachi H8/500
Hitachi H8/500
Intel IA-64 processor architecture
Intel IA-64 processor architecture
Stanford MIPS-X
Stanford MIPS-X
Motorola ColdFire
Motorola ColdFire
Motorola M68HC12
Motorola M68HC12
Fujitsu MMA Multimedia Accelerator
Fujitsu MMA Multimedia Accelerator
Siemens PCP
Siemens PCP
Sony nCPU embedded RISC processor
Sony nCPU embedded RISC processor
Denso NDR1 microprocessor
Denso NDR1 microprocessor
Motorola Star*Core processor
Motorola Star*Core processor
Toyota ME16 processor
Toyota ME16 processor
STMicroelectronics ST100 processor
STMicroelectronics ST100 processor
Advanced Logic Corp. TinyJ embedded processor family
Advanced Logic Corp. TinyJ embedded processor family
AMD x86-64 architecture
AMD x86-64 architecture
Sony DSP Processor
Sony DSP Processor
Digital Equipment Corp. PDP-10
Digital Equipment Corp. PDP-10
Digital Equipment Corp. PDP-11
Digital Equipment Corp. PDP-11
Siemens FX66 microcontroller
Siemens FX66 microcontroller
STMicroelectronics ST9+ 8/16 bit microcontroller
STMicroelectronics ST9+ 8/16 bit microcontroller
STMicroelectronics ST7 8-bit microcontroller
STMicroelectronics ST7 8-bit microcontroller
Motorola MC68HC16 Microcontroller
Motorola MC68HC16 Microcontroller
Motorola MC68HC11 Microcontroller
Motorola MC68HC11 Microcontroller
Motorola MC68HC08 Microcontroller
Motorola MC68HC08 Microcontroller
Motorola MC68HC05 Microcontroller
Motorola MC68HC05 Microcontroller
Silicon Graphics SVx
Silicon Graphics SVx
STMicroelectronics ST19 8-bit microcontroller
STMicroelectronics ST19 8-bit microcontroller
Digital VAX
Digital VAX
Axis Communications 32-bit embedded processor
Axis Communications 32-bit embedded processor
Infineon Technologies 32-bit embedded processor
Infineon Technologies 32-bit embedded processor
Element 14 64-bit DSP Processor
Element 14 64-bit DSP Processor
Reserved by Intel
Reserved by Intel
Reserved by Intel
Reserved by Intel
Reserved by Intel
Reserved by Intel
Reserved by Intel
Reserved by Intel
Reserved by Intel
Reserved by Intel
Reserved by Intel
Reserved by Intel
Reserved by ARM
Reserved by ARM
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
Reserved for future use
string_of_elf_machine_architecture m produces a string representation of * the numeric encoding m of the ELF machine architecture. * TODO: finish this .
ELF version numbers. Denotes the ELF version number of an ELF file. Current is * defined to have a value of 1 with the present specification. Extensions * may create versions of ELF with higher version numbers.
Invalid version
Current version
Current version
string_of_elf_version_number m produces a string representation of the * numeric encoding m of the ELF version number.
Check that an extended version number is correct (i.e. greater than 1).
Identification indices. The initial bytes of an ELF header (and an object * file) correspond to the e_ident member.
File identification
File identification
File identification
File identification
File identification
File identification
File identification
File class
File class
Data encoding
Data encoding
File version
File version
Operating system/ABI identification
Operating system/ABI identification
ABI version
ABI version
Start of padding bytes
Start of padding bytes
Size of e*_ident
Size of e*_ident
Magic number indices. A file's first 4 bytes hold a ``magic number,'' * identifying the file as an ELF object file.
Position: e*_identelf_ii_mag0, 0x7f magic number
Position: e*_identelf_ii_mag1, 'E' format identifier
Position: e*_identelf_ii_mag1, 'E' format identifier
Position: e*_identelf_ii_mag2, 'L' format identifier
Position: e*_identelf_ii_mag2, 'L' format identifier
Position: e*_identelf_ii_mag3, 'F' format identifier
Position: e*_identelf_ii_mag3, 'F' format identifier
ELf file classes. The file format is designed to be portable among machines * of various sizes, without imposing the sizes of the largest machine on the * smallest. The class of the file defines the basic types used by the data * structures of the object file container itself.
Invalid class
32 bit objects
32 bit objects
64 bit objects
64 bit objects
string_of_elf_file_class m produces a string representation of the numeric * encoding m of the ELF file class.
ELF data encodings. Byte e_identelf_ei_data specifies the encoding of both the * data structures used by object file container and data contained in object * file sections.
Invalid data encoding
Two's complement values, least significant byte occupying lowest address
Two's complement values, least significant byte occupying lowest address
Two's complement values, most significant byte occupying lowest address
Two's complement values, most significant byte occupying lowest address
string_of_elf_data_encoding m produces a string representation of the * numeric encoding m of the ELF data encoding.
OS and ABI versions. Byte e_identelf_ei_osabi identifies the OS- or * ABI-specific ELF extensions used by this file. Some fields in other ELF * structures have flags and values that have operating system and/or ABI * specific meanings; the interpretation of those fields is determined by the * value of this byte.
No extensions or unspecified
Hewlett-Packard HP-UX
Hewlett-Packard HP-UX
NetBSD
NetBSD
GNU
GNU
Linux, historical alias for GNU
Linux, historical alias for GNU
Sun Solaris
Sun Solaris
AIX
AIX
IRIX
IRIX
FreeBSD
FreeBSD
Compaq Tru64 Unix
Compaq Tru64 Unix
Novell Modesto
Novell Modesto
OpenBSD
OpenBSD
OpenVMS
OpenVMS
Hewlett-Packard Non-stop Kernel
Hewlett-Packard Non-stop Kernel
Amiga Research OS
Amiga Research OS
FenixOS highly-scalable multi-core OS
FenixOS highly-scalable multi-core OS
Nuxi CloudABI
Nuxi CloudABI
Stratus technologies OpenVOS
Stratus technologies OpenVOS
Checks an architecture defined OSABI version is correct, i.e. in the range * 64 to 255 inclusive.
string_of_elf_osabi_version m produces a string representation of the * numeric encoding m of the ELF OSABI version.
ELF Header type
ei_nident is the fixed length of the identification field in the * elf32_ehdr type.
type elf32_header = {elf32_ident : Uint32_wrapper.uint32 list;(*Identification field
*)elf32_type : Uint32_wrapper.uint32;(*The object file type
*)elf32_machine : Uint32_wrapper.uint32;(*Required machine architecture
*)elf32_version : Uint32_wrapper.uint32;(*Object file version
*)elf32_entry : Uint32_wrapper.uint32;(*Virtual address for transfer of control
*)elf32_phoff : Uint32_wrapper.uint32;(*Program header table offset in bytes
*)elf32_shoff : Uint32_wrapper.uint32;(*Section header table offset in bytes
*)elf32_flags : Uint32_wrapper.uint32;(*Processor-specific flags
*)elf32_ehsize : Uint32_wrapper.uint32;(*ELF header size in bytes
*)elf32_phentsize : Uint32_wrapper.uint32;(*Program header table entry size in bytes
*)elf32_phnum : Uint32_wrapper.uint32;(*Number of entries in program header table
*)elf32_shentsize : Uint32_wrapper.uint32;(*Section header table entry size in bytes
*)elf32_shnum : Uint32_wrapper.uint32;(*Number of entries in section header table
*)elf32_shstrndx : Uint32_wrapper.uint32;(*Section header table entry for section name string table
*)
}elf32_header is the type of headers for 32-bit ELF files.
type elf64_header = {elf64_ident : Uint32_wrapper.uint32 list;(*Identification field
*)elf64_type : Uint32_wrapper.uint32;(*The object file type
*)elf64_machine : Uint32_wrapper.uint32;(*Required machine architecture
*)elf64_version : Uint32_wrapper.uint32;(*Object file version
*)elf64_entry : Uint64_wrapper.uint64;(*Virtual address for transfer of control
*)elf64_phoff : Uint64_wrapper.uint64;(*Program header table offset in bytes
*)elf64_shoff : Uint64_wrapper.uint64;(*Section header table offset in bytes
*)elf64_flags : Uint32_wrapper.uint32;(*Processor-specific flags
*)elf64_ehsize : Uint32_wrapper.uint32;(*ELF header size in bytes
*)elf64_phentsize : Uint32_wrapper.uint32;(*Program header table entry size in bytes
*)elf64_phnum : Uint32_wrapper.uint32;(*Number of entries in program header table
*)elf64_shentsize : Uint32_wrapper.uint32;(*Section header table entry size in bytes
*)elf64_shnum : Uint32_wrapper.uint32;(*Number of entries in section header table
*)elf64_shstrndx : Uint32_wrapper.uint32;(*Section header table entry for section name string table
*)
}elf64_header is the type of headers for 64-bit ELF files.
is_valid_elf32_header hdr checks whether header hdr is valid, i.e. has * the correct magic numbers. * TODO: this should be expanded, presumably, or merged with some of the other * checks.
is_valid_elf64_header hdr checks whether header hdr is valid, i.e. has * the correct magic numbers. * TODO: this should be expanded, presumably, or merged with some of the other * checks.
elf32_header_compare hdr1 hdr2 is an ordering comparison function for * ELF headers suitable for use in sets, finite maps and other ordered * data types.
val instance_Basic_classes_Ord_Elf_header_elf32_header_dict :
elf32_header Lem_basic_classes.ord_clasself64_header_compare hdr1 hdr2 is an ordering comparison function for * ELF headers suitable for use in sets, finite maps and other ordered * data types.
val instance_Basic_classes_Ord_Elf_header_elf64_header_dict :
elf64_header Lem_basic_classes.ord_classis_elf32_executable_file hdr checks whether the header hdr states if the * ELF file is of executable type.
is_elf64_executable_file hdr checks whether the header hdr states if the * ELF file is of executable type.
is_elf32_shared_object_file hdr checks whether the header hdr states if the * ELF file is of shared object type.
is_elf64_shared_object_file hdr checks whether the header hdr states if the * ELF file is of shared object type.
is_elf32_relocatable_file hdr checks whether the header hdr states if the * ELF file is of relocatable type.
is_elf64_relocatable_file hdr checks whether the header hdr states if the * ELF file is of relocatable type.
is_elf32_linkable_file hdr checks whether the header hdr states if the * ELF file is of linkable (shared object or relocatable) type.
is_elf64_linkable_file hdr checks whether the header hdr states if the * ELF file is of linkable (shared object or relocatable) type.
get_elf32_machine_architecture hdr returns the ELF file's declared machine * architecture, extracting the information from header hdr.
get_elf64_machine_architecture hdr returns the ELF file's declared machine * architecture, extracting the information from header hdr.
get_elf32_osabi hdr returns the ELF file's declared OS/ABI * architecture, extracting the information from header hdr.
get_elf64_osabi hdr returns the ELF file's declared OS/ABI * architecture, extracting the information from header hdr.
get_elf32_data_encoding hdr returns the ELF file's declared data * encoding, extracting the information from header hdr.
get_elf64_data_encoding hdr returns the ELF file's declared data * encoding, extracting the information from header hdr.
get_elf32_file_class hdr returns the ELF file's declared file * class, extracting the information from header hdr.
get_elf64_file_class hdr returns the ELF file's declared file * class, extracting the information from header hdr.
get_elf32_version_number hdr returns the ELF file's declared version * number, extracting the information from header hdr.
get_elf64_version_number hdr returns the ELF file's declared version * number, extracting the information from header hdr.
is_valid_elf32_version_number hdr checks whether an ELF file's declared * version number matches the current, mandatory version number. * TODO: this should be merged into is_valid_elf32_header to create a single * correctness check.
is_valid_elf64_version_number hdr checks whether an ELF file's declared * version number matches the current, mandatory version number. * TODO: this should be merged into is_valid_elf64_header to create a single * correctness check.
get_elf32_abi_version hdr returns the ELF file's declared ABI version * number, extracting the information from header hdr.
get_elf64_abi_version hdr returns the ELF file's declared ABI version * number, extracting the information from header hdr.
deduce_endianness uc deduces the endianness of an ELF file based on the ELF * header's magic number uc.
get_elf32_header_endianness hdr returns the endianness of the ELF file * as declared in its header, hdr.
get_elf64_header_endianness hdr returns the endianness of the ELF file * as declared in its header, hdr.
has_elf32_header_associated_entry_point hdr checks whether the header * hdr declares an entry point for the program.
has_elf64_header_associated_entry_point hdr checks whether the header * hdr declares an entry point for the program.
has_elf32_header_string_table hdr checks whether the header * hdr declares whether the program has a string table or not.
has_elf64_header_string_table hdr checks whether the header * hdr declares whether the program has a string table or not.
is_elf32_header_section_size_in_section_header_table hdr checks whether the header * hdr declares whether the section size is too large to fit in the header * field and is instead stored in the section header table.
is_elf64_header_section_size_in_section_header_table hdr checks whether the header * hdr declares whether the section size is too large to fit in the header * field and is instead stored in the section header table.
is_elf32_header_string_table_index_in_link hdr checks whether the header * hdr declares whether the string table index is too large to fit in the * header's field and is instead stored in the link field of an entry in the * section header table.
is_elf64_header_string_table_index_in_link hdr checks whether the header * hdr declares whether the string table index is too large to fit in the * header's field and is instead stored in the link field of an entry in the * section header table.
The hdr_print_bundle type is used to tidy up other type signatures. Some of the * top-level string_of_ functions require six or more functions passed to them, * which quickly gets out of hand. This type is used to reduce that complexity. * The first component of the type is an OS specific print function, the second is * a processor specific print function.
val string_of_elf32_header :
((Nat_big_num.num -> string) * (Nat_big_num.num -> string)) ->
elf32_header ->
stringstring_of_elf32_header hdr_bdl hdr returns a string-based representation * of header hdr using the ABI-specific print bundle hdr_bdl.
val string_of_elf64_header :
((Nat_big_num.num -> string) * (Nat_big_num.num -> string)) ->
elf64_header ->
stringstring_of_elf64_header hdr_bdl hdr returns a string-based representation * of header hdr using the ABI-specific print bundle hdr_bdl.
The following are thin wrappers around the pretty-printing functions above * using a default print bundle for the header.
val read_elf_ident :
Byte_sequence_wrapper.byte_sequence ->
(Uint32_wrapper.uint32 list * Byte_sequence_wrapper.byte_sequence)
Error.errorread_elf_ident bs0 reads the initial bytes of an ELF file from byte sequence * bs0, returning the remainder of the byte sequence too. * Fails if transcription fails.
bytes_of_elf32_header hdr blits an ELF header hdr to a byte sequence, * ready for transcription to a binary file.
bytes_of_elf64_header hdr blits an ELF header hdr to a byte sequence, * ready for transcription to a binary file.
val read_elf32_header :
Byte_sequence_wrapper.byte_sequence ->
(elf32_header * Byte_sequence_wrapper.byte_sequence) Error.errorread_elf32_header bs0 reads an ELF header from the byte sequence bs0. * Fails if transcription fails.
val read_elf64_header :
Byte_sequence_wrapper.byte_sequence ->
(elf64_header * Byte_sequence_wrapper.byte_sequence) Error.errorread_elf64_header bs0 reads an ELF header from the byte sequence bs0. * Fails if transcription fails.
is_elf32_header_class_correct hdr checks whether the declared file class * is correct.
is_elf64_header_class_correct hdr checks whether the declared file class * is correct.
is_elf32_header_version_correct hdr checks whether the declared file version * is correct.
is_elf64_header_version_correct hdr checks whether the declared file version * is correct.
is_elf32_header_valid checks whether an elf32_header value is a valid 32-bit * ELF file header (i.e. elf32_ident is ei_nident entries long, and other * constraints on headers).
get_elf32_header_program_table_size calculates the size of the program table * (entry size x number of entries) based on data in the ELF header.
get_elf64_header_program_table_size calculates the size of the program table * (entry size x number of entries) based on data in the ELF header.
is_elf32_header_section_table_present calculates whether a section table * is present in the ELF file or not.
is_elf64_header_section_table_present calculates whether a section table * is present in the ELF file or not.
get_elf32_header_section_table_size calculates the size of the section table * (entry size x number of entries) based on data in the ELF header.
get_elf64_header_section_table_size calculates the size of the section table * (entry size x number of entries) based on data in the ELF header.