package linksem
-
linksem_zarith
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package linksem
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
elf_header includes types, functions and other definitions for working with * ELF headers.
Special section header table indices
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).
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.
val elf_ft_none : Nat_big_num.numNo file type
Relocatable file
val elf_ft_rel : Nat_big_num.numRelocatable file
Executable file
val elf_ft_exec : Nat_big_num.numExecutable file
Shared object file
val elf_ft_dyn : Nat_big_num.numShared object file
Core file
val elf_ft_core : Nat_big_num.numCore file
Operating-system specific
val elf_ft_lo_os : Nat_big_num.numOperating-system specific
Operating-system specific
val elf_ft_hi_os : Nat_big_num.numOperating-system specific
Processor specific
val elf_ft_lo_proc : Nat_big_num.numProcessor specific
Processor specific
val elf_ft_hi_proc : Nat_big_num.numProcessor 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.
val is_operating_system_specific_object_file_type_value :
Nat_big_num.num ->
boolis_operating_specific_file_type_value checks whether a numeric value is * reserved by the ABI for operating system-specific purposes.
val is_processor_specific_object_file_type_value : Nat_big_num.num -> boolis_processor_specific_file_type_value checks whether a numeric value is * reserved by the ABI for processor-specific purposes.
ELF machine architectures
val elf_ma_riscv : Nat_big_num.numRISC-V
AMD GPU architecture
val elf_ma_amdgpu : Nat_big_num.numAMD GPU architecture
Moxie processor family
val elf_ma_moxie : Nat_big_num.numMoxie processor family
FTDI Chip FT32 high performance 32-bit RISC architecture
val elf_ma_ft32 : Nat_big_num.numFTDI Chip FT32 high performance 32-bit RISC architecture
Controls and Data Services VISIUMcore processor
val elf_ma_visium : Nat_big_num.numControls and Data Services VISIUMcore processor
Zilog Z80
val elf_ma_z80 : Nat_big_num.numZilog Z80
CSR Kalimba architecture family
val elf_ma_kalimba : Nat_big_num.numCSR Kalimba architecture family
Nanoradio optimised RISC
val elf_ma_norc : Nat_big_num.numNanoradio optimised RISC
iCelero CoolEngine
val elf_ma_cool : Nat_big_num.numiCelero CoolEngine
Cognitive Smart Memory Processor
val elf_ma_coge : Nat_big_num.numCognitive Smart Memory Processor
Paneve CDP architecture family
val elf_ma_cdp : Nat_big_num.numPaneve CDP architecture family
KM211 KVARC processor
val elf_ma_kvarc : Nat_big_num.numKM211 KVARC processor
KM211 KMX8 8-bit processor
val elf_ma_kmx8 : Nat_big_num.numKM211 KMX8 8-bit processor
KM211 KMX16 16-bit processor
val elf_ma_kmx16 : Nat_big_num.numKM211 KMX16 16-bit processor
KM211 KMX32 32-bit processor
val elf_ma_kmx32 : Nat_big_num.numKM211 KMX32 32-bit processor
KM211 KM32 32-bit processor
val elf_ma_km32 : Nat_big_num.numKM211 KM32 32-bit processor
Microchip 8-bit PIC(r) family
val elf_ma_mchp_pic : Nat_big_num.numMicrochip 8-bit PIC(r) family
XMOS xCORE processor family
val elf_ma_xcore : Nat_big_num.numXMOS xCORE processor family
Beyond BA2 CPU architecture
val elf_ma_ba2 : Nat_big_num.numBeyond BA2 CPU architecture
Beyond BA1 CPU architecture
val elf_ma_ba1 : Nat_big_num.numBeyond BA1 CPU architecture
Freescale 56800EX Digital Signal Controller (DSC)
val elf_ma_5600ex : Nat_big_num.numFreescale 56800EX Digital Signal Controller (DSC)
199 Renesas 78KOR family
val elf_ma_78kor : Nat_big_num.num199 Renesas 78KOR family
Broadcom VideoCore V processor
val elf_ma_videocore5 : Nat_big_num.numBroadcom VideoCore V processor
Renesas RL78 family
val elf_ma_rl78 : Nat_big_num.numRenesas RL78 family
Open8 8-bit RISC soft processing core
val elf_ma_open8 : Nat_big_num.numOpen8 8-bit RISC soft processing core
Synopsys ARCompact V2
val elf_ma_arc_compact2 : Nat_big_num.numSynopsys ARCompact V2
KIPO_KAIST Core-A 2nd generation processor family
val elf_ma_corea_2nd : Nat_big_num.numKIPO_KAIST Core-A 2nd generation processor family
KIPO_KAIST Core-A 1st generation processor family
val elf_ma_corea_1st : Nat_big_num.numKIPO_KAIST Core-A 1st generation processor family
CloudShield architecture family
val elf_ma_cloudshield : Nat_big_num.numCloudShield architecture family
Infineon Technologies SLE9X core
val elf_ma_sle9x : Nat_big_num.numInfineon Technologies SLE9X core
Intel L10M
val elf_ma_l10m : Nat_big_num.numIntel L10M
Intel K10M
val elf_ma_k10m : Nat_big_num.numIntel K10M
ARM 64-bit architecture (AARCH64)
val elf_ma_aarch64 : Nat_big_num.numARM 64-bit architecture (AARCH64)
Atmel Corporation 32-bit microprocessor family
val elf_ma_avr32 : Nat_big_num.numAtmel Corporation 32-bit microprocessor family
STMicroelectronics STM8 8-bit microcontroller
val elf_ma_stm8 : Nat_big_num.numSTMicroelectronics STM8 8-bit microcontroller
Tilera TILE64 multicore architecture family
val elf_ma_tile64 : Nat_big_num.numTilera TILE64 multicore architecture family
Tilera TILEPro multicore architecture family
val elf_ma_tilepro : Nat_big_num.numTilera TILEPro multicore architecture family
Xilinix MicroBlaze 32-bit RISC soft processor core
val elf_ma_microblaze : Nat_big_num.numXilinix MicroBlaze 32-bit RISC soft processor core
NVIDIA CUDA architecture
val elf_ma_cuda : Nat_big_num.numNVIDIA CUDA architecture
Tilera TILE-Gx multicore architecture family
val elf_ma_tilegx : Nat_big_num.numTilera TILE-Gx multicore architecture family
Cypress M8C microprocessor
val elf_ma_cypress : Nat_big_num.numCypress M8C microprocessor
Renesas R32C series microprocessors
val elf_ma_r32c : Nat_big_num.numRenesas R32C series microprocessors
NXP Semiconductors TriMedia architecture family
val elf_ma_trimedia : Nat_big_num.numNXP Semiconductors TriMedia architecture family
QUALCOMM DSP6 processor
val elf_ma_qdsp6 : Nat_big_num.numQUALCOMM DSP6 processor
Intel 8051 and variants
val elf_ma_8051 : Nat_big_num.numIntel 8051 and variants
STMicroelectronics STxP7x family of configurable and extensible RISC processors
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
val elf_ma_nds32 : Nat_big_num.numAndes Technology compact code size embedded RISC processor family
Cyan Technology eCOG1X family
val elf_ma_ecog1x : Nat_big_num.numCyan Technology eCOG1X family
Dallas Semiconductor MAXQ30 Core Micro-controllers
val elf_ma_maxq30 : Nat_big_num.numDallas Semiconductor MAXQ30 Core Micro-controllers
New Japan Radio (NJR) 16-bit DSP Processor
val elf_ma_ximo16 : Nat_big_num.numNew Japan Radio (NJR) 16-bit DSP Processor
M2000 Reconfigurable RISC Microprocessor
val elf_ma_manik : Nat_big_num.numM2000 Reconfigurable RISC Microprocessor
Cray Inc. NV2 vector architecture
val elf_ma_craynv2 : Nat_big_num.numCray Inc. NV2 vector architecture
Renesas RX family
val elf_ma_rx : Nat_big_num.numRenesas RX family
Imagination Technologies META processor architecture
val elf_ma_metag : Nat_big_num.numImagination Technologies META processor architecture
MCST Elbrus general purpose hardware architecture
val elf_ma_mcst_elbrus : Nat_big_num.numMCST Elbrus general purpose hardware architecture
Cyan Technology eCOG16 family
val elf_ma_ecog16 : Nat_big_num.numCyan Technology eCOG16 family
National Semiconductor CompactRISC CR16 16-bit microprocessor
val elf_ma_cr16 : Nat_big_num.numNational Semiconductor CompactRISC CR16 16-bit microprocessor
Freescale Extended Time Processing Unit
val elf_ma_etpu : Nat_big_num.numFreescale Extended Time Processing Unit
Altium TSK3000 core
val elf_ma_tsk3000 : Nat_big_num.numAltium TSK3000 core
Freescale RS08 embedded processor
val elf_ma_rs08 : Nat_big_num.numFreescale RS08 embedded processor
Analog Devices SHARC family of 32-bit DSP processors
val elf_ma_sharc : Nat_big_num.numAnalog Devices SHARC family of 32-bit DSP processors
Cyan Technology eCOG2 microprocessor
val elf_ma_ecog2 : Nat_big_num.numCyan Technology eCOG2 microprocessor
Sunplus S+core7 RISC processor
val elf_ma_ccore7 : Nat_big_num.numSunplus S+core7 RISC processor
New Japan Radio (NJR) 24-bit DSP Processor
val elf_ma_dsp24 : Nat_big_num.numNew Japan Radio (NJR) 24-bit DSP Processor
Broadcom VideoCore III processor
val elf_ma_videocore3 : Nat_big_num.numBroadcom VideoCore III processor
RISC processor for Lattice FPGA architecture
val elf_ma_latticemico32 : Nat_big_num.numRISC processor for Lattice FPGA architecture
Seiko Epson C17 family
val elf_ma_c17 : Nat_big_num.numSeiko Epson C17 family
The Texas Instruments TMS320C6000 DSP family
val elf_ma_c6000 : Nat_big_num.numThe Texas Instruments TMS320C6000 DSP family
The Texas Instruments TMS320C2000 DSP family
val elf_ma_c2000 : Nat_big_num.numThe Texas Instruments TMS320C2000 DSP family
The Texas Instruments TMS320C55x DSP family
val elf_ma_c5500 : Nat_big_num.numThe Texas Instruments TMS320C55x DSP family
STMicroelectronics 64bit VLIW Data Signal Processor
val elf_ma_mmdsp_plus : Nat_big_num.numSTMicroelectronics 64bit VLIW Data Signal Processor
LSI Logic 16-bit DSP Processor
val elf_ma_zsp : Nat_big_num.numLSI Logic 16-bit DSP Processor
Donald Knuth's educational 64-bit processor
val elf_ma_mmix : Nat_big_num.numDonald Knuth's educational 64-bit processor
Harvard University machine-independent object files
val elf_ma_huany : Nat_big_num.numHarvard University machine-independent object files
SiTera Prism
val elf_ma_prism : Nat_big_num.numSiTera Prism
Atmel AVR 8-bit microcontroller
val elf_ma_avr : Nat_big_num.numAtmel AVR 8-bit microcontroller
Fujitsu FR30
val elf_ma_fr30 : Nat_big_num.numFujitsu FR30
Mitsubishi D10V
val elf_ma_d10v : Nat_big_num.numMitsubishi D10V
Mitsubishi D30V
val elf_ma_d30v : Nat_big_num.numMitsubishi D30V
NEC v850
val elf_ma_v850 : Nat_big_num.numNEC v850
Mitsubishi M32R
val elf_ma_m32r : Nat_big_num.numMitsubishi M32R
Matsushita MN10300
val elf_ma_mn10300 : Nat_big_num.numMatsushita MN10300
Matsushita MN10200
val elf_ma_mn10200 : Nat_big_num.numMatsushita MN10200
picoJava
val elf_ma_pj : Nat_big_num.numpicoJava
OpenRISC 32-bit embedded processor
val elf_ma_openrisc : Nat_big_num.numOpenRISC 32-bit embedded processor
ARC International ARCompact processor (old spelling/synonym: ELF_MA_ARC_A5)
val elf_ma_arc_compact : Nat_big_num.numARC International ARCompact processor (old spelling/synonym: ELF_MA_ARC_A5)
Tensilica Xtensa Architecture
val elf_ma_xtensa : Nat_big_num.numTensilica Xtensa Architecture
Alphamosaic VideoCore processor
val elf_ma_videocore : Nat_big_num.numAlphamosaic VideoCore processor
Thompson Multimedia General Purpose Processor
val elf_ma_tmm_gpp : Nat_big_num.numThompson Multimedia General Purpose Processor
National Semiconductor 32000 series
val elf_ma_ns32k : Nat_big_num.numNational Semiconductor 32000 series
Tenor Network TPC processor
val elf_ma_tpc : Nat_big_num.numTenor Network TPC processor
Trebia SNP 1000 processor
val elf_ma_snp1k : Nat_big_num.numTrebia SNP 1000 processor
STMicroelectronics ST200 microcontroller
val elf_ma_st200 : Nat_big_num.numSTMicroelectronics ST200 microcontroller
Ubicom IP2xxx microcontroller family
val elf_ma_ip2k : Nat_big_num.numUbicom IP2xxx microcontroller family
MAX Processor
val elf_ma_max : Nat_big_num.numMAX Processor
National Semiconductor CompactRISC microprocessor
val elf_ma_cr : Nat_big_num.numNational Semiconductor CompactRISC microprocessor
Fujitsu F2MC16
val elf_ma_f2mc16 : Nat_big_num.numFujitsu F2MC16
Texas Instruments embedded microcontroller msp430
val elf_ma_msp430 : Nat_big_num.numTexas Instruments embedded microcontroller msp430
Analog Devices Blackfin (DSP) processor
val elf_ma_blackfin : Nat_big_num.numAnalog Devices Blackfin (DSP) processor
S1C33 Family of Seiko Epson processors
val elf_ma_se_c33 : Nat_big_num.numS1C33 Family of Seiko Epson processors
Sharp embedded microprocessor
val elf_ma_sep : Nat_big_num.numSharp embedded microprocessor
Arca RISC Microprocessor
val elf_ma_arca : Nat_big_num.numArca RISC Microprocessor
Microprocessor series from PKU-Unity Ltd. and MPRC of Peking University
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
val elf_ma_excess : Nat_big_num.numeXcess: 16/32/64-bit configurable embedded CPU
Icera Semiconductor Inc. Deep Execution Processor
val elf_ma_dxp : Nat_big_num.numIcera Semiconductor Inc. Deep Execution Processor
Altera Nios II soft-core processor
val elf_ma_altera_nios2 : Nat_big_num.numAltera Nios II soft-core processor
National Semiconductor CompactRISC CRX microprocessor
val elf_ma_crx : Nat_big_num.numNational Semiconductor CompactRISC CRX microprocessor
Motorola XGATE embedded processor
val elf_ma_xgate : Nat_big_num.numMotorola XGATE embedded processor
Infineon C16x/XC16x processor
val elf_ma_c166 : Nat_big_num.numInfineon C16x/XC16x processor
Renesas M16C series microprocessors
val elf_ma_m16c : Nat_big_num.numRenesas M16C series microprocessors
Microchip Technology dsPIC30F Digital Signal Controller
val elf_ma_dspic30f : Nat_big_num.numMicrochip Technology dsPIC30F Digital Signal Controller
Freescale Communication Engine RISC core
val elf_ma_ce : Nat_big_num.numFreescale Communication Engine RISC core
Renesas M32C series microprocessors
val elf_ma_m32c : Nat_big_num.numRenesas M32C series microprocessors
No machine
val elf_ma_none : Nat_big_num.numNo machine
AT&T WE 32100
val elf_ma_m32 : Nat_big_num.numAT&T WE 32100
SPARC
val elf_ma_sparc : Nat_big_num.numSPARC
Intel 80386
val elf_ma_386 : Nat_big_num.numIntel 80386
Motorola 68000
val elf_ma_68k : Nat_big_num.numMotorola 68000
Motorola 88000
val elf_ma_88k : Nat_big_num.numMotorola 88000
Intel 80860
val elf_ma_860 : Nat_big_num.numIntel 80860
MIPS I Architecture
val elf_ma_mips : Nat_big_num.numMIPS I Architecture
IBM System/370 Processor
val elf_ma_s370 : Nat_big_num.numIBM System/370 Processor
MIPS RS3000 Little-endian
val elf_ma_mips_rs3_le : Nat_big_num.numMIPS RS3000 Little-endian
Hewlett-Packard PA-RISC
val elf_ma_parisc : Nat_big_num.numHewlett-Packard PA-RISC
Fujitsu VPP500
val elf_ma_vpp500 : Nat_big_num.numFujitsu VPP500
Enhanced instruction set SPARC
val elf_ma_sparc32plus : Nat_big_num.numEnhanced instruction set SPARC
Intel 80960
val elf_ma_960 : Nat_big_num.numIntel 80960
PowerPC
val elf_ma_ppc : Nat_big_num.numPowerPC
64-bit PowerPC
val elf_ma_ppc64 : Nat_big_num.num64-bit PowerPC
IBM System/390 Processor
val elf_ma_s390 : Nat_big_num.numIBM System/390 Processor
IBM SPU/SPC
val elf_ma_spu : Nat_big_num.numIBM SPU/SPC
NEC V800
val elf_ma_v800 : Nat_big_num.numNEC V800
Fujitsu FR20
val elf_ma_fr20 : Nat_big_num.numFujitsu FR20
TRW RH-32
val elf_ma_rh32 : Nat_big_num.numTRW RH-32
Motorola RCE
val elf_ma_rce : Nat_big_num.numMotorola RCE
ARM 32-bit architecture (AARCH32)
val elf_ma_arm : Nat_big_num.numARM 32-bit architecture (AARCH32)
Digital Alpha
val elf_ma_alpha : Nat_big_num.numDigital Alpha
Hitachi SH
val elf_ma_sh : Nat_big_num.numHitachi SH
SPARC Version 9
val elf_ma_sparcv9 : Nat_big_num.numSPARC Version 9
Siemens TriCore embedded processor
val elf_ma_tricore : Nat_big_num.numSiemens TriCore embedded processor
Argonaut RISC Core, Argonaut Technologies Inc.
val elf_ma_arc : Nat_big_num.numArgonaut RISC Core, Argonaut Technologies Inc.
Hitachi H8/300
val elf_ma_h8_300 : Nat_big_num.numHitachi H8/300
Hitachi H8/300H
val elf_ma_h8_300h : Nat_big_num.numHitachi H8/300H
Hitachi H8S
val elf_ma_h8s : Nat_big_num.numHitachi H8S
Hitachi H8/500
val elf_ma_h8_500 : Nat_big_num.numHitachi H8/500
Intel IA-64 processor architecture
val elf_ma_ia_64 : Nat_big_num.numIntel IA-64 processor architecture
Stanford MIPS-X
val elf_ma_mips_x : Nat_big_num.numStanford MIPS-X
Motorola ColdFire
val elf_ma_coldfire : Nat_big_num.numMotorola ColdFire
Motorola M68HC12
val elf_ma_68hc12 : Nat_big_num.numMotorola M68HC12
Fujitsu MMA Multimedia Accelerator
val elf_ma_mma : Nat_big_num.numFujitsu MMA Multimedia Accelerator
Siemens PCP
val elf_ma_pcp : Nat_big_num.numSiemens PCP
Sony nCPU embedded RISC processor
val elf_ma_ncpu : Nat_big_num.numSony nCPU embedded RISC processor
Denso NDR1 microprocessor
val elf_ma_ndr1 : Nat_big_num.numDenso NDR1 microprocessor
Motorola Star*Core processor
val elf_ma_starcore : Nat_big_num.numMotorola Star*Core processor
Toyota ME16 processor
val elf_ma_me16 : Nat_big_num.numToyota ME16 processor
STMicroelectronics ST100 processor
val elf_ma_st100 : Nat_big_num.numSTMicroelectronics ST100 processor
Advanced Logic Corp. TinyJ embedded processor family
val elf_ma_tinyj : Nat_big_num.numAdvanced Logic Corp. TinyJ embedded processor family
AMD x86-64 architecture
val elf_ma_x86_64 : Nat_big_num.numAMD x86-64 architecture
Sony DSP Processor
val elf_ma_pdsp : Nat_big_num.numSony DSP Processor
Digital Equipment Corp. PDP-10
val elf_ma_pdp10 : Nat_big_num.numDigital Equipment Corp. PDP-10
Digital Equipment Corp. PDP-11
val elf_ma_pdp11 : Nat_big_num.numDigital Equipment Corp. PDP-11
Siemens FX66 microcontroller
val elf_ma_fx66 : Nat_big_num.numSiemens FX66 microcontroller
STMicroelectronics ST9+ 8/16 bit microcontroller
val elf_ma_st9plus : Nat_big_num.numSTMicroelectronics ST9+ 8/16 bit microcontroller
STMicroelectronics ST7 8-bit microcontroller
val elf_ma_st7 : Nat_big_num.numSTMicroelectronics ST7 8-bit microcontroller
Motorola MC68HC16 Microcontroller
val elf_ma_68hc16 : Nat_big_num.numMotorola MC68HC16 Microcontroller
Motorola MC68HC11 Microcontroller
val elf_ma_68hc11 : Nat_big_num.numMotorola MC68HC11 Microcontroller
Motorola MC68HC08 Microcontroller
val elf_ma_68hc08 : Nat_big_num.numMotorola MC68HC08 Microcontroller
Motorola MC68HC05 Microcontroller
val elf_ma_68hc05 : Nat_big_num.numMotorola MC68HC05 Microcontroller
Silicon Graphics SVx
val elf_ma_svx : Nat_big_num.numSilicon Graphics SVx
STMicroelectronics ST19 8-bit microcontroller
val elf_ma_st19 : Nat_big_num.numSTMicroelectronics ST19 8-bit microcontroller
Digital VAX
val elf_ma_vax : Nat_big_num.numDigital VAX
Axis Communications 32-bit embedded processor
val elf_ma_cris : Nat_big_num.numAxis Communications 32-bit embedded processor
Infineon Technologies 32-bit embedded processor
val elf_ma_javelin : Nat_big_num.numInfineon Technologies 32-bit embedded processor
Element 14 64-bit DSP Processor
val elf_ma_firepath : Nat_big_num.numElement 14 64-bit DSP Processor
Reserved by Intel
val elf_ma_intel209 : Nat_big_num.numReserved by Intel
Reserved by Intel
val elf_ma_intel208 : Nat_big_num.numReserved by Intel
Reserved by Intel
val elf_ma_intel207 : Nat_big_num.numReserved by Intel
Reserved by Intel
val elf_ma_intel206 : Nat_big_num.numReserved by Intel
Reserved by Intel
val elf_ma_intel205 : Nat_big_num.numReserved by Intel
Reserved by Intel
val elf_ma_intel182 : Nat_big_num.numReserved by Intel
Reserved by ARM
val elf_ma_arm184 : Nat_big_num.numReserved by ARM
Reserved for future use
val elf_ma_reserved6 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved11 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved12 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved13 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved14 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved16 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved24 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved25 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved26 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved27 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved28 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved29 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved30 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved31 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved32 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved33 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved34 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved35 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved121 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved122 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved123 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved124 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved125 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved126 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved127 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved128 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved129 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved130 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved143 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved144 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved145 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved146 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved147 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved148 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved149 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved150 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved151 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved152 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved153 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved154 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved155 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved156 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved157 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved158 : Nat_big_num.numReserved for future use
Reserved for future use
val elf_ma_reserved159 : Nat_big_num.numReserved for future use
val string_of_elf_machine_architecture : Nat_big_num.num -> stringstring_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.
val elf_ev_none : Nat_big_num.numInvalid version
Current version
val elf_ev_current : Nat_big_num.numCurrent version
val string_of_elf_version_number : Nat_big_num.num -> stringstring_of_elf_version_number m produces a string representation of the * numeric encoding m of the ELF version number.
val is_valid_extended_version_number : Nat_big_num.num -> boolCheck 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.
val elf_ii_mag0 : Nat_big_num.numFile identification
File identification
val elf_ii_mag1 : Nat_big_num.numFile identification
File identification
val elf_ii_mag2 : Nat_big_num.numFile identification
File identification
val elf_ii_mag3 : Nat_big_num.numFile identification
File class
val elf_ii_class : Nat_big_num.numFile class
Data encoding
val elf_ii_data : Nat_big_num.numData encoding
File version
val elf_ii_version : Nat_big_num.numFile version
Operating system/ABI identification
val elf_ii_osabi : Nat_big_num.numOperating system/ABI identification
ABI version
val elf_ii_abiversion : Nat_big_num.numABI version
Start of padding bytes
val elf_ii_pad : Nat_big_num.numStart of padding bytes
Size of e*_ident
val elf_ii_nident : Nat_big_num.numSize of e*_ident
Magic number indices. A file's first 4 bytes hold a ``magic number,'' * identifying the file as an ELF object file.
val elf_mn_mag0 : Uint32_wrapper.uint32Position: e*_identelf_ii_mag0, 0x7f magic number
Position: e*_identelf_ii_mag1, 'E' format identifier
val elf_mn_mag1 : Uint32_wrapper.uint32Position: e*_identelf_ii_mag1, 'E' format identifier
Position: e*_identelf_ii_mag2, 'L' format identifier
val elf_mn_mag2 : Uint32_wrapper.uint32Position: e*_identelf_ii_mag2, 'L' format identifier
Position: e*_identelf_ii_mag3, 'F' format identifier
val elf_mn_mag3 : Uint32_wrapper.uint32Position: 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.
val elf_class_none : Nat_big_num.numInvalid class
32 bit objects
val elf_class_32 : Nat_big_num.num32 bit objects
64 bit objects
val elf_class_64 : Nat_big_num.num64 bit objects
val string_of_elf_file_class : Nat_big_num.num -> stringstring_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.
val elf_data_none : Nat_big_num.numInvalid data encoding
Two's complement values, least significant byte occupying lowest address
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
val elf_data_2msb : Nat_big_num.numTwo's complement values, most significant byte occupying lowest address
val string_of_elf_data_encoding : Nat_big_num.num -> stringstring_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.
val elf_osabi_none : Nat_big_num.numNo extensions or unspecified
Hewlett-Packard HP-UX
val elf_osabi_hpux : Nat_big_num.numHewlett-Packard HP-UX
NetBSD
val elf_osabi_netbsd : Nat_big_num.numNetBSD
GNU
val elf_osabi_gnu : Nat_big_num.numGNU
Linux, historical alias for GNU
val elf_osabi_linux : Nat_big_num.numLinux, historical alias for GNU
Sun Solaris
val elf_osabi_solaris : Nat_big_num.numSun Solaris
AIX
val elf_osabi_aix : Nat_big_num.numAIX
IRIX
val elf_osabi_irix : Nat_big_num.numIRIX
FreeBSD
val elf_osabi_freebsd : Nat_big_num.numFreeBSD
Compaq Tru64 Unix
val elf_osabi_tru64 : Nat_big_num.numCompaq Tru64 Unix
Novell Modesto
val elf_osabi_modesto : Nat_big_num.numNovell Modesto
OpenBSD
val elf_osabi_openbsd : Nat_big_num.numOpenBSD
OpenVMS
val elf_osabi_openvms : Nat_big_num.numOpenVMS
Hewlett-Packard Non-stop Kernel
val elf_osabi_nsk : Nat_big_num.numHewlett-Packard Non-stop Kernel
Amiga Research OS
val elf_osabi_aros : Nat_big_num.numAmiga Research OS
FenixOS highly-scalable multi-core OS
val elf_osabi_fenixos : Nat_big_num.numFenixOS highly-scalable multi-core OS
Nuxi CloudABI
val elf_osabi_cloudabi : Nat_big_num.numNuxi CloudABI
Stratus technologies OpenVOS
val elf_osabi_openvos : Nat_big_num.numStratus technologies OpenVOS
val is_valid_architecture_defined_osabi_version : Nat_big_num.num -> boolChecks an architecture defined OSABI version is correct, i.e. in the range * 64 to 255 inclusive.
val string_of_elf_osabi_version :
(Nat_big_num.num -> string) ->
Nat_big_num.num ->
stringstring_of_elf_osabi_version m produces a string representation of the * numeric encoding m of the ELF OSABI version.
ELF Header type
val ei_nident : Nat_big_num.numei_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.
val is_valid_elf32_header : elf32_header -> boolis_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.
val is_valid_elf64_header : elf64_header -> boolis_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.
val elf32_header_compare : elf32_header -> elf32_header -> intelf32_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_classval elf64_header_compare : elf64_header -> elf64_header -> intelf64_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_classval is_elf32_executable_file : elf32_header -> boolis_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.
val is_elf32_relocatable_file : elf32_header -> boolis_elf32_relocatable_file hdr checks whether the header hdr states if the * ELF file is of relocatable type.
val is_elf64_relocatable_file : elf64_header -> boolis_elf64_relocatable_file hdr checks whether the header hdr states if the * ELF file is of relocatable type.
val is_elf32_linkable_file : elf32_header -> boolis_elf32_linkable_file hdr checks whether the header hdr states if the * ELF file is of linkable (shared object or relocatable) type.
val is_elf64_linkable_file : elf64_header -> boolis_elf64_linkable_file hdr checks whether the header hdr states if the * ELF file is of linkable (shared object or relocatable) type.
val get_elf32_machine_architecture : elf32_header -> Nat_big_num.numget_elf32_machine_architecture hdr returns the ELF file's declared machine * architecture, extracting the information from header hdr.
val get_elf64_machine_architecture : elf64_header -> Nat_big_num.numget_elf64_machine_architecture hdr returns the ELF file's declared machine * architecture, extracting the information from header hdr.
val get_elf32_osabi : elf32_header -> Nat_big_num.numget_elf32_osabi hdr returns the ELF file's declared OS/ABI * architecture, extracting the information from header hdr.
val get_elf64_osabi : elf64_header -> Nat_big_num.numget_elf64_osabi hdr returns the ELF file's declared OS/ABI * architecture, extracting the information from header hdr.
val get_elf32_data_encoding : elf32_header -> Nat_big_num.numget_elf32_data_encoding hdr returns the ELF file's declared data * encoding, extracting the information from header hdr.
val get_elf64_data_encoding : elf64_header -> Nat_big_num.numget_elf64_data_encoding hdr returns the ELF file's declared data * encoding, extracting the information from header hdr.
val get_elf32_file_class : elf32_header -> Nat_big_num.numget_elf32_file_class hdr returns the ELF file's declared file * class, extracting the information from header hdr.
val get_elf64_file_class : elf64_header -> Nat_big_num.numget_elf64_file_class hdr returns the ELF file's declared file * class, extracting the information from header hdr.
val get_elf32_version_number : elf32_header -> Nat_big_num.numget_elf32_version_number hdr returns the ELF file's declared version * number, extracting the information from header hdr.
val get_elf64_version_number : elf64_header -> Nat_big_num.numget_elf64_version_number hdr returns the ELF file's declared version * number, extracting the information from header hdr.
val is_valid_elf32_version_numer : elf32_header -> boolis_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.
val is_valid_elf64_version_numer : elf64_header -> boolis_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.
val get_elf32_abi_version : elf32_header -> Nat_big_num.numget_elf32_abi_version hdr returns the ELF file's declared ABI version * number, extracting the information from header hdr.
val get_elf64_abi_version : elf64_header -> Nat_big_num.numget_elf64_abi_version hdr returns the ELF file's declared ABI version * number, extracting the information from header hdr.
val deduce_endianness : Uint32_wrapper.uint32 list -> Endianness.endiannessdeduce_endianness uc deduces the endianness of an ELF file based on the ELF * header's magic number uc.
val get_elf32_header_endianness : elf32_header -> Endianness.endiannessget_elf32_header_endianness hdr returns the endianness of the ELF file * as declared in its header, hdr.
val get_elf64_header_endianness : elf64_header -> Endianness.endiannessget_elf64_header_endianness hdr returns the endianness of the ELF file * as declared in its header, hdr.
val has_elf32_header_associated_entry_point : elf32_header -> boolhas_elf32_header_associated_entry_point hdr checks whether the header * hdr declares an entry point for the program.
val has_elf64_header_associated_entry_point : elf64_header -> boolhas_elf64_header_associated_entry_point hdr checks whether the header * hdr declares an entry point for the program.
val has_elf32_header_string_table : elf32_header -> boolhas_elf32_header_string_table hdr checks whether the header * hdr declares whether the program has a string table or not.
val has_elf64_header_string_table : elf64_header -> boolhas_elf64_header_string_table hdr checks whether the header * hdr declares whether the program has a string table or not.
val is_elf32_header_section_size_in_section_header_table : elf32_header -> boolis_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.
val is_elf64_header_section_size_in_section_header_table : elf64_header -> boolis_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.
val is_elf32_header_string_table_index_in_link : elf32_header -> boolis_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.
val is_elf64_header_string_table_index_in_link : elf64_header -> boolis_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.
type hdr_print_bundle =
(Nat_big_num.num -> string) * (Nat_big_num.num -> string)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 string_of_elf32_header_default : elf32_header -> stringval string_of_elf64_header_default : elf64_header -> stringval instance_Show_Show_Elf_header_elf32_header_dict :
elf32_header Show.show_classval instance_Show_Show_Elf_header_elf64_header_dict :
elf64_header Show.show_classval 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.
val bytes_of_elf32_header : elf32_header -> Byte_sequence_wrapper.byte_sequencebytes_of_elf32_header hdr blits an ELF header hdr to a byte sequence, * ready for transcription to a binary file.
val bytes_of_elf64_header : elf64_header -> Byte_sequence_wrapper.byte_sequencebytes_of_elf64_header hdr blits an ELF header hdr to a byte sequence, * ready for transcription to a binary file.
val is_elf32_header_padding_correct : elf32_header -> boolval is_magic_number_correct : Uint32_wrapper.uint32 list -> boolval 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.
val is_elf32_header_class_correct : elf32_header -> boolis_elf32_header_class_correct hdr checks whether the declared file class * is correct.
val is_elf64_header_class_correct : elf64_header -> boolis_elf64_header_class_correct hdr checks whether the declared file class * is correct.
val is_elf32_header_version_correct : elf32_header -> boolis_elf32_header_version_correct hdr checks whether the declared file version * is correct.
val is_elf64_header_version_correct : elf64_header -> boolis_elf64_header_version_correct hdr checks whether the declared file version * is correct.
val is_elf32_header_valid : elf32_header -> boolis_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).
val get_elf32_header_program_table_size : elf32_header -> Nat_big_num.numget_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.
val get_elf64_header_program_table_size : elf64_header -> Nat_big_num.numget_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.
val is_elf32_header_section_table_present : elf32_header -> boolis_elf32_header_section_table_present calculates whether a section table * is present in the ELF file or not.
val is_elf64_header_section_table_present : elf64_header -> boolis_elf64_header_section_table_present calculates whether a section table * is present in the ELF file or not.
val get_elf32_header_section_table_size : elf32_header -> Nat_big_num.numget_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.
val get_elf64_header_section_table_size : elf64_header -> Nat_big_num.numget_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.