package linksem

  1. Overview
  2. Docs
Legend:
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.num

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).

val shn_xindex : Nat_big_num.num

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.

val elf_ft_none : Nat_big_num.num

No file type

Relocatable file

val elf_ft_rel : Nat_big_num.num

Relocatable file

Executable file

val elf_ft_exec : Nat_big_num.num

Executable file

Shared object file

val elf_ft_dyn : Nat_big_num.num

Shared object file

Core file

val elf_ft_core : Nat_big_num.num

Core file

Operating-system specific

val elf_ft_lo_os : Nat_big_num.num

Operating-system specific

Operating-system specific

val elf_ft_hi_os : Nat_big_num.num

Operating-system specific

Processor specific

val elf_ft_lo_proc : Nat_big_num.num

Processor specific

Processor specific

val elf_ft_hi_proc : Nat_big_num.num

Processor specific

val string_of_elf_file_type : (Nat_big_num.num -> string) -> (Nat_big_num.num -> string) -> Nat_big_num.num -> string

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.

val is_operating_system_specific_object_file_type_value : Nat_big_num.num -> bool

is_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 -> bool

is_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.num

RISC-V

AMD GPU architecture

val elf_ma_amdgpu : Nat_big_num.num

AMD GPU architecture

Moxie processor family

val elf_ma_moxie : Nat_big_num.num

Moxie processor family

FTDI Chip FT32 high performance 32-bit RISC architecture

val elf_ma_ft32 : Nat_big_num.num

FTDI Chip FT32 high performance 32-bit RISC architecture

Controls and Data Services VISIUMcore processor

val elf_ma_visium : Nat_big_num.num

Controls and Data Services VISIUMcore processor

Zilog Z80

val elf_ma_z80 : Nat_big_num.num

Zilog Z80

CSR Kalimba architecture family

val elf_ma_kalimba : Nat_big_num.num

CSR Kalimba architecture family

Nanoradio optimised RISC

val elf_ma_norc : Nat_big_num.num

Nanoradio optimised RISC

iCelero CoolEngine

val elf_ma_cool : Nat_big_num.num

iCelero CoolEngine

Cognitive Smart Memory Processor

val elf_ma_coge : Nat_big_num.num

Cognitive Smart Memory Processor

Paneve CDP architecture family

val elf_ma_cdp : Nat_big_num.num

Paneve CDP architecture family

KM211 KVARC processor

val elf_ma_kvarc : Nat_big_num.num

KM211 KVARC processor

KM211 KMX8 8-bit processor

val elf_ma_kmx8 : Nat_big_num.num

KM211 KMX8 8-bit processor

KM211 KMX16 16-bit processor

val elf_ma_kmx16 : Nat_big_num.num

KM211 KMX16 16-bit processor

KM211 KMX32 32-bit processor

val elf_ma_kmx32 : Nat_big_num.num

KM211 KMX32 32-bit processor

KM211 KM32 32-bit processor

val elf_ma_km32 : Nat_big_num.num

KM211 KM32 32-bit processor

Microchip 8-bit PIC(r) family

val elf_ma_mchp_pic : Nat_big_num.num

Microchip 8-bit PIC(r) family

XMOS xCORE processor family

val elf_ma_xcore : Nat_big_num.num

XMOS xCORE processor family

Beyond BA2 CPU architecture

val elf_ma_ba2 : Nat_big_num.num

Beyond BA2 CPU architecture

Beyond BA1 CPU architecture

val elf_ma_ba1 : Nat_big_num.num

Beyond BA1 CPU architecture

Freescale 56800EX Digital Signal Controller (DSC)

val elf_ma_5600ex : Nat_big_num.num

Freescale 56800EX Digital Signal Controller (DSC)

199 Renesas 78KOR family

val elf_ma_78kor : Nat_big_num.num

199 Renesas 78KOR family

Broadcom VideoCore V processor

val elf_ma_videocore5 : Nat_big_num.num

Broadcom VideoCore V processor

Renesas RL78 family

val elf_ma_rl78 : Nat_big_num.num

Renesas RL78 family

Open8 8-bit RISC soft processing core

val elf_ma_open8 : Nat_big_num.num

Open8 8-bit RISC soft processing core

Synopsys ARCompact V2

val elf_ma_arc_compact2 : Nat_big_num.num

Synopsys ARCompact V2

KIPO_KAIST Core-A 2nd generation processor family

val elf_ma_corea_2nd : Nat_big_num.num

KIPO_KAIST Core-A 2nd generation processor family

KIPO_KAIST Core-A 1st generation processor family

val elf_ma_corea_1st : Nat_big_num.num

KIPO_KAIST Core-A 1st generation processor family

CloudShield architecture family

val elf_ma_cloudshield : Nat_big_num.num

CloudShield architecture family

Infineon Technologies SLE9X core

val elf_ma_sle9x : Nat_big_num.num

Infineon Technologies SLE9X core

Intel L10M

val elf_ma_l10m : Nat_big_num.num

Intel L10M

Intel K10M

val elf_ma_k10m : Nat_big_num.num

Intel K10M

ARM 64-bit architecture (AARCH64)

val elf_ma_aarch64 : Nat_big_num.num

ARM 64-bit architecture (AARCH64)

Atmel Corporation 32-bit microprocessor family

val elf_ma_avr32 : Nat_big_num.num

Atmel Corporation 32-bit microprocessor family

STMicroelectronics STM8 8-bit microcontroller

val elf_ma_stm8 : Nat_big_num.num

STMicroelectronics STM8 8-bit microcontroller

Tilera TILE64 multicore architecture family

val elf_ma_tile64 : Nat_big_num.num

Tilera TILE64 multicore architecture family

Tilera TILEPro multicore architecture family

val elf_ma_tilepro : Nat_big_num.num

Tilera TILEPro multicore architecture family

Xilinix MicroBlaze 32-bit RISC soft processor core

val elf_ma_microblaze : Nat_big_num.num

Xilinix MicroBlaze 32-bit RISC soft processor core

NVIDIA CUDA architecture

val elf_ma_cuda : Nat_big_num.num

NVIDIA CUDA architecture

Tilera TILE-Gx multicore architecture family

val elf_ma_tilegx : Nat_big_num.num

Tilera TILE-Gx multicore architecture family

Cypress M8C microprocessor

val elf_ma_cypress : Nat_big_num.num

Cypress M8C microprocessor

Renesas R32C series microprocessors

val elf_ma_r32c : Nat_big_num.num

Renesas R32C series microprocessors

NXP Semiconductors TriMedia architecture family

val elf_ma_trimedia : Nat_big_num.num

NXP Semiconductors TriMedia architecture family

QUALCOMM DSP6 processor

val elf_ma_qdsp6 : Nat_big_num.num

QUALCOMM DSP6 processor

Intel 8051 and variants

val elf_ma_8051 : Nat_big_num.num

Intel 8051 and variants

STMicroelectronics STxP7x family of configurable and extensible RISC processors

val elf_ma_stxp7x : Nat_big_num.num

STMicroelectronics STxP7x family of configurable and extensible RISC processors

Andes Technology compact code size embedded RISC processor family

val elf_ma_nds32 : Nat_big_num.num

Andes Technology compact code size embedded RISC processor family

Cyan Technology eCOG1X family

val elf_ma_ecog1x : Nat_big_num.num

Cyan Technology eCOG1X family

Dallas Semiconductor MAXQ30 Core Micro-controllers

val elf_ma_maxq30 : Nat_big_num.num

Dallas Semiconductor MAXQ30 Core Micro-controllers

New Japan Radio (NJR) 16-bit DSP Processor

val elf_ma_ximo16 : Nat_big_num.num

New Japan Radio (NJR) 16-bit DSP Processor

M2000 Reconfigurable RISC Microprocessor

val elf_ma_manik : Nat_big_num.num

M2000 Reconfigurable RISC Microprocessor

Cray Inc. NV2 vector architecture

val elf_ma_craynv2 : Nat_big_num.num

Cray Inc. NV2 vector architecture

Renesas RX family

val elf_ma_rx : Nat_big_num.num

Renesas RX family

Imagination Technologies META processor architecture

val elf_ma_metag : Nat_big_num.num

Imagination Technologies META processor architecture

MCST Elbrus general purpose hardware architecture

val elf_ma_mcst_elbrus : Nat_big_num.num

MCST Elbrus general purpose hardware architecture

Cyan Technology eCOG16 family

val elf_ma_ecog16 : Nat_big_num.num

Cyan Technology eCOG16 family

National Semiconductor CompactRISC CR16 16-bit microprocessor

val elf_ma_cr16 : Nat_big_num.num

National Semiconductor CompactRISC CR16 16-bit microprocessor

Freescale Extended Time Processing Unit

val elf_ma_etpu : Nat_big_num.num

Freescale Extended Time Processing Unit

Altium TSK3000 core

val elf_ma_tsk3000 : Nat_big_num.num

Altium TSK3000 core

Freescale RS08 embedded processor

val elf_ma_rs08 : Nat_big_num.num

Freescale RS08 embedded processor

Analog Devices SHARC family of 32-bit DSP processors

val elf_ma_sharc : Nat_big_num.num

Analog Devices SHARC family of 32-bit DSP processors

Cyan Technology eCOG2 microprocessor

val elf_ma_ecog2 : Nat_big_num.num

Cyan Technology eCOG2 microprocessor

Sunplus S+core7 RISC processor

val elf_ma_ccore7 : Nat_big_num.num

Sunplus S+core7 RISC processor

New Japan Radio (NJR) 24-bit DSP Processor

val elf_ma_dsp24 : Nat_big_num.num

New Japan Radio (NJR) 24-bit DSP Processor

Broadcom VideoCore III processor

val elf_ma_videocore3 : Nat_big_num.num

Broadcom VideoCore III processor

RISC processor for Lattice FPGA architecture

val elf_ma_latticemico32 : Nat_big_num.num

RISC processor for Lattice FPGA architecture

Seiko Epson C17 family

val elf_ma_c17 : Nat_big_num.num

Seiko Epson C17 family

The Texas Instruments TMS320C6000 DSP family

val elf_ma_c6000 : Nat_big_num.num

The Texas Instruments TMS320C6000 DSP family

The Texas Instruments TMS320C2000 DSP family

val elf_ma_c2000 : Nat_big_num.num

The Texas Instruments TMS320C2000 DSP family

The Texas Instruments TMS320C55x DSP family

val elf_ma_c5500 : Nat_big_num.num

The Texas Instruments TMS320C55x DSP family

STMicroelectronics 64bit VLIW Data Signal Processor

val elf_ma_mmdsp_plus : Nat_big_num.num

STMicroelectronics 64bit VLIW Data Signal Processor

LSI Logic 16-bit DSP Processor

val elf_ma_zsp : Nat_big_num.num

LSI Logic 16-bit DSP Processor

Donald Knuth's educational 64-bit processor

val elf_ma_mmix : Nat_big_num.num

Donald Knuth's educational 64-bit processor

Harvard University machine-independent object files

val elf_ma_huany : Nat_big_num.num

Harvard University machine-independent object files

SiTera Prism

val elf_ma_prism : Nat_big_num.num

SiTera Prism

Atmel AVR 8-bit microcontroller

val elf_ma_avr : Nat_big_num.num

Atmel AVR 8-bit microcontroller

Fujitsu FR30

val elf_ma_fr30 : Nat_big_num.num

Fujitsu FR30

Mitsubishi D10V

val elf_ma_d10v : Nat_big_num.num

Mitsubishi D10V

Mitsubishi D30V

val elf_ma_d30v : Nat_big_num.num

Mitsubishi D30V

NEC v850

val elf_ma_v850 : Nat_big_num.num

NEC v850

Mitsubishi M32R

val elf_ma_m32r : Nat_big_num.num

Mitsubishi M32R

Matsushita MN10300

val elf_ma_mn10300 : Nat_big_num.num

Matsushita MN10300

Matsushita MN10200

val elf_ma_mn10200 : Nat_big_num.num

Matsushita MN10200

picoJava

val elf_ma_pj : Nat_big_num.num

picoJava

OpenRISC 32-bit embedded processor

val elf_ma_openrisc : Nat_big_num.num

OpenRISC 32-bit embedded processor

ARC International ARCompact processor (old spelling/synonym: ELF_MA_ARC_A5)

val elf_ma_arc_compact : Nat_big_num.num

ARC International ARCompact processor (old spelling/synonym: ELF_MA_ARC_A5)

Tensilica Xtensa Architecture

val elf_ma_xtensa : Nat_big_num.num

Tensilica Xtensa Architecture

Alphamosaic VideoCore processor

val elf_ma_videocore : Nat_big_num.num

Alphamosaic VideoCore processor

Thompson Multimedia General Purpose Processor

val elf_ma_tmm_gpp : Nat_big_num.num

Thompson Multimedia General Purpose Processor

National Semiconductor 32000 series

val elf_ma_ns32k : Nat_big_num.num

National Semiconductor 32000 series

Tenor Network TPC processor

val elf_ma_tpc : Nat_big_num.num

Tenor Network TPC processor

Trebia SNP 1000 processor

val elf_ma_snp1k : Nat_big_num.num

Trebia SNP 1000 processor

STMicroelectronics ST200 microcontroller

val elf_ma_st200 : Nat_big_num.num

STMicroelectronics ST200 microcontroller

Ubicom IP2xxx microcontroller family

val elf_ma_ip2k : Nat_big_num.num

Ubicom IP2xxx microcontroller family

MAX Processor

val elf_ma_max : Nat_big_num.num

MAX Processor

National Semiconductor CompactRISC microprocessor

val elf_ma_cr : Nat_big_num.num

National Semiconductor CompactRISC microprocessor

Fujitsu F2MC16

val elf_ma_f2mc16 : Nat_big_num.num

Fujitsu F2MC16

Texas Instruments embedded microcontroller msp430

val elf_ma_msp430 : Nat_big_num.num

Texas Instruments embedded microcontroller msp430

Analog Devices Blackfin (DSP) processor

val elf_ma_blackfin : Nat_big_num.num

Analog Devices Blackfin (DSP) processor

S1C33 Family of Seiko Epson processors

val elf_ma_se_c33 : Nat_big_num.num

S1C33 Family of Seiko Epson processors

Sharp embedded microprocessor

val elf_ma_sep : Nat_big_num.num

Sharp embedded microprocessor

Arca RISC Microprocessor

val elf_ma_arca : Nat_big_num.num

Arca RISC Microprocessor

Microprocessor series from PKU-Unity Ltd. and MPRC of Peking University

val elf_ma_unicore : Nat_big_num.num

Microprocessor 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.num

eXcess: 16/32/64-bit configurable embedded CPU

Icera Semiconductor Inc. Deep Execution Processor

val elf_ma_dxp : Nat_big_num.num

Icera Semiconductor Inc. Deep Execution Processor

Altera Nios II soft-core processor

val elf_ma_altera_nios2 : Nat_big_num.num

Altera Nios II soft-core processor

National Semiconductor CompactRISC CRX microprocessor

val elf_ma_crx : Nat_big_num.num

National Semiconductor CompactRISC CRX microprocessor

Motorola XGATE embedded processor

val elf_ma_xgate : Nat_big_num.num

Motorola XGATE embedded processor

Infineon C16x/XC16x processor

val elf_ma_c166 : Nat_big_num.num

Infineon C16x/XC16x processor

Renesas M16C series microprocessors

val elf_ma_m16c : Nat_big_num.num

Renesas M16C series microprocessors

Microchip Technology dsPIC30F Digital Signal Controller

val elf_ma_dspic30f : Nat_big_num.num

Microchip Technology dsPIC30F Digital Signal Controller

Freescale Communication Engine RISC core

val elf_ma_ce : Nat_big_num.num

Freescale Communication Engine RISC core

Renesas M32C series microprocessors

val elf_ma_m32c : Nat_big_num.num

Renesas M32C series microprocessors

No machine

val elf_ma_none : Nat_big_num.num

No machine

AT&T WE 32100

val elf_ma_m32 : Nat_big_num.num

AT&T WE 32100

SPARC

val elf_ma_sparc : Nat_big_num.num

SPARC

Intel 80386

val elf_ma_386 : Nat_big_num.num

Intel 80386

Motorola 68000

val elf_ma_68k : Nat_big_num.num

Motorola 68000

Motorola 88000

val elf_ma_88k : Nat_big_num.num

Motorola 88000

Intel 80860

val elf_ma_860 : Nat_big_num.num

Intel 80860

MIPS I Architecture

val elf_ma_mips : Nat_big_num.num

MIPS I Architecture

IBM System/370 Processor

val elf_ma_s370 : Nat_big_num.num

IBM System/370 Processor

MIPS RS3000 Little-endian

val elf_ma_mips_rs3_le : Nat_big_num.num

MIPS RS3000 Little-endian

Hewlett-Packard PA-RISC

val elf_ma_parisc : Nat_big_num.num

Hewlett-Packard PA-RISC

Fujitsu VPP500

val elf_ma_vpp500 : Nat_big_num.num

Fujitsu VPP500

Enhanced instruction set SPARC

val elf_ma_sparc32plus : Nat_big_num.num

Enhanced instruction set SPARC

Intel 80960

val elf_ma_960 : Nat_big_num.num

Intel 80960

PowerPC

val elf_ma_ppc : Nat_big_num.num

PowerPC

64-bit PowerPC

val elf_ma_ppc64 : Nat_big_num.num

64-bit PowerPC

IBM System/390 Processor

val elf_ma_s390 : Nat_big_num.num

IBM System/390 Processor

IBM SPU/SPC

val elf_ma_spu : Nat_big_num.num

IBM SPU/SPC

NEC V800

val elf_ma_v800 : Nat_big_num.num

NEC V800

Fujitsu FR20

val elf_ma_fr20 : Nat_big_num.num

Fujitsu FR20

TRW RH-32

val elf_ma_rh32 : Nat_big_num.num

TRW RH-32

Motorola RCE

val elf_ma_rce : Nat_big_num.num

Motorola RCE

ARM 32-bit architecture (AARCH32)

val elf_ma_arm : Nat_big_num.num

ARM 32-bit architecture (AARCH32)

Digital Alpha

val elf_ma_alpha : Nat_big_num.num

Digital Alpha

Hitachi SH

val elf_ma_sh : Nat_big_num.num

Hitachi SH

SPARC Version 9

val elf_ma_sparcv9 : Nat_big_num.num

SPARC Version 9

Siemens TriCore embedded processor

val elf_ma_tricore : Nat_big_num.num

Siemens TriCore embedded processor

Argonaut RISC Core, Argonaut Technologies Inc.

val elf_ma_arc : Nat_big_num.num

Argonaut RISC Core, Argonaut Technologies Inc.

Hitachi H8/300

val elf_ma_h8_300 : Nat_big_num.num

Hitachi H8/300

Hitachi H8/300H

val elf_ma_h8_300h : Nat_big_num.num

Hitachi H8/300H

Hitachi H8S

val elf_ma_h8s : Nat_big_num.num

Hitachi H8S

Hitachi H8/500

val elf_ma_h8_500 : Nat_big_num.num

Hitachi H8/500

Intel IA-64 processor architecture

val elf_ma_ia_64 : Nat_big_num.num

Intel IA-64 processor architecture

Stanford MIPS-X

val elf_ma_mips_x : Nat_big_num.num

Stanford MIPS-X

Motorola ColdFire

val elf_ma_coldfire : Nat_big_num.num

Motorola ColdFire

Motorola M68HC12

val elf_ma_68hc12 : Nat_big_num.num

Motorola M68HC12

Fujitsu MMA Multimedia Accelerator

val elf_ma_mma : Nat_big_num.num

Fujitsu MMA Multimedia Accelerator

Siemens PCP

val elf_ma_pcp : Nat_big_num.num

Siemens PCP

Sony nCPU embedded RISC processor

val elf_ma_ncpu : Nat_big_num.num

Sony nCPU embedded RISC processor

Denso NDR1 microprocessor

val elf_ma_ndr1 : Nat_big_num.num

Denso NDR1 microprocessor

Motorola Star*Core processor

val elf_ma_starcore : Nat_big_num.num

Motorola Star*Core processor

Toyota ME16 processor

val elf_ma_me16 : Nat_big_num.num

Toyota ME16 processor

STMicroelectronics ST100 processor

val elf_ma_st100 : Nat_big_num.num

STMicroelectronics ST100 processor

Advanced Logic Corp. TinyJ embedded processor family

val elf_ma_tinyj : Nat_big_num.num

Advanced Logic Corp. TinyJ embedded processor family

AMD x86-64 architecture

val elf_ma_x86_64 : Nat_big_num.num

AMD x86-64 architecture

Sony DSP Processor

val elf_ma_pdsp : Nat_big_num.num

Sony DSP Processor

Digital Equipment Corp. PDP-10

val elf_ma_pdp10 : Nat_big_num.num

Digital Equipment Corp. PDP-10

Digital Equipment Corp. PDP-11

val elf_ma_pdp11 : Nat_big_num.num

Digital Equipment Corp. PDP-11

Siemens FX66 microcontroller

val elf_ma_fx66 : Nat_big_num.num

Siemens FX66 microcontroller

STMicroelectronics ST9+ 8/16 bit microcontroller

val elf_ma_st9plus : Nat_big_num.num

STMicroelectronics ST9+ 8/16 bit microcontroller

STMicroelectronics ST7 8-bit microcontroller

val elf_ma_st7 : Nat_big_num.num

STMicroelectronics ST7 8-bit microcontroller

Motorola MC68HC16 Microcontroller

val elf_ma_68hc16 : Nat_big_num.num

Motorola MC68HC16 Microcontroller

Motorola MC68HC11 Microcontroller

val elf_ma_68hc11 : Nat_big_num.num

Motorola MC68HC11 Microcontroller

Motorola MC68HC08 Microcontroller

val elf_ma_68hc08 : Nat_big_num.num

Motorola MC68HC08 Microcontroller

Motorola MC68HC05 Microcontroller

val elf_ma_68hc05 : Nat_big_num.num

Motorola MC68HC05 Microcontroller

Silicon Graphics SVx

val elf_ma_svx : Nat_big_num.num

Silicon Graphics SVx

STMicroelectronics ST19 8-bit microcontroller

val elf_ma_st19 : Nat_big_num.num

STMicroelectronics ST19 8-bit microcontroller

Digital VAX

val elf_ma_vax : Nat_big_num.num

Digital VAX

Axis Communications 32-bit embedded processor

val elf_ma_cris : Nat_big_num.num

Axis Communications 32-bit embedded processor

Infineon Technologies 32-bit embedded processor

val elf_ma_javelin : Nat_big_num.num

Infineon Technologies 32-bit embedded processor

Element 14 64-bit DSP Processor

val elf_ma_firepath : Nat_big_num.num

Element 14 64-bit DSP Processor

Reserved by Intel

val elf_ma_intel209 : Nat_big_num.num

Reserved by Intel

Reserved by Intel

val elf_ma_intel208 : Nat_big_num.num

Reserved by Intel

Reserved by Intel

val elf_ma_intel207 : Nat_big_num.num

Reserved by Intel

Reserved by Intel

val elf_ma_intel206 : Nat_big_num.num

Reserved by Intel

Reserved by Intel

val elf_ma_intel205 : Nat_big_num.num

Reserved by Intel

Reserved by Intel

val elf_ma_intel182 : Nat_big_num.num

Reserved by Intel

Reserved by ARM

val elf_ma_arm184 : Nat_big_num.num

Reserved by ARM

Reserved for future use

val elf_ma_reserved6 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved11 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved12 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved13 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved14 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved16 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved24 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved25 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved26 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved27 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved28 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved29 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved30 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved31 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved32 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved33 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved34 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved35 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved121 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved122 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved123 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved124 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved125 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved126 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved127 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved128 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved129 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved130 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved143 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved144 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved145 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved146 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved147 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved148 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved149 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved150 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved151 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved152 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved153 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved154 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved155 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved156 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved157 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved158 : Nat_big_num.num

Reserved for future use

Reserved for future use

val elf_ma_reserved159 : Nat_big_num.num

Reserved for future use

val string_of_elf_machine_architecture : Nat_big_num.num -> string

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.

val elf_ev_none : Nat_big_num.num

Invalid version

Current version

val elf_ev_current : Nat_big_num.num

Current version

val string_of_elf_version_number : Nat_big_num.num -> string

string_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 -> bool

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.

val elf_ii_mag0 : Nat_big_num.num

File identification

File identification

val elf_ii_mag1 : Nat_big_num.num

File identification

File identification

val elf_ii_mag2 : Nat_big_num.num

File identification

File identification

val elf_ii_mag3 : Nat_big_num.num

File identification

File class

val elf_ii_class : Nat_big_num.num

File class

Data encoding

val elf_ii_data : Nat_big_num.num

Data encoding

File version

val elf_ii_version : Nat_big_num.num

File version

Operating system/ABI identification

val elf_ii_osabi : Nat_big_num.num

Operating system/ABI identification

ABI version

val elf_ii_abiversion : Nat_big_num.num

ABI version

Start of padding bytes

val elf_ii_pad : Nat_big_num.num

Start of padding bytes

Size of e*_ident

val elf_ii_nident : Nat_big_num.num

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.

val elf_mn_mag0 : Uint32_wrapper.uint32

Position: e*_identelf_ii_mag0, 0x7f magic number

Position: e*_identelf_ii_mag1, 'E' format identifier

val elf_mn_mag1 : Uint32_wrapper.uint32

Position: e*_identelf_ii_mag1, 'E' format identifier

Position: e*_identelf_ii_mag2, 'L' format identifier

val elf_mn_mag2 : Uint32_wrapper.uint32

Position: e*_identelf_ii_mag2, 'L' format identifier

Position: e*_identelf_ii_mag3, 'F' format identifier

val elf_mn_mag3 : Uint32_wrapper.uint32

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.

val elf_class_none : Nat_big_num.num

Invalid class

32 bit objects

val elf_class_32 : Nat_big_num.num

32 bit objects

64 bit objects

val elf_class_64 : Nat_big_num.num

64 bit objects

val string_of_elf_file_class : Nat_big_num.num -> string

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.

val elf_data_none : Nat_big_num.num

Invalid data encoding

Two's complement values, least significant byte occupying lowest address

val elf_data_2lsb : Nat_big_num.num

Two'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.num

Two's complement values, most significant byte occupying lowest address

val string_of_elf_data_encoding : Nat_big_num.num -> string

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.

val elf_osabi_none : Nat_big_num.num

No extensions or unspecified

Hewlett-Packard HP-UX

val elf_osabi_hpux : Nat_big_num.num

Hewlett-Packard HP-UX

NetBSD

val elf_osabi_netbsd : Nat_big_num.num

NetBSD

GNU

val elf_osabi_gnu : Nat_big_num.num

GNU

Linux, historical alias for GNU

val elf_osabi_linux : Nat_big_num.num

Linux, historical alias for GNU

Sun Solaris

val elf_osabi_solaris : Nat_big_num.num

Sun Solaris

AIX

val elf_osabi_aix : Nat_big_num.num

AIX

IRIX

val elf_osabi_irix : Nat_big_num.num

IRIX

FreeBSD

val elf_osabi_freebsd : Nat_big_num.num

FreeBSD

Compaq Tru64 Unix

val elf_osabi_tru64 : Nat_big_num.num

Compaq Tru64 Unix

Novell Modesto

val elf_osabi_modesto : Nat_big_num.num

Novell Modesto

OpenBSD

val elf_osabi_openbsd : Nat_big_num.num

OpenBSD

OpenVMS

val elf_osabi_openvms : Nat_big_num.num

OpenVMS

Hewlett-Packard Non-stop Kernel

val elf_osabi_nsk : Nat_big_num.num

Hewlett-Packard Non-stop Kernel

Amiga Research OS

val elf_osabi_aros : Nat_big_num.num

Amiga Research OS

FenixOS highly-scalable multi-core OS

val elf_osabi_fenixos : Nat_big_num.num

FenixOS highly-scalable multi-core OS

Nuxi CloudABI

val elf_osabi_cloudabi : Nat_big_num.num

Nuxi CloudABI

Stratus technologies OpenVOS

val elf_osabi_openvos : Nat_big_num.num

Stratus technologies OpenVOS

val is_valid_architecture_defined_osabi_version : Nat_big_num.num -> bool

Checks 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 -> string

string_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.num

ei_nident is the fixed length of the identification field in the * elf32_ehdr type.

type elf32_header = {
  1. elf32_ident : Uint32_wrapper.uint32 list;
    (*

    Identification field

    *)
  2. elf32_type : Uint32_wrapper.uint32;
    (*

    The object file type

    *)
  3. elf32_machine : Uint32_wrapper.uint32;
    (*

    Required machine architecture

    *)
  4. elf32_version : Uint32_wrapper.uint32;
    (*

    Object file version

    *)
  5. elf32_entry : Uint32_wrapper.uint32;
    (*

    Virtual address for transfer of control

    *)
  6. elf32_phoff : Uint32_wrapper.uint32;
    (*

    Program header table offset in bytes

    *)
  7. elf32_shoff : Uint32_wrapper.uint32;
    (*

    Section header table offset in bytes

    *)
  8. elf32_flags : Uint32_wrapper.uint32;
    (*

    Processor-specific flags

    *)
  9. elf32_ehsize : Uint32_wrapper.uint32;
    (*

    ELF header size in bytes

    *)
  10. elf32_phentsize : Uint32_wrapper.uint32;
    (*

    Program header table entry size in bytes

    *)
  11. elf32_phnum : Uint32_wrapper.uint32;
    (*

    Number of entries in program header table

    *)
  12. elf32_shentsize : Uint32_wrapper.uint32;
    (*

    Section header table entry size in bytes

    *)
  13. elf32_shnum : Uint32_wrapper.uint32;
    (*

    Number of entries in section header table

    *)
  14. 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 = {
  1. elf64_ident : Uint32_wrapper.uint32 list;
    (*

    Identification field

    *)
  2. elf64_type : Uint32_wrapper.uint32;
    (*

    The object file type

    *)
  3. elf64_machine : Uint32_wrapper.uint32;
    (*

    Required machine architecture

    *)
  4. elf64_version : Uint32_wrapper.uint32;
    (*

    Object file version

    *)
  5. elf64_entry : Uint64_wrapper.uint64;
    (*

    Virtual address for transfer of control

    *)
  6. elf64_phoff : Uint64_wrapper.uint64;
    (*

    Program header table offset in bytes

    *)
  7. elf64_shoff : Uint64_wrapper.uint64;
    (*

    Section header table offset in bytes

    *)
  8. elf64_flags : Uint32_wrapper.uint32;
    (*

    Processor-specific flags

    *)
  9. elf64_ehsize : Uint32_wrapper.uint32;
    (*

    ELF header size in bytes

    *)
  10. elf64_phentsize : Uint32_wrapper.uint32;
    (*

    Program header table entry size in bytes

    *)
  11. elf64_phnum : Uint32_wrapper.uint32;
    (*

    Number of entries in program header table

    *)
  12. elf64_shentsize : Uint32_wrapper.uint32;
    (*

    Section header table entry size in bytes

    *)
  13. elf64_shnum : Uint32_wrapper.uint32;
    (*

    Number of entries in section header table

    *)
  14. 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 -> bool

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.

val is_valid_elf64_header : elf64_header -> bool

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.

val elf32_header_compare : elf32_header -> elf32_header -> int

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_class
val elf64_header_compare : elf64_header -> elf64_header -> int

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.

val instance_Basic_classes_Ord_Elf_header_elf64_header_dict : elf64_header Lem_basic_classes.ord_class
val is_elf32_executable_file : elf32_header -> bool

is_elf32_executable_file hdr checks whether the header hdr states if the * ELF file is of executable type.

val is_elf64_executable_file : 'a -> bool

is_elf64_executable_file hdr checks whether the header hdr states if the * ELF file is of executable type.

val is_elf32_shared_object_file : elf32_header -> bool

is_elf32_shared_object_file hdr checks whether the header hdr states if the * ELF file is of shared object type.

val is_elf64_shared_object_file : elf64_header -> bool

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 -> bool

is_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 -> bool

is_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 -> bool

is_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 -> bool

is_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.num

get_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.num

get_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.num

get_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.num

get_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.num

get_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.num

get_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.num

get_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.num

get_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.num

get_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.num

get_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 -> bool

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.

val is_valid_elf64_version_numer : elf64_header -> bool

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.

val get_elf32_abi_version : elf32_header -> Nat_big_num.num

get_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.num

get_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.endianness

deduce_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.endianness

get_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.endianness

get_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 -> bool

has_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 -> bool

has_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 -> bool

has_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 -> bool

has_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 -> bool

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.

val is_elf64_header_section_size_in_section_header_table : elf64_header -> bool

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.

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 -> string

string_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 -> string

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.

val string_of_elf32_header_default : elf32_header -> string
val string_of_elf64_header_default : elf64_header -> string
val instance_Show_Show_Elf_header_elf32_header_dict : elf32_header Show.show_class
val instance_Show_Show_Elf_header_elf64_header_dict : elf64_header Show.show_class

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.

val bytes_of_elf32_header : elf32_header -> Byte_sequence_wrapper.byte_sequence

bytes_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_sequence

bytes_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 -> bool
val is_magic_number_correct : Uint32_wrapper.uint32 list -> bool

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.

val is_elf32_header_class_correct : elf32_header -> bool

is_elf32_header_class_correct hdr checks whether the declared file class * is correct.

val is_elf64_header_class_correct : elf64_header -> bool

is_elf64_header_class_correct hdr checks whether the declared file class * is correct.

val is_elf32_header_version_correct : elf32_header -> bool

is_elf32_header_version_correct hdr checks whether the declared file version * is correct.

val is_elf64_header_version_correct : elf64_header -> bool

is_elf64_header_version_correct hdr checks whether the declared file version * is correct.

val is_elf32_header_valid : elf32_header -> bool

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).

val get_elf32_header_program_table_size : elf32_header -> Nat_big_num.num

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.

val get_elf64_header_program_table_size : elf64_header -> Nat_big_num.num

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.

val is_elf32_header_section_table_present : elf32_header -> bool

is_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 -> bool

is_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.num

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.

val get_elf64_header_section_table_size : elf64_header -> Nat_big_num.num

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.

OCaml

Innovation. Community. Security.