Module Elf_header Source elf_header includes types, functions and other definitions for working with * ELF headers.
Special section header table indices
Source val shn_undef : Nat_big_num .numshn_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).
Source val shn_xindex : Nat_big_num .numshn_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.
Source val elf_ft_none : Nat_big_num .numNo file type
Relocatable file
Source val elf_ft_rel : Nat_big_num .numRelocatable file
Executable file
Source val elf_ft_exec : Nat_big_num .numExecutable file
Shared object file
Source val elf_ft_dyn : Nat_big_num .numShared object file
Core file
Source val elf_ft_core : Nat_big_num .numCore file
Operating-system specific
Source val elf_ft_lo_os : Nat_big_num .numOperating-system specific
Operating-system specific
Source val elf_ft_hi_os : Nat_big_num .numOperating-system specific
Processor specific
Source val elf_ft_lo_proc : Nat_big_num .numProcessor specific
Processor specific
Source val elf_ft_hi_proc : Nat_big_num .numSource val string_of_elf_file_type :
(Nat_big_num .num -> -> (Nat_big_num .num -> -> Nat_big_num .num -> string_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.
Source val is_operating_system_specific_object_file_type_value :
Nat_big_num .num -> is_operating_specific_file_type_value checks whether a numeric value is * reserved by the ABI for operating system-specific purposes.
Source val is_processor_specific_object_file_type_value : Nat_big_num .num -> is_processor_specific_file_type_value checks whether a numeric value is * reserved by the ABI for processor-specific purposes.
ELF machine architectures
Source val elf_ma_riscv : Nat_big_num .numRISC-V
AMD GPU architecture
Source val elf_ma_amdgpu : Nat_big_num .numAMD GPU architecture
Moxie processor family
Source val elf_ma_moxie : Nat_big_num .numMoxie processor family
FTDI Chip FT32 high performance 32-bit RISC architecture
Source val elf_ma_ft32 : Nat_big_num .numFTDI Chip FT32 high performance 32-bit RISC architecture
Controls and Data Services VISIUMcore processor
Source val elf_ma_visium : Nat_big_num .numControls and Data Services VISIUMcore processor
Zilog Z80
Source val elf_ma_z80 : Nat_big_num .numZilog Z80
CSR Kalimba architecture family
Source val elf_ma_kalimba : Nat_big_num .numCSR Kalimba architecture family
Nanoradio optimised RISC
Source val elf_ma_norc : Nat_big_num .numNanoradio optimised RISC
iCelero CoolEngine
Source val elf_ma_cool : Nat_big_num .numiCelero CoolEngine
Cognitive Smart Memory Processor
Source val elf_ma_coge : Nat_big_num .numCognitive Smart Memory Processor
Paneve CDP architecture family
Source val elf_ma_cdp : Nat_big_num .numPaneve CDP architecture family
KM211 KVARC processor
Source val elf_ma_kvarc : Nat_big_num .numKM211 KVARC processor
KM211 KMX8 8-bit processor
Source val elf_ma_kmx8 : Nat_big_num .numKM211 KMX8 8-bit processor
KM211 KMX16 16-bit processor
Source val elf_ma_kmx16 : Nat_big_num .numKM211 KMX16 16-bit processor
KM211 KMX32 32-bit processor
Source val elf_ma_kmx32 : Nat_big_num .numKM211 KMX32 32-bit processor
KM211 KM32 32-bit processor
Source val elf_ma_km32 : Nat_big_num .numKM211 KM32 32-bit processor
Microchip 8-bit PIC(r) family
Source val elf_ma_mchp_pic : Nat_big_num .numMicrochip 8-bit PIC(r) family
XMOS xCORE processor family
Source val elf_ma_xcore : Nat_big_num .numXMOS xCORE processor family
Beyond BA2 CPU architecture
Source val elf_ma_ba2 : Nat_big_num .numBeyond BA2 CPU architecture
Beyond BA1 CPU architecture
Source val elf_ma_ba1 : Nat_big_num .numBeyond BA1 CPU architecture
Freescale 56800EX Digital Signal Controller (DSC)
Source val elf_ma_5600ex : Nat_big_num .numFreescale 56800EX Digital Signal Controller (DSC)
199 Renesas 78KOR family
Source val elf_ma_78kor : Nat_big_num .num199 Renesas 78KOR family
Broadcom VideoCore V processor
Source val elf_ma_videocore5 : Nat_big_num .numBroadcom VideoCore V processor
Renesas RL78 family
Source val elf_ma_rl78 : Nat_big_num .numRenesas RL78 family
Open8 8-bit RISC soft processing core
Source val elf_ma_open8 : Nat_big_num .numOpen8 8-bit RISC soft processing core
Synopsys ARCompact V2
Source val elf_ma_arc_compact2 : Nat_big_num .numSynopsys ARCompact V2
KIPO_KAIST Core-A 2nd generation processor family
Source val elf_ma_corea_2nd : Nat_big_num .numKIPO_KAIST Core-A 2nd generation processor family
KIPO_KAIST Core-A 1st generation processor family
Source val elf_ma_corea_1st : Nat_big_num .numKIPO_KAIST Core-A 1st generation processor family
CloudShield architecture family
Source val elf_ma_cloudshield : Nat_big_num .numCloudShield architecture family
Infineon Technologies SLE9X core
Source val elf_ma_sle9x : Nat_big_num .numInfineon Technologies SLE9X core
Intel L10M
Source val elf_ma_l10m : Nat_big_num .numSource val elf_ma_k10m : Nat_big_num .numIntel K10M
ARM 64-bit architecture (AARCH64)
Source val elf_ma_aarch64 : Nat_big_num .numARM 64-bit architecture (AARCH64)
Atmel Corporation 32-bit microprocessor family
Source val elf_ma_avr32 : Nat_big_num .numAtmel Corporation 32-bit microprocessor family
STMicroelectronics STM8 8-bit microcontroller
Source val elf_ma_stm8 : Nat_big_num .numSTMicroelectronics STM8 8-bit microcontroller
Tilera TILE64 multicore architecture family
Source val elf_ma_tile64 : Nat_big_num .numTilera TILE64 multicore architecture family
Tilera TILEPro multicore architecture family
Source val elf_ma_tilepro : Nat_big_num .numTilera TILEPro multicore architecture family
Xilinix MicroBlaze 32-bit RISC soft processor core
Source val elf_ma_microblaze : Nat_big_num .numXilinix MicroBlaze 32-bit RISC soft processor core
NVIDIA CUDA architecture
Source val elf_ma_cuda : Nat_big_num .numNVIDIA CUDA architecture
Tilera TILE-Gx multicore architecture family
Source val elf_ma_tilegx : Nat_big_num .numTilera TILE-Gx multicore architecture family
Cypress M8C microprocessor
Source val elf_ma_cypress : Nat_big_num .numCypress M8C microprocessor
Renesas R32C series microprocessors
Source val elf_ma_r32c : Nat_big_num .numRenesas R32C series microprocessors
NXP Semiconductors TriMedia architecture family
NXP Semiconductors TriMedia architecture family
QUALCOMM DSP6 processor
Source val elf_ma_qdsp6 : Nat_big_num .numQUALCOMM DSP6 processor
Intel 8051 and variants
Source val elf_ma_8051 : Nat_big_num .numIntel 8051 and variants
STMicroelectronics STxP7x family of configurable and extensible RISC processors
Source val elf_ma_stxp7x : Nat_big_num .numSTMicroelectronics STxP7x family of configurable and extensible RISC processors
Andes Technology compact code size embedded RISC processor family
Source val elf_ma_nds32 : Nat_big_num .numAndes Technology compact code size embedded RISC processor family
Cyan Technology eCOG1X family
Source val elf_ma_ecog1x : Nat_big_num .numCyan Technology eCOG1X family
Dallas Semiconductor MAXQ30 Core Micro-controllers
Source val elf_ma_maxq30 : Nat_big_num .numDallas Semiconductor MAXQ30 Core Micro-controllers
New Japan Radio (NJR) 16-bit DSP Processor
Source val elf_ma_ximo16 : Nat_big_num .numNew Japan Radio (NJR) 16-bit DSP Processor
M2000 Reconfigurable RISC Microprocessor
Source val elf_ma_manik : Nat_big_num .numM2000 Reconfigurable RISC Microprocessor
Cray Inc. NV2 vector architecture
Source val elf_ma_craynv2 : Nat_big_num .numCray Inc. NV2 vector architecture
Renesas RX family
Source val elf_ma_rx : Nat_big_num .numRenesas RX family
Imagination Technologies META processor architecture
Imagination Technologies META processor architecture
MCST Elbrus general purpose hardware architecture
Source val elf_ma_mcst_elbrus : Nat_big_num .numMCST Elbrus general purpose hardware architecture
Cyan Technology eCOG16 family
Source val elf_ma_ecog16 : Nat_big_num .numCyan Technology eCOG16 family
National Semiconductor CompactRISC CR16 16-bit microprocessor
Source val elf_ma_cr16 : Nat_big_num .numNational Semiconductor CompactRISC CR16 16-bit microprocessor
Freescale Extended Time Processing Unit
Source val elf_ma_etpu : Nat_big_num .numFreescale Extended Time Processing Unit
Altium TSK3000 core
Source val elf_ma_tsk3000 : Nat_big_num .numAltium TSK3000 core
Freescale RS08 embedded processor
Source val elf_ma_rs08 : Nat_big_num .numFreescale RS08 embedded processor
Analog Devices SHARC family of 32-bit DSP processors
Source val elf_ma_sharc : Nat_big_num .numAnalog Devices SHARC family of 32-bit DSP processors
Cyan Technology eCOG2 microprocessor
Source val elf_ma_ecog2 : Nat_big_num .numCyan Technology eCOG2 microprocessor
Sunplus S+core7 RISC processor
Source val elf_ma_ccore7 : Nat_big_num .numSunplus S+core7 RISC processor
New Japan Radio (NJR) 24-bit DSP Processor
Source val elf_ma_dsp24 : Nat_big_num .numNew Japan Radio (NJR) 24-bit DSP Processor
Broadcom VideoCore III processor
Source val elf_ma_videocore3 : Nat_big_num .numBroadcom VideoCore III processor
RISC processor for Lattice FPGA architecture
Source val elf_ma_latticemico32 : Nat_big_num .numRISC processor for Lattice FPGA architecture
Seiko Epson C17 family
Source val elf_ma_c17 : Nat_big_num .numSeiko Epson C17 family
The Texas Instruments TMS320C6000 DSP family
Source val elf_ma_c6000 : Nat_big_num .numThe Texas Instruments TMS320C6000 DSP family
The Texas Instruments TMS320C2000 DSP family
Source val elf_ma_c2000 : Nat_big_num .numThe Texas Instruments TMS320C2000 DSP family
The Texas Instruments TMS320C55x DSP family
Source val elf_ma_c5500 : Nat_big_num .numThe Texas Instruments TMS320C55x DSP family
STMicroelectronics 64bit VLIW Data Signal Processor
Source val elf_ma_mmdsp_plus : Nat_big_num .numSTMicroelectronics 64bit VLIW Data Signal Processor
LSI Logic 16-bit DSP Processor
Source val elf_ma_zsp : Nat_big_num .numLSI Logic 16-bit DSP Processor
Donald Knuth's educational 64-bit processor
Source val elf_ma_mmix : Nat_big_num .numDonald Knuth's educational 64-bit processor
Harvard University machine-independent object files
Source val elf_ma_huany : Nat_big_num .numHarvard University machine-independent object files
SiTera Prism
Source val elf_ma_prism : Nat_big_num .numSiTera Prism
Atmel AVR 8-bit microcontroller
Source val elf_ma_avr : Nat_big_num .numAtmel AVR 8-bit microcontroller
Fujitsu FR30
Source val elf_ma_fr30 : Nat_big_num .numFujitsu FR30
Mitsubishi D10V
Source val elf_ma_d10v : Nat_big_num .numMitsubishi D10V
Mitsubishi D30V
Source val elf_ma_d30v : Nat_big_num .numSource val elf_ma_v850 : Nat_big_num .numSource val elf_ma_m32r : Nat_big_num .numMitsubishi M32R
Matsushita MN10300
Source val elf_ma_mn10300 : Nat_big_num .numMatsushita MN10300
Matsushita MN10200
Source val elf_ma_mn10200 : Nat_big_num .numMatsushita MN10200
picoJava
Source val elf_ma_pj : Nat_big_num .numpicoJava
OpenRISC 32-bit embedded processor
Source val elf_ma_openrisc : Nat_big_num .numOpenRISC 32-bit embedded processor
ARC International ARCompact processor (old spelling/synonym: ELF_MA_ARC_A5)
Source val elf_ma_arc_compact : Nat_big_num .numARC International ARCompact processor (old spelling/synonym: ELF_MA_ARC_A5)
Tensilica Xtensa Architecture
Source val elf_ma_xtensa : Nat_big_num .numTensilica Xtensa Architecture
Alphamosaic VideoCore processor
Source val elf_ma_videocore : Nat_big_num .numAlphamosaic VideoCore processor
Thompson Multimedia General Purpose Processor
Source val elf_ma_tmm_gpp : Nat_big_num .numThompson Multimedia General Purpose Processor
National Semiconductor 32000 series
Source val elf_ma_ns32k : Nat_big_num .numNational Semiconductor 32000 series
Tenor Network TPC processor
Source val elf_ma_tpc : Nat_big_num .numTenor Network TPC processor
Trebia SNP 1000 processor
Source val elf_ma_snp1k : Nat_big_num .numTrebia SNP 1000 processor
STMicroelectronics ST200 microcontroller
Source val elf_ma_st200 : Nat_big_num .numSTMicroelectronics ST200 microcontroller
Ubicom IP2xxx microcontroller family
Source val elf_ma_ip2k : Nat_big_num .numUbicom IP2xxx microcontroller family
MAX Processor
Source val elf_ma_max : Nat_big_num .numMAX Processor
National Semiconductor CompactRISC microprocessor
Source val elf_ma_cr : Nat_big_num .numNational Semiconductor CompactRISC microprocessor
Fujitsu F2MC16
Source val elf_ma_f2mc16 : Nat_big_num .numFujitsu F2MC16
Texas Instruments embedded microcontroller msp430
Source val elf_ma_msp430 : Nat_big_num .numTexas Instruments embedded microcontroller msp430
Analog Devices Blackfin (DSP) processor
Source val elf_ma_blackfin : Nat_big_num .numAnalog Devices Blackfin (DSP) processor
S1C33 Family of Seiko Epson processors
Source val elf_ma_se_c33 : Nat_big_num .numS1C33 Family of Seiko Epson processors
Sharp embedded microprocessor
Source val elf_ma_sep : Nat_big_num .numSharp embedded microprocessor
Arca RISC Microprocessor
Source val elf_ma_arca : Nat_big_num .numArca RISC Microprocessor
Microprocessor series from PKU-Unity Ltd. and MPRC of Peking University
Source val elf_ma_unicore : Nat_big_num .numMicroprocessor series from PKU-Unity Ltd. and MPRC of Peking University
eXcess: 16/32/64-bit configurable embedded CPU
Source val elf_ma_excess : Nat_big_num .numeXcess: 16/32/64-bit configurable embedded CPU
Icera Semiconductor Inc. Deep Execution Processor
Source val elf_ma_dxp : Nat_big_num .numIcera Semiconductor Inc. Deep Execution Processor
Altera Nios II soft-core processor
Source val elf_ma_altera_nios2 : Nat_big_num .numAltera Nios II soft-core processor
National Semiconductor CompactRISC CRX microprocessor
Source val elf_ma_crx : Nat_big_num .numNational Semiconductor CompactRISC CRX microprocessor
Motorola XGATE embedded processor
Source val elf_ma_xgate : Nat_big_num .numMotorola XGATE embedded processor
Infineon C16x/XC16x processor
Source val elf_ma_c166 : Nat_big_num .numInfineon C16x/XC16x processor
Renesas M16C series microprocessors
Source val elf_ma_m16c : Nat_big_num .numRenesas M16C series microprocessors
Microchip Technology dsPIC30F Digital Signal Controller
Source val elf_ma_dspic30f : Nat_big_num .numMicrochip Technology dsPIC30F Digital Signal Controller
Freescale Communication Engine RISC core
Source val elf_ma_ce : Nat_big_num .numFreescale Communication Engine RISC core
Renesas M32C series microprocessors
Source val elf_ma_m32c : Nat_big_num .numRenesas M32C series microprocessors
No machine
Source val elf_ma_none : Nat_big_num .numSource val elf_ma_m32 : Nat_big_num .numSource val elf_ma_sparc : Nat_big_num .numSource val elf_ma_386 : Nat_big_num .numIntel 80386
Motorola 68000
Source val elf_ma_68k : Nat_big_num .numMotorola 68000
Motorola 88000
Source val elf_ma_88k : Nat_big_num .numMotorola 88000
Intel 80860
Source val elf_ma_860 : Nat_big_num .numIntel 80860
MIPS I Architecture
Source val elf_ma_mips : Nat_big_num .numMIPS I Architecture
IBM System/370 Processor
Source val elf_ma_s370 : Nat_big_num .numIBM System/370 Processor
MIPS RS3000 Little-endian
Source val elf_ma_mips_rs3_le : Nat_big_num .numMIPS RS3000 Little-endian
Hewlett-Packard PA-RISC
Source val elf_ma_parisc : Nat_big_num .numHewlett-Packard PA-RISC
Fujitsu VPP500
Source val elf_ma_vpp500 : Nat_big_num .numFujitsu VPP500
Enhanced instruction set SPARC
Source val elf_ma_sparc32plus : Nat_big_num .numEnhanced instruction set SPARC
Intel 80960
Source val elf_ma_960 : Nat_big_num .numSource val elf_ma_ppc : Nat_big_num .numSource val elf_ma_ppc64 : Nat_big_num .num64-bit PowerPC
IBM System/390 Processor
Source val elf_ma_s390 : Nat_big_num .numIBM System/390 Processor
IBM SPU/SPC
Source val elf_ma_spu : Nat_big_num .numSource val elf_ma_v800 : Nat_big_num .numSource val elf_ma_fr20 : Nat_big_num .numSource val elf_ma_rh32 : Nat_big_num .numSource val elf_ma_rce : Nat_big_num .numMotorola RCE
ARM 32-bit architecture (AARCH32)
Source val elf_ma_arm : Nat_big_num .numARM 32-bit architecture (AARCH32)
Digital Alpha
Source val elf_ma_alpha : Nat_big_num .numSource val elf_ma_sh : Nat_big_num .numHitachi SH
SPARC Version 9
Source val elf_ma_sparcv9 : Nat_big_num .numSPARC Version 9
Siemens TriCore embedded processor
Source val elf_ma_tricore : Nat_big_num .numSiemens TriCore embedded processor
Argonaut RISC Core, Argonaut Technologies Inc.
Source val elf_ma_arc : Nat_big_num .numArgonaut RISC Core, Argonaut Technologies Inc.
Hitachi H8/300
Source val elf_ma_h8_300 : Nat_big_num .numHitachi H8/300
Hitachi H8/300H
Source val elf_ma_h8_300h : Nat_big_num .numHitachi H8/300H
Hitachi H8S
Source val elf_ma_h8s : Nat_big_num .numHitachi H8S
Hitachi H8/500
Source val elf_ma_h8_500 : Nat_big_num .numHitachi H8/500
Intel IA-64 processor architecture
Source val elf_ma_ia_64 : Nat_big_num .numIntel IA-64 processor architecture
Stanford MIPS-X
Source val elf_ma_mips_x : Nat_big_num .numStanford MIPS-X
Motorola ColdFire
Source val elf_ma_coldfire : Nat_big_num .numMotorola ColdFire
Motorola M68HC12
Source val elf_ma_68hc12 : Nat_big_num .numMotorola M68HC12
Fujitsu MMA Multimedia Accelerator
Source val elf_ma_mma : Nat_big_num .numFujitsu MMA Multimedia Accelerator
Siemens PCP
Source val elf_ma_pcp : Nat_big_num .numSiemens PCP
Sony nCPU embedded RISC processor
Source val elf_ma_ncpu : Nat_big_num .numSony nCPU embedded RISC processor
Denso NDR1 microprocessor
Source val elf_ma_ndr1 : Nat_big_num .numDenso NDR1 microprocessor
Motorola Star*Core processor
Source val elf_ma_starcore : Nat_big_num .numMotorola Star*Core processor
Toyota ME16 processor
Source val elf_ma_me16 : Nat_big_num .numToyota ME16 processor
STMicroelectronics ST100 processor
Source val elf_ma_st100 : Nat_big_num .numSTMicroelectronics ST100 processor
Advanced Logic Corp. TinyJ embedded processor family
Source val elf_ma_tinyj : Nat_big_num .numAdvanced Logic Corp. TinyJ embedded processor family
AMD x86-64 architecture
Source val elf_ma_x86_64 : Nat_big_num .numAMD x86-64 architecture
Sony DSP Processor
Source val elf_ma_pdsp : Nat_big_num .numSony DSP Processor
Digital Equipment Corp. PDP-10
Source val elf_ma_pdp10 : Nat_big_num .numDigital Equipment Corp. PDP-10
Digital Equipment Corp. PDP-11
Source val elf_ma_pdp11 : Nat_big_num .numDigital Equipment Corp. PDP-11
Siemens FX66 microcontroller
Source val elf_ma_fx66 : Nat_big_num .numSiemens FX66 microcontroller
STMicroelectronics ST9+ 8/16 bit microcontroller
Source val elf_ma_st9plus : Nat_big_num .numSTMicroelectronics ST9+ 8/16 bit microcontroller
STMicroelectronics ST7 8-bit microcontroller
Source val elf_ma_st7 : Nat_big_num .numSTMicroelectronics ST7 8-bit microcontroller
Motorola MC68HC16 Microcontroller
Source val elf_ma_68hc16 : Nat_big_num .numMotorola MC68HC16 Microcontroller
Motorola MC68HC11 Microcontroller
Source val elf_ma_68hc11 : Nat_big_num .numMotorola MC68HC11 Microcontroller
Motorola MC68HC08 Microcontroller
Source val elf_ma_68hc08 : Nat_big_num .numMotorola MC68HC08 Microcontroller
Motorola MC68HC05 Microcontroller
Source val elf_ma_68hc05 : Nat_big_num .numMotorola MC68HC05 Microcontroller
Silicon Graphics SVx
Source val elf_ma_svx : Nat_big_num .numSilicon Graphics SVx
STMicroelectronics ST19 8-bit microcontroller
Source val elf_ma_st19 : Nat_big_num .numSTMicroelectronics ST19 8-bit microcontroller
Digital VAX
Source val elf_ma_vax : Nat_big_num .numDigital VAX
Axis Communications 32-bit embedded processor
Source val elf_ma_cris : Nat_big_num .numAxis Communications 32-bit embedded processor
Infineon Technologies 32-bit embedded processor
Source val elf_ma_javelin : Nat_big_num .numInfineon Technologies 32-bit embedded processor
Element 14 64-bit DSP Processor
Source val elf_ma_firepath : Nat_big_num .numElement 14 64-bit DSP Processor
Reserved by Intel
Source val elf_ma_intel209 : Nat_big_num .numReserved by Intel
Reserved by Intel
Source val elf_ma_intel208 : Nat_big_num .numReserved by Intel
Reserved by Intel
Source val elf_ma_intel207 : Nat_big_num .numReserved by Intel
Reserved by Intel
Source val elf_ma_intel206 : Nat_big_num .numReserved by Intel
Reserved by Intel
Source val elf_ma_intel205 : Nat_big_num .numReserved by Intel
Reserved by Intel
Source val elf_ma_intel182 : Nat_big_num .numReserved by Intel
Reserved by ARM
Source val elf_ma_arm184 : Nat_big_num .numReserved by ARM
Reserved for future use
Source val elf_ma_reserved6 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved11 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved12 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved13 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved14 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved16 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved24 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved25 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved26 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved27 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved28 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved29 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved30 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved31 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved32 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved33 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved34 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved35 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved121 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved122 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved123 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved124 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved125 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved126 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved127 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved128 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved129 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved130 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved143 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved144 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved145 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved146 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved147 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved148 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved149 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved150 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved151 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved152 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved153 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved154 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved155 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved156 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved157 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved158 : Nat_big_num .numReserved for future use
Reserved for future use
Source val elf_ma_reserved159 : Nat_big_num .numSource val string_of_elf_machine_architecture : Nat_big_num .num -> 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.
Source val elf_ev_none : Nat_big_num .numInvalid version
Current version
Source val elf_ev_current : Nat_big_num .numSource val string_of_elf_version_number : Nat_big_num .num -> string_of_elf_version_number m produces a string representation of the * numeric encoding m of the ELF version number.
Source val is_valid_extended_version_number : Nat_big_num .num -> 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.
Source val elf_ii_mag0 : Nat_big_num .numFile identification
File identification
Source val elf_ii_mag1 : Nat_big_num .numFile identification
File identification
Source val elf_ii_mag2 : Nat_big_num .numFile identification
File identification
Source val elf_ii_mag3 : Nat_big_num .numFile identification
File class
Source val elf_ii_class : Nat_big_num .numSource val elf_ii_data : Nat_big_num .numData encoding
File version
Source val elf_ii_version : Nat_big_num .numFile version
Operating system/ABI identification
Source val elf_ii_osabi : Nat_big_num .numOperating system/ABI identification
ABI version
Source val elf_ii_abiversion : Nat_big_num .numABI version
Start of padding bytes
Source val elf_ii_pad : Nat_big_num .numStart of padding bytes
Size of e*_ident
Source val elf_ii_nident : Nat_big_num .numMagic 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.
Source val elf_class_none : Nat_big_num .numInvalid class
32 bit objects
Source val elf_class_32 : Nat_big_num .num32 bit objects
64 bit objects
Source val elf_class_64 : Nat_big_num .numSource val string_of_elf_file_class : Nat_big_num .num -> 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.
Source val elf_data_none : Nat_big_num .numInvalid data encoding
Two's complement values, least significant byte occupying lowest address
Source val elf_data_2lsb : Nat_big_num .numTwo's complement values, least significant byte occupying lowest address
Two's complement values, most significant byte occupying lowest address
Source val elf_data_2msb : Nat_big_num .numTwo's complement values, most significant byte occupying lowest address
Source val string_of_elf_data_encoding : Nat_big_num .num -> 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.
Source val elf_osabi_none : Nat_big_num .numNo extensions or unspecified
Hewlett-Packard HP-UX
Source val elf_osabi_hpux : Nat_big_num .numHewlett-Packard HP-UX
NetBSD
Source val elf_osabi_netbsd : Nat_big_num .numSource val elf_osabi_gnu : Nat_big_num .numGNU
Linux, historical alias for GNU
Source val elf_osabi_linux : Nat_big_num .numLinux, historical alias for GNU
Sun Solaris
Source val elf_osabi_solaris : Nat_big_num .numSource val elf_osabi_aix : Nat_big_num .numSource val elf_osabi_irix : Nat_big_num .numSource val elf_osabi_freebsd : Nat_big_num .numSource val elf_osabi_tru64 : Nat_big_num .numCompaq Tru64 Unix
Novell Modesto
Source val elf_osabi_modesto : Nat_big_num .numSource val elf_osabi_openbsd : Nat_big_num .numSource val elf_osabi_openvms : Nat_big_num .numOpenVMS
Hewlett-Packard Non-stop Kernel
Source val elf_osabi_nsk : Nat_big_num .numHewlett-Packard Non-stop Kernel
Amiga Research OS
Source val elf_osabi_aros : Nat_big_num .numAmiga Research OS
FenixOS highly-scalable multi-core OS
Source val elf_osabi_fenixos : Nat_big_num .numFenixOS highly-scalable multi-core OS
Nuxi CloudABI
Source val elf_osabi_cloudabi : Nat_big_num .numNuxi CloudABI
Stratus technologies OpenVOS
Source val elf_osabi_openvos : Nat_big_num .numStratus technologies OpenVOS
Source val is_valid_architecture_defined_osabi_version : Nat_big_num .num -> Checks an architecture defined OSABI version is correct, i.e. in the range * 64 to 255 inclusive.
Source val string_of_elf_osabi_version :
(Nat_big_num .num -> -> Nat_big_num .num -> string_of_elf_osabi_version m produces a string representation of the * numeric encoding m of the ELF OSABI version.
ELF Header type
Source val ei_nident : Nat_big_num .numei_nident is the fixed length of the identification field in the * elf32_ehdr type.
elf32_header is the type of headers for 32-bit ELF files.
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.
elf64_header_compare hdr1 hdr2 is an ordering comparison function for * ELF headers suitable for use in sets, finite maps and other ordered * data types.
is_elf32_executable_file hdr checks whether the header hdr states if the * ELF file is of executable type.
Source val is_elf64_executable_file : 'a -> 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.
Source type hdr_print_bundle =
(Nat_big_num .num -> * (Nat_big_num .num -> 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.
string_of_elf32_header hdr_bdl hdr returns a string-based representation * of header hdr using the ABI-specific print bundle hdr_bdl.
string_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.
read_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.
read_elf32_header bs0 reads an ELF header from the byte sequence bs0. * Fails if transcription fails.
read_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.