remove old elf sources

1 files changed, 0 insertions, 825 deletions

diff --git a/src/elf_model/elf_header.lem b/src/elf_model/elf_header.lem
deleted file mode 100644
index 3fbe0af9..00000000
--- a/src/elf_model/elf_header.lem
+++ /dev/null
@@ -1,825 +0,0 @@
-open import Basic_classes
-open import Bool
-open import Function
-open import List
-open import Maybe
-open import Num
-open import String
-
-open import Default_printing
-open import Endianness
-
-open import Elf_types
-
-open import Bitstring
-open import Error
-open import Missing_pervasives
-open import Show
-
-(** ELF object file types.  Enumerates the ELF object file types specified in the
- *  System V ABI.  Values between [elf_ft_lo_os] and [elf_ft_hi_os] inclusive are
- *  reserved for operating system specific values typically defined in an
- *  addendum to the System V ABI for that operating system.  Values between
- *  [elf_ft_lo_proc] and [elf_ft_hi_proc] inclusive are processor specific and
- *  are typically defined in an addendum to the System V ABI for that processor
- *  series.
- *)
-
-(** No file type *)
-let elf_ft_none : nat = 0
-(** Relocatable file *)
-let elf_ft_rel : nat = 1
-(** Executable file *)
-let elf_ft_exec : nat = 2
-(** Shared object file *)
-let elf_ft_dyn : nat = 3
-(** Core file *)
-let elf_ft_core : nat = 4
-(** Operating-system specific *)
-let elf_ft_lo_os : nat = 65024 (* 0xfe00 *)
-(** Operating-system specific *)
-let elf_ft_hi_os : nat = 65279 (* 0xfeff *)
-(** Processor specific *)
-let elf_ft_lo_proc : nat = 65280 (* 0xff00 *)
-(** Processor specific *)
-let elf_ft_hi_proc : nat = 65535 (* 0xffff *)
-
-(** [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 string_of_elf_file_type : (nat -> string) -> (nat -> string) -> nat -> string
-let string_of_elf_file_type os_specific proc_specific m =
-	if m = elf_ft_none then
-		"No file type"
-	else if m = elf_ft_rel then
-		"Relocatable file type"
-	else if m = elf_ft_exec then
-		"Executable file type"
-	else if m = elf_ft_dyn then
-		"Shared object file type"
-	else if m = elf_ft_core then
-		"Core file type"
-	else if m >= elf_ft_lo_os && m <= elf_ft_hi_os then
-		os_specific m
-	else if m >= elf_ft_lo_proc && m <= elf_ft_hi_proc then
-		proc_specific m
-	else
-		"Invalid file type"
-
-(** [is_operating_specific_file_type_value] checks whether a numeric value is
-  * reserved by the ABI for operating system-specific purposes.
-  *)
-val is_operating_system_specific_object_file_type_value : nat -> bool
-let is_operating_system_specific_object_file_type_value v =
-  v >= 65024 && v <= 65279
-
-(** [is_processor_specific_file_type_value] checks whether a numeric value is
-  * reserved by the ABI for processor-specific purposes.
-  *)
-val is_processor_specific_object_file_type_value : nat -> bool
-let is_processor_specific_object_file_type_value v =
-  v >= 65280 && v <= 65535
-
-(** ELF machine architectures (TODO: complete the conversion of the enumeration.) *)
-
-(** Intel 386 *)
-let elf_ma_386 : nat = 3
-(** IBM PowerPC *)
-let elf_ma_ppc : nat = 20
-(** IBM PowerPC 64 *)
-let elf_ma_ppc64 : nat = 21
-(** AMD x86-64 *)
-let elf_ma_x86_64 : nat = 62
-
-(** [string_of_elf_machine_architecture m] produces a string representation of
-  * the numeric encoding [m] of the ELF machine architecture.
-  *)
-val string_of_elf_machine_architecture : nat -> string
-let string_of_elf_machine_architecture m =
-	if m = elf_ma_386 then
-		"Intel 386 architecture"
-  else if m = elf_ma_ppc then
-    "IBM PowerPC"
-  else if m = elf_ma_ppc64 then
-    "IBM PowerPC 64"
-  else if m = elf_ma_x86_64 then
-    "AMD x86-64"
-	else
-		"Other architecture"
-
-(* XXX: convert these into top-level definitions later...
-(** [elf_machine_architecture] enumerates all the supported machine architectures
-  * in the System V ABI.
-  *)
-type elf_machine_architecture
-  = ELF_MA_Norc          (* Nanoradio optimised RISC *)
-  | ELF_MA_Cool          (* iCelero CoolEngine *)
-  | ELF_MA_Coge          (* Cognitive Smart Memory Processor *)
-  | ELF_MA_CDP           (* Paneve CDP architecture family *)
-  | ELF_MA_KVARC         (* KM211 KVARC processor *)
-  | ELF_MA_KMX8          (* KM211 KMX8 8-bit processor *)
-  | ELF_MA_KMX16         (* KM211 KMX16 16-bit processor *)
-  | ELF_MA_KMX32         (* KM211 KMX32 32-bit processor *)
-  | ELF_MA_KM32          (* KM211 KM32 32-bit processor *)
-  | ELF_MA_MCHP_PIC      (* Microchip 8-bit PIC(r) family *)
-  | ELF_MA_XCORE         (* XMOS xCORE processor family *)
-  | ELF_MA_BA2           (* Beyond BA2 CPU architecture *)
-  | ELF_MA_BA1           (* Beyond BA1 CPU architecture *)  
-  | ELF_MA_5600EX        (* Freescale 56800EX Digital Signal Controller (DSC) *)
-  | ELF_MA_78KOR         (* 199 Renesas 78KOR family *)
-  | ELF_MA_VideoCore5    (* Broadcom VideoCore V processor *)
-  | ELF_MA_RL78          (* Renesas RL78 family *)
-  | ELF_MA_Open8         (* Open8 8-bit RISC soft processing core *)
-  | ELF_MA_ARC_Compact2  (* Synopsys ARCompact V2 *)
-  | ELF_MA_CoreA_2nd     (* KIPO_KAIST Core-A 2nd generation processor family *)
-  | ELF_MA_CoreA_1st     (* KIPO_KAIST Core-A 1st generation processor family *)
-  | ELF_MA_CloudShield   (* CloudShield architecture family *)
-  | ELF_MA_SLE9X         (* Infineon Technologies SLE9X core *)
-  | ELF_MA_L10M          (* Intel L10M *)
-  | ELF_MA_K10M          (* Intel K10M *)
-  | ELF_MA_AArch64       (* ARM 64-bit architecture (AARCH64) *)
-  | ELF_MA_AVR32         (* Atmel Corporation 32-bit microprocessor family *)
-  | ELF_MA_STM8          (* STMicroelectronics STM8 8-bit microcontroller *)
-  | ELF_MA_TILE64        (* Tilera TILE64 multicore architecture family *)
-  | ELF_MA_TILEPro       (* Tilera TILEPro multicore architecture family *)
-  | ELF_MA_MicroBlaze    (* Xilinix MicroBlaze 32-bit RISC soft processor core *)
-  | ELF_MA_CUDA          (* NVIDIA CUDA architecture *)
-  | ELF_MA_TILEGx        (* Tilera TILE-Gx multicore architecture family *)
-  | ELF_MA_Cypress       (* Cypress M8C microprocessor *)
-  | ELF_MA_R32C          (* Renesas R32C series microprocessors *)
-  | ELF_MA_TriMedia      (* NXP Semiconductors TriMedia architecture family *)
-  | ELF_MA_QDSP6         (* QUALCOMM DSP6 processor *)
-  | ELF_MA_8051          (* Intel 8051 and variants *)
-  | ELF_MA_STXP7X        (* STMicroelectronics STxP7x family of configurable and extensible RISC processors *)
-  | ELF_MA_NDS32         (* Andes Technology compact code size embedded RISC processor family *)
-  | ELF_MA_eCOG1X        (* Cyan Technology eCOG1X family *)
-  | ELF_MA_MAXQ30        (* Dallas Semiconductor MAXQ30 Core Micro-controllers *)
-  | ELF_MA_XIMO16        (* New Japan Radio (NJR) 16-bit DSP Processor *)
-  | ELF_MA_MANIK         (* M2000 Reconfigurable RISC Microprocessor *)
-  | ELF_MA_CrayNV2       (* Cray Inc. NV2 vector architecture *)
-  | ELF_MA_RX            (* Renesas RX family *)
-  | ELF_MA_METAG         (* Imagination Technologies META processor architecture *)
-  | ELF_MA_MCST_Elbrus   (* MCST Elbrus general purpose hardware architecture *)
-  | ELF_MA_eCOG16        (* Cyan Technology eCOG16 family *)
-  | ELF_MA_CR16          (* National Semiconductor CompactRISC CR16 16-bit microprocessor *)
-  | ELF_MA_ETPU          (* Freescale Extended Time Processing Unit *)
-  | ELF_MA_TSK3000       (* Altium TSK3000 core *)
-  | ELF_MA_RS08          (* Freescale RS08 embedded processor *)
-  | ELF_MA_SHARC         (* Analog Devices SHARC family of 32-bit DSP processors *)
-  | ELF_MA_eCOG2         (* Cyan Technology eCOG2 microprocessor *)
-  | ELF_MA_Score7        (* Sunplus S+core7 RISC processor *)
-  | ELF_MA_DSP24         (* New Japan Radio (NJR) 24-bit DSP Processor *)
-  | ELF_MA_VideoCore3    (* Broadcom VideoCore III processor *)
-  | ELF_MA_LatticeMICO32 (* RISC processor for Lattice FPGA architecture *)
-  | ELF_MA_C17           (* Seiko Epson C17 family *)
-  | ELF_MA_C6000         (* The Texas Instruments TMS320C6000 DSP family *)
-  | ELF_MA_C2000         (* The Texas Instruments TMS320C2000 DSP family *)
-  | ELF_MA_C5500         (* The Texas Instruments TMS320C55x DSP family *)
-  | ELF_MA_MMDSP_PLUS    (* STMicroelectronics 64bit VLIW Data Signal Processor *)
-  | ELF_MA_ZSP           (* LSI Logic 16-bit DSP Processor *)
-  | ELF_MA_MMIX          (* Donald Knuth's educational 64-bit processor *)
-  | ELF_MA_HUANY         (* Harvard University machine-independent object files *)
-  | ELF_MA_Prism         (* SiTera Prism *)
-  | ELF_MA_AVR           (* Atmel AVR 8-bit microcontroller *)
-  | ELF_MA_FR30          (* Fujitsu FR30 *)
-  | ELF_MA_D10V          (* Mitsubishi D10V *)
-  | ELF_MA_D30V          (* Mitsubishi D30V *)
-  | ELF_MA_v850          (* NEC v850 *)
-  | ELF_MA_M32R          (* Mitsubishi M32R *)
-  | ELF_MA_MN10300       (* Matsushita MN10300 *)
-  | ELF_MA_MN10200       (* Matsushita MN10200 *)
-  | ELF_MA_pJ            (* picoJava *)
-  | ELF_MA_OpenRISC      (* OpenRISC 32-bit embedded processor *)
-  | ELF_MA_ARC_Compact   (* ARC International ARCompact processor (old spelling/synonym: ELF_MA_ARC_A5) *)
-  | ELF_MA_Xtensa        (* Tensilica Xtensa Architecture *)
-  | ELF_MA_VideoCore     (* Alphamosaic VideoCore processor *)
-  | ELF_MA_TMM_GPP       (* Thompson Multimedia General Purpose Processor *)
-  | ELF_MA_NS32K         (* National Semiconductor 32000 series *)
-  | ELF_MA_TPC           (* Tenor Network TPC processor *)
-  | ELF_MA_SNP1K         (* Trebia SNP 1000 processor *)
-  | ELF_MA_ST200         (* STMicroelectronics ST200 microcontroller *)
-  | ELF_MA_IP2K          (* Ubicom IP2xxx microcontroller family *)
-  | ELF_MA_MAX           (* MAX Processor *)
-  | ELF_MA_CR            (* National Semiconductor CompactRISC microprocessor *)
-  | ELF_MA_F2MC16        (* Fujitsu F2MC16 *)
-  | ELF_MA_MSP430        (* Texas Instruments embedded microcontroller msp430 *)
-  | ELF_MA_Blackfin      (* Analog Devices Blackfin (DSP) processor *)
-  | ELF_MA_SE_C33        (* S1C33 Family of Seiko Epson processors *)
-  | ELF_MA_SEP           (* Sharp embedded microprocessor *)
-  | ELF_MA_Arca          (* Arca RISC Microprocessor *)
-  | ELF_MA_Unicore       (* Microprocessor series from PKU-Unity Ltd. and MPRC of Peking University *)
-  | ELF_MA_eXcess        (* eXcess: 16/32/64-bit configurable embedded CPU *)
-  | ELF_MA_DXP           (* Icera Semiconductor Inc. Deep Execution Processor *)
-  | ELF_MA_Altera_Nios2  (* Altera Nios II soft-core processor *)
-  | ELF_MA_CRX           (* National Semiconductor CompactRISC CRX microprocessor *)
-  | ELF_MA_XGATE         (* Motorola XGATE embedded processor *)
-  | ELF_MA_C166          (* Infineon C16x/XC16x processor *)
-  | ELF_MA_M16C          (* Renesas M16C series microprocessors *)
-  | ELF_MA_dsPIC30F      (* Microchip Technology dsPIC30F Digital Signal Controller *)
-  | ELF_MA_CE            (* Freescale Communication Engine RISC core *)
-  | ELF_MA_M32C          (* Renesas M32C series microprocessors *)
-  | ELF_MA_None          (* No machine *)
-  | ELF_MA_M32           (* AT&T WE 32100 *)
-  | ELF_MA_SPARC         (* SPARC *)
-  | ELF_MA_386           (* Intel 80386 *)
-  | ELF_MA_68K           (* Motorola 68000 *)
-  | ELF_MA_88K           (* Motorola 88000 *)
-  | ELF_MA_860           (* Intel 80860 *)
-  | ELF_MA_MIPS          (* MIPS I Architecture *)
-  | ELF_MA_S370          (* IBM System/370 Processor *)
-  | ELF_MA_MIPS_RS3_LE   (* MIPS RS3000 Little-endian *)
-  | ELF_MA_PARISC        (* Hewlett-Packard PA-RISC *)
-  | ELF_MA_VPP500        (* Fujitsu VPP500 *)
-  | ELF_MA_SPARC32PLUS   (* Enhanced instruction set SPARC *)
-  | ELF_MA_960           (* Intel 80960 *)
-  | ELF_MA_PPC           (* PowerPC *)
-  | ELF_MA_PPC64         (* 64-bit PowerPC *)
-  | ELF_MA_S390          (* IBM System/390 Processor *)
-  | ELF_MA_SPU           (* IBM SPU/SPC *)
-  | ELF_MA_V800          (* NEC V800 *)
-  | ELF_MA_FR20          (* Fujitsu FR20 *)
-  | ELF_MA_RH32          (* TRW RH-32 *)
-  | ELF_MA_RCE           (* Motorola RCE *)
-  | ELF_MA_ARM           (* ARM 32-bit architecture (AARCH32) *)
-  | ELF_MA_Alpha         (* Digital Alpha *)
-  | ELF_MA_SH            (* Hitachi SH *)
-  | ELF_MA_SPARCv9       (* SPARC Version 9 *)
-  | ELF_MA_TriCore       (* Siemens TriCore embedded processor *)
-  | ELF_MA_ARC           (* Argonaut RISC Core, Argonaut Technologies Inc. *)
-  | ELF_MA_H8_300        (* Hitachi H8/300 *)
-  | ELF_MA_H8_300H       (* Hitachi H8/300H *)
-  | ELF_MA_H8S           (* Hitachi H8S *)
-  | ELF_MA_H8_500        (* Hitachi H8/500 *)
-  | ELF_MA_IA_64         (* Intel IA-64 processor architecture *)
-  | ELF_MA_MIPS_X        (* Stanford MIPS-X *)
-  | ELF_MA_ColdFire      (* Motorola ColdFire *)
-  | ELF_MA_68HC12        (* Motorola M68HC12 *)
-  | ELF_MA_MMA           (* Fujitsu MMA Multimedia Accelerator *)
-  | ELF_MA_PCP           (* Siemens PCP *)
-  | ELF_MA_nCPU          (* Sony nCPU embedded RISC processor *)
-  | ELF_MA_NDR1          (* Denso NDR1 microprocessor *)
-  | ELF_MA_StarCore      (* Motorola Star*Core processor *)
-  | ELF_MA_ME16          (* Toyota ME16 processor *)
-  | ELF_MA_ST100         (* STMicroelectronics ST100 processor *)
-  | ELF_MA_TinyJ         (* Advanced Logic Corp. TinyJ embedded processor family *)
-  | ELF_MA_X86_64        (* AMD x86-64 architecture *)
-  | ELF_MA_PDSP          (* Sony DSP Processor *)
-  | ELF_MA_PDP10         (* Digital Equipment Corp. PDP-10 *)
-  | ELF_MA_PDP11         (* Digital Equipment Corp. PDP-11 *)
-  | ELF_MA_FX66          (* Siemens FX66 microcontroller *)
-  | ELF_MA_ST9Plus       (* STMicroelectronics ST9+ 8/16 bit microcontroller *)
-  | ELF_MA_ST7           (* STMicroelectronics ST7 8-bit microcontroller *)
-  | ELF_MA_68HC16        (* Motorola MC68HC16 Microcontroller *)
-  | ELF_MA_68HC11        (* Motorola MC68HC11 Microcontroller *)
-  | ELF_MA_68HC08        (* Motorola MC68HC08 Microcontroller *)
-  | ELF_MA_68HC05        (* Motorola MC68HC05 Microcontroller *)
-  | ELF_MA_SVx           (* Silicon Graphics SVx *)
-  | ELF_MA_ST19          (* STMicroelectronics ST19 8-bit microcontroller *)
-  | ELF_MA_VAX           (* Digital VAX *)
-  | ELF_MA_CRIS          (* Axis Communications 32-bit embedded processor *)
-  | ELF_MA_Javelin       (* Infineon Technologies 32-bit embedded processor *)
-  | ELF_MA_Firepath      (* Element 14 64-bit DSP Processor *)
-  | ELF_MA_Intel209      (* Reserved by Intel *)
-  | ELF_MA_Intel208      (* Reserved by Intel *)
-  | ELF_MA_Intel207      (* Reserved by Intel *)
-  | ELF_MA_Intel206      (* Reserved by Intel *)
-  | ELF_MA_Intel205      (* Reserved by Intel *)
-  | ELF_MA_Intel182      (* Reserved by Intel *)
-  | ELF_MA_ARM184        (* Reserved by ARM *)
-  | ELF_MA_Reserved6     (* Reserved for future use *)
-  | ELF_MA_Reserved11    (* Reserved for future use *)
-  | ELF_MA_Reserved12    (* Reserved for future use *)
-  | ELF_MA_Reserved13    (* Reserved for future use *)
-  | ELF_MA_Reserved14    (* Reserved for future use *)
-  | ELF_MA_Reserved16    (* Reserved for future use *)
-  | ELF_MA_Reserved24    (* Reserved for future use *)
-  | ELF_MA_Reserved25    (* Reserved for future use *)
-  | ELF_MA_Reserved26    (* Reserved for future use *)
-  | ELF_MA_Reserved27    (* Reserved for future use *)
-  | ELF_MA_Reserved28    (* Reserved for future use *)
-  | ELF_MA_Reserved29    (* Reserved for future use *)
-  | ELF_MA_Reserved30    (* Reserved for future use *)
-  | ELF_MA_Reserved31    (* Reserved for future use *)
-  | ELF_MA_Reserved32    (* Reserved for future use *)
-  | ELF_MA_Reserved33    (* Reserved for future use *)
-  | ELF_MA_Reserved34    (* Reserved for future use *)
-  | ELF_MA_Reserved35    (* Reserved for future use *)
-  | ELF_MA_Reserved121   (* Reserved for future use *)
-  | ELF_MA_Reserved122   (* Reserved for future use *)
-  | ELF_MA_Reserved123   (* Reserved for future use *)
-  | ELF_MA_Reserved124   (* Reserved for future use *)
-  | ELF_MA_Reserved125   (* Reserved for future use *)
-  | ELF_MA_Reserved126   (* Reserved for future use *)
-  | ELF_MA_Reserved127   (* Reserved for future use *)
-  | ELF_MA_Reserved128   (* Reserved for future use *)
-  | ELF_MA_Reserved129   (* Reserved for future use *)
-  | ELF_MA_Reserved130   (* Reserved for future use *)
-  | ELF_MA_Reserved143   (* Reserved for future use *)
-  | ELF_MA_Reserved144   (* Reserved for future use *)
-  | ELF_MA_Reserved145   (* Reserved for future use *)
-  | ELF_MA_Reserved146   (* Reserved for future use *)
-  | ELF_MA_Reserved147   (* Reserved for future use *)
-  | ELF_MA_Reserved148   (* Reserved for future use *)
-  | ELF_MA_Reserved149   (* Reserved for future use *)
-  | ELF_MA_Reserved150   (* Reserved for future use *)
-  | ELF_MA_Reserved151   (* Reserved for future use *)
-  | ELF_MA_Reserved152   (* Reserved for future use *)
-  | ELF_MA_Reserved153   (* Reserved for future use *)
-  | ELF_MA_Reserved154   (* Reserved for future use *)
-  | ELF_MA_Reserved155   (* Reserved for future use *)
-  | ELF_MA_Reserved156   (* Reserved for future use *)
-  | ELF_MA_Reserved157   (* Reserved for future use *)
-  | ELF_MA_Reserved158   (* Reserved for future use *)
-  | ELF_MA_Reserved159   (* Reserved for future use *)
-  | ELF_MA_ReservedExt of nat (* Reserved for future use *)
-*)
-
-(** ELF version numbers.  Denotes the ELF version number of an ELF file.  Current is
-  * defined to have a value of 1 with the present specification.  Extensions
-  * may create versions of ELF with higher version numbers.
-  *)
-
-(** Invalid version *)
-let elf_ev_none : nat = 0
-(** Current version *)
-let elf_ev_current : nat = 1
-
-(** [string_of_elf_version_number m] produces a string representation of the
-  * numeric encoding [m] of the ELF version number.
-  *)
-val string_of_elf_version_number : nat -> string
-let string_of_elf_version_number m =
-	if m = elf_ev_none then
-		"Invalid ELF version"
-	else if m = elf_ev_current then
-		"Current ELF version"
-	else
-		"Extended ELF version"
-
-(** Check that an extended version number is correct (i.e. greater than 1). *)
-let is_valid_extended_version_number (n : nat) = n > 1
-
-(** Identification indices.  The initial bytes of an ELF header (and an object
-  * file) correspond to the e_ident member.
-  *)
-
-(** File identification *)
-let elf_ii_mag0 : nat = 0
-(** File identification *)
-let elf_ii_mag1 : nat = 1
-(** File identification *)
-let elf_ii_mag2 : nat = 2
-(** File identification *)
-let elf_ii_mag3 : nat = 3
-(** File class *)
-let elf_ii_class : nat = 4
-(** Data encoding *)
-let elf_ii_data : nat = 5
-(** File version *)
-let elf_ii_version : nat = 6
-(** Operating system/ABI identification *)
-let elf_ii_osabi : nat = 7
-(** ABI version *)
-let elf_ii_abiversion : nat = 8
-(** Start of padding bytes *)
-let elf_ii_pad : nat = 9
-(** Size of e*_ident[] *)
-let elf_ii_nident : nat = 16
-
-(** Magic number indices.  A file's first 4 bytes hold a ``magic number,''
-  * identifying the file as an ELF object file.
-  *)
-
-(** Position: e*_ident[elf_ii_mag0], 0x7f magic number *)
-let elf_mn_mag0 : nat = 127
-(** Position: e*_ident[elf_ii_mag1], 'E' format identifier *)
-let elf_mn_mag1 : nat = 69
-(** Position: e*_ident[elf_ii_mag2], 'L' format identifier *)
-let elf_mn_mag2 : nat = 76
-(** Position: e*_ident[elf_ii_mag3], 'F' format identifier *)
-let elf_mn_mag3 : nat = 70
-
-(** ELf file classes.  The file format is designed to be portable among machines
-  * of various sizes, without imposing the sizes of the largest machine on the
-  * smallest. The class of the file defines the basic types used by the data
-  * structures of the object file container itself.
-  *)
-
-(** Invalid class *)
-let elf_class_none : nat = 0
-(** 32 bit objects *)
-let elf_class_32 : nat = 1
-(** 64 bit objects *)
-let elf_class_64 : nat = 2
-
-(** [string_of_elf_file_class m] produces a string representation of the numeric
-  * encoding [m] of the ELF file class.
-  *)
-val string_of_elf_file_class : nat -> string
-let string_of_elf_file_class m =
-	if m = elf_class_none then
-		"Invalid ELF file class"
-	else if m = elf_class_32 then
-		"32 bit ELF object"
-	else if m = elf_class_64 then
-		"64 bit ELF object"
-	else
-		"Invalid ELF file class"
-
-(** ELF data encodings.  Byte e_ident[elf_ei_data] specifies the encoding of both the
-  * data structures used by object file container and data contained in object
-  * file sections.
-  *)
-
-(** Invalid data encoding *)
-let elf_data_none : nat = 0
-(** Two's complement values, least significant byte occupying lowest address *)
-let elf_data_2lsb : nat = 1
-(** Two's complement values, most significant byte occupying lowest address *)
-let elf_data_2msb : nat = 2
-
-(** [string_of_elf_data_encoding m] produces a string representation of the
-  * numeric encoding [m] of the ELF data encoding.
-  *)
-val string_of_elf_data_encoding : nat -> string
-let string_of_elf_data_encoding m =
-	if m = elf_data_none then
-		"Invalid data encoding"
-	else if m = elf_data_2lsb then
-		"Two's complement values, LSB at lowest address"
-	else if m = elf_data_2msb then
-		"Two's complement values, MSB at lowest address"
-	else
-		"Invalid data encoding"
-
-(** OS and ABI versions.  Byte e_ident[elf_ei_osabi] identifies the OS- or
-  * ABI-specific ELF extensions used by this file. Some fields in other ELF
-  * structures have flags and values that have operating system and/or ABI
-  * specific meanings; the interpretation of those fields is determined by the
-  * value of this byte.
-  *)
-
-(** No extensions or unspecified *)
-let elf_osabi_none : nat = 0
-(** Hewlett-Packard HP-UX *)
-let elf_osabi_hpux : nat = 1
-(** NetBSD *)
-let elf_osabi_netbsd : nat = 2
-(** GNU *)
-let elf_osabi_gnu : nat = 3
-(** Linux, historical alias for GNU *)
-let elf_osabi_linux : nat = 3
-(** Sun Solaris *)
-let elf_osabi_solaris : nat = 6
-(** AIX *)
-let elf_osabi_aix : nat = 7
-(** IRIX *)
-let elf_osabi_irix : nat = 8
-(** FreeBSD *)
-let elf_osabi_freebsd : nat = 9
-(** Compaq Tru64 Unix *)
-let elf_osabi_tru64 : nat = 10
-(** Novell Modesto *)
-let elf_osabi_modesto : nat = 11
-(** OpenBSD *)
-let elf_osabi_openbsd : nat = 12
-(** OpenVMS *)
-let elf_osabi_openvms : nat = 13
-(** Hewlett-Packard Non-stop Kernel *)
-let elf_osabi_nsk : nat = 14
-(** Amiga Research OS *)
-let elf_osabi_aros : nat = 15
-(** FenixOS highly-scalable multi-core OS *)
-let elf_osabi_fenixos : nat = 16
-
-(** [string_of_elf_osabi_version m] produces a string representation of the
-  * numeric encoding [m] of the ELF OSABI version.
-  *)
-val string_of_elf_osabi_version : nat -> string
-let string_of_elf_osabi_version m =
-	if m = elf_osabi_none then
-		"No extension or unspecified"
-	else if m = elf_osabi_netbsd then
-		"Hewlett-Packard HP-UX"
-	else if m = elf_osabi_netbsd then
-		"NetBSD"
-	else if m = elf_osabi_gnu then
-		"GNU"
-	else if m = elf_osabi_linux then
-		"Linux (GNU alias)"
-	else if m = elf_osabi_solaris then
-		"Sun Solaris"
-	else if m = elf_osabi_aix then
-		"AIX"
-	else if m = elf_osabi_irix then
-		"IRIX"
-	else if m = elf_osabi_freebsd then
-		"FreeBSD"
-	else if m = elf_osabi_tru64 then
-		"Compaq Tru64 Unix"
-	else if m = elf_osabi_modesto then
-		"Novell Modesto"
-	else if m = elf_osabi_openbsd then
-		"OpenBSD"
-	else if m = elf_osabi_openvms then
-		"OpenVMS"
-	else if m = elf_osabi_nsk then
-		"Hewlett-Packard Non-stop Kernel"
-	else if m = elf_osabi_aros then
-		"Amiga Research OS"
-	else if m = elf_osabi_fenixos then
-		"FenixOS highly-scalable multi-core OS"
-	else
-		"Invalid OSABI version"
-
-(** Checks an architecture defined OSABI version is correct, i.e. in the range
-  * 64 to 255 inclusive.
-  *)
-let is_valid_architecture_defined_osabi_version (n : nat) = n >= 64 && n <= 255
-
-(** ELF Header type *)
-
-(** [ei_nident] is the fixed length of the identification field in the
-  * [elf32_ehdr] type.
-  *)
-val ei_nident : nat
-let ei_nident = 16
-
-(** [elf32_header] is the type of headers for 32-bit ELF files.
-  *)
-type elf32_header =
-  <| elf32_ident    : list unsigned_char (** Identification field *)
-   ; elf32_type     : elf32_half         (** The object file type *)
-   ; elf32_machine  : elf32_half         (** Required machine architecture *)
-   ; elf32_version  : elf32_word         (** Object file version *)
-   ; elf32_entry    : elf32_addr         (** Virtual address for transfer of control *)
-   ; elf32_phoff    : elf32_off          (** Program header table offset in bytes *)
-   ; elf32_shoff    : elf32_off          (** Section header table offset in bytes *)
-   ; elf32_flags    : elf32_word         (** Processor-specific flags *)
-   ; elf32_ehsize   : elf32_half         (** ELF header size in bytes *)
-   ; elf32_phentsize: elf32_half         (** Program header table entry size in bytes *)
-   ; elf32_phnum    : elf32_half         (** Number of entries in program header table *)
-   ; elf32_shentsize: elf32_half         (** Section header table entry size in bytes *)
-   ; elf32_shnum    : elf32_half         (** Number of entries in section header table *)
-   ; elf32_shstrndx : elf32_half         (** Section header table entry for section name string table *)
-   |>
-
-class (HasElf32Header 'a)
-  val get_elf32_header : 'a -> elf32_header
-end
-
-(** [elf64_header] is the type of headers for 32-bit ELF files.
-  *)
-type elf64_header =
-  <| elf64_ident    : list unsigned_char (** Identification field *)
-   ; elf64_type     : elf64_half         (** The object file type *)
-   ; elf64_machine  : elf64_half         (** Required machine architecture *)
-   ; elf64_version  : elf64_word         (** Object file version *)
-   ; elf64_entry    : elf64_addr         (** Virtual address for transfer of control *)
-   ; elf64_phoff    : elf64_off          (** Program header table offset in bytes *)
-   ; elf64_shoff    : elf64_off          (** Section header table offset in bytes *)
-   ; elf64_flags    : elf64_word         (** Processor-specific flags *)
-   ; elf64_ehsize   : elf64_half         (** ELF header size in bytes *)
-   ; elf64_phentsize: elf64_half         (** Program header table entry size in bytes *)
-   ; elf64_phnum    : elf64_half         (** Number of entries in program header table *)
-   ; elf64_shentsize: elf64_half         (** Section header table entry size in bytes *)
-   ; elf64_shnum    : elf64_half         (** Number of entries in section header table *)
-   ; elf64_shstrndx : elf64_half         (** Section header table entry for section name string table *)
-   |>
-
-class (HasElf64Header 'a)
-  val get_elf64_header : 'a -> elf64_header
-end
-
-(** [deduce_endian] deduces the endianness of an ELF file based on the ELF
-  * header's magic number.
-  *)
-val deduce_endianness : list unsigned_char -> endianness
-let deduce_endianness id =
-  match List.index id 5 with
-    | Nothing -> Little (* XXX: random default as read of magic number has failed! *)
-    | Just v  ->
-      if nat_of_unsigned_char v = elf_data_2lsb then
-        Little
-      else if nat_of_unsigned_char v = elf_data_2msb then
-        Big
-      else
-        Little (* XXX: random default as value is not valid! *)
-  end
-
-val get_elf32_header_endianness : elf32_header -> endianness
-let get_elf32_header_endianness hdr =
-  deduce_endianness (hdr.elf32_ident)
-
-val get_elf64_header_endianness : elf64_header -> endianness
-let get_elf64_header_endianness hdr =
-  deduce_endianness (hdr.elf64_ident)
-
-(** 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.
-  *)
-type hdr_print_bundle = (nat -> string) * (nat -> string)
-
-val string_of_elf32_header : hdr_print_bundle -> elf32_header -> string
-let string_of_elf32_header (os, proc) hdr =
-	unlines [
-	  "\t" ^ "Magic number: " ^ show hdr.elf32_ident
-  ; "\t" ^ "Endianness: " ^ show (deduce_endianness hdr.elf32_ident)
-	; "\t" ^ "Type: " ^ string_of_elf_file_type os proc (nat_of_elf32_half hdr.elf32_type)
-  ; "\t" ^ "Version: " ^ string_of_elf_version_number (nat_of_elf32_word hdr.elf32_version)
-	; "\t" ^ "Machine: " ^ string_of_elf_machine_architecture (nat_of_elf32_half hdr.elf32_machine)
-  ; "\t" ^ "Entry point: " ^ show hdr.elf32_entry
-  ; "\t" ^ "Flags: " ^ show hdr.elf32_flags
-  ; "\t" ^ "Entries in program header table: " ^ show hdr.elf32_phnum
-  ; "\t" ^ "Entries in section header table: " ^ show hdr.elf32_shnum
-	]
-
-val string_of_elf64_header : hdr_print_bundle -> elf64_header -> string
-let string_of_elf64_header (os, proc) hdr =
-  unlines [
-    "\t" ^ "Magic number: " ^ show hdr.elf64_ident
-  ; "\t" ^ "Endianness: " ^ show (deduce_endianness hdr.elf64_ident)
-  ; "\t" ^ "Type: " ^ string_of_elf_file_type os proc (nat_of_elf64_half hdr.elf64_type)
-  ; "\t" ^ "Version: " ^ string_of_elf_version_number (nat_of_elf64_word hdr.elf64_version)
-  ; "\t" ^ "Machine: " ^ string_of_elf_machine_architecture (nat_of_elf64_half hdr.elf64_machine)
-  ; "\t" ^ "Entry point: " ^ show hdr.elf64_entry
-  ; "\t" ^ "Flags: " ^ show hdr.elf64_flags
-  ; "\t" ^ "Entries in program header table: " ^ show hdr.elf64_phnum
-  ; "\t" ^ "Entries in section header table: " ^ show hdr.elf64_shnum
-  ]
-
-val string_of_elf32_header_default : elf32_header -> string
-let string_of_elf32_header_default =
-	string_of_elf32_header
-    (default_os_specific_print,
-      default_proc_specific_print)
-
-val string_of_elf64_header_default : elf64_header -> string
-let string_of_elf64_header_default =
-  string_of_elf64_header
-    (default_os_specific_print,
-      default_proc_specific_print)
-	
-instance (Show elf32_header)
-	let show = string_of_elf32_header_default
-end
-
-instance (Show elf64_header)
-  let show = string_of_elf64_header_default
-end
-
-val read_elf32_header : bitstring -> error (elf32_header * bitstring)
-let read_elf32_header bs =
-	repeatM' ei_nident bs (read_unsigned_char default_endianness) >>= fun (ident, bs) ->
-  let endian = deduce_endianness ident in
-	read_elf32_half endian bs >>= fun (typ, bs) ->
-	read_elf32_half endian bs >>= fun (machine, bs) ->
-	read_elf32_word endian bs >>= fun (version, bs) ->
-	read_elf32_addr endian bs >>= fun (entry, bs) ->
-	read_elf32_off  endian bs >>= fun (phoff, bs) ->
-	read_elf32_off  endian bs >>= fun (shoff, bs) ->
-	read_elf32_word endian bs >>= fun (flags, bs) ->
-	read_elf32_half endian bs >>= fun (ehsize, bs) ->
-	read_elf32_half endian bs >>= fun (phentsize, bs) ->
-	read_elf32_half endian bs >>= fun (phnum, bs) ->
-	read_elf32_half endian bs >>= fun (shentsize, bs) ->
-	read_elf32_half endian bs >>= fun (shnum, bs) ->
-	read_elf32_half endian bs >>= fun (shstrndx, bs) ->
-    match List.index ident 4 with
-      | Nothing -> fail "read_elf32_header: transcription of ELF identifier failed"
-      | Just c  ->
-        if nat_of_unsigned_char c = elf_class_32 then
-		      return (<| elf32_ident = ident; elf32_type  = typ;
-                      elf32_machine = machine; elf32_version = version;
-                      elf32_entry = entry; elf32_phoff = phoff;
-                      elf32_shoff = shoff; elf32_flags = flags;
-                      elf32_ehsize = ehsize; elf32_phentsize = phentsize;
-                      elf32_phnum = phnum; elf32_shentsize = shentsize;
-                      elf32_shnum = shnum; elf32_shstrndx = shstrndx |>, bs)
-        else
-          fail "read_elf32_header: not a 32-bit ELF file"
-    end
-
-val read_elf64_header : bitstring -> error (elf64_header * bitstring)
-let read_elf64_header bs =
-  repeatM' ei_nident bs (read_unsigned_char default_endianness) >>= fun (ident, bs) ->
-  let endian = deduce_endianness ident in
-  read_elf64_half endian bs >>= fun (typ, bs) ->
-  read_elf64_half endian bs >>= fun (machine, bs) ->
-  read_elf64_word endian bs >>= fun (version, bs) ->
-  read_elf64_addr endian bs >>= fun (entry, bs) ->
-  read_elf64_off  endian bs >>= fun (phoff, bs) ->
-  read_elf64_off  endian bs >>= fun (shoff, bs) ->
-  read_elf64_word endian bs >>= fun (flags, bs) ->
-  read_elf64_half endian bs >>= fun (ehsize, bs) ->
-  read_elf64_half endian bs >>= fun (phentsize, bs) ->
-  read_elf64_half endian bs >>= fun (phnum, bs) ->
-  read_elf64_half endian bs >>= fun (shentsize, bs) ->
-  read_elf64_half endian bs >>= fun (shnum, bs) ->
-  read_elf64_half endian bs >>= fun (shstrndx, bs) ->
-    match List.index ident 4 with
-      | Nothing -> fail "read_elf64_header: transcription of ELF identifier failed"
-      | Just c  ->
-        if nat_of_unsigned_char c = elf_class_64 then
-          return (<| elf64_ident = ident; elf64_type  = typ;
-                     elf64_machine = machine; elf64_version = version;
-                     elf64_entry = entry; elf64_phoff = phoff;
-                     elf64_shoff = shoff; elf64_flags = flags;
-                     elf64_ehsize = ehsize; elf64_phentsize = phentsize;
-                     elf64_phnum = phnum; elf64_shentsize = shentsize;
-                     elf64_shnum = shnum; elf64_shstrndx = shstrndx |>, bs)
-        else
-          fail "read_elf64_header: not a 64-bit ELF file"
-    end
-
-val is_elf32_header_padding_correct : elf32_header -> bool
-let is_elf32_header_padding_correct ehdr =
-  List.index ehdr.elf32_ident 9  = Just (unsigned_char_of_nat 0) &&
-  List.index ehdr.elf32_ident 10 = Just (unsigned_char_of_nat 0) &&
-  List.index ehdr.elf32_ident 11 = Just (unsigned_char_of_nat 0) &&
-  List.index ehdr.elf32_ident 12 = Just (unsigned_char_of_nat 0) &&
-  List.index ehdr.elf32_ident 13 = Just (unsigned_char_of_nat 0) &&
-  List.index ehdr.elf32_ident 14 = Just (unsigned_char_of_nat 0) &&
-  List.index ehdr.elf32_ident 15 = Just (unsigned_char_of_nat 0)
-
-val is_elf32_header_magic_number_correct : elf32_header -> bool
-let is_elf32_header_magic_number_correct ehdr =
-  List.index ehdr.elf32_ident 0 = Just (unsigned_char_of_nat 127) &&
-  List.index ehdr.elf32_ident 1 = Just (unsigned_char_of_nat 69)  &&
-  List.index ehdr.elf32_ident 2 = Just (unsigned_char_of_nat 76)  &&
-  List.index ehdr.elf32_ident 3 = Just (unsigned_char_of_nat 70)
-
-val is_elf32_header_class_correct : elf32_header -> bool
-let is_elf32_header_class_correct ehdr =
-  List.index ehdr.elf32_ident 4 = Just (unsigned_char_of_nat 1)
-
-val is_elf32_header_version_correct : elf32_header -> bool
-let is_elf32_header_version_correct ehdr =
-  List.index ehdr.elf32_ident 6 = Just (unsigned_char_of_nat 1)
-
-(** [is_valid_elf32_header] 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 is_elf32_header_valid : elf32_header -> bool
-let is_elf32_header_valid ehdr =
-  List.length ehdr.elf32_ident = ei_nident &&
-  is_elf32_header_magic_number_correct ehdr &&
-  is_elf32_header_padding_correct ehdr &&
-  is_elf32_header_class_correct ehdr &&
-  is_elf32_header_version_correct ehdr
-
-(** [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_elf32_header_program_table_size : elf32_header -> nat
-let get_elf32_header_program_table_size ehdr =
-  let phentsize = nat_of_elf32_half ehdr.elf32_phentsize in
-  let phnum     = nat_of_elf32_half ehdr.elf32_phnum in
-    phentsize * phnum
-
-(** [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 get_elf64_header_program_table_size : elf64_header -> nat
-let get_elf64_header_program_table_size ehdr =
-  let phentsize = nat_of_elf64_half ehdr.elf64_phentsize in
-  let phnum     = nat_of_elf64_half ehdr.elf64_phnum in
-    phentsize * phnum
-
-(** [is_elf32_header_section_table_present] calculates whether a section table
-  * is present in the ELF file or not.
-  *)
-val is_elf32_header_section_table_present : elf32_header -> bool
-let is_elf32_header_section_table_present ehdr =
-  not (nat_of_elf32_off ehdr.elf32_shoff = 0)
-
-(** [is_elf64_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
-let is_elf64_header_section_table_present ehdr =
-  not (nat_of_elf64_off ehdr.elf64_shoff = 0)
-
-(** [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_elf32_header_section_table_size : elf32_header -> nat
-let get_elf32_header_section_table_size ehdr =
-  let shentsize = nat_of_elf32_half ehdr.elf32_shentsize in
-  let shnum     = nat_of_elf32_half ehdr.elf32_shnum in
-    shentsize * shnum
-
-(** [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.
-  *)
-val get_elf64_header_section_table_size : elf64_header -> nat
-let get_elf64_header_section_table_size ehdr =
-  let shentsize = nat_of_elf64_half ehdr.elf64_shentsize in
-  let shnum     = nat_of_elf64_half ehdr.elf64_shnum in
-    shentsize * shnum