Modified ocaml backend to use ocamlfind for linksem and lem

Fixed test cases for ocaml backend and interpreter

1 files changed, 0 insertions, 1202 deletions

diff --git a/lib/ocaml_rts/linksem/elf_dynamic.ml b/lib/ocaml_rts/linksem/elf_dynamic.ml
deleted file mode 100644
index 0355337e..00000000
--- a/lib/ocaml_rts/linksem/elf_dynamic.ml
+++ /dev/null
@@ -1,1202 +0,0 @@
-(*Generated by Lem from elf_dynamic.lem.*)
-(** [elf_dynamic] module exports types and definitions relating to the dynamic
-  * section and dynamic linking functionality of an ELF file.
-  *)
-
-open Lem_basic_classes
-open Lem_bool
-open Lem_list
-open Lem_num
-open Lem_string
-
-open Byte_sequence
-open Endianness
-open Error
-open Show
-open String_table
-
-open Elf_file
-open Elf_header
-open Elf_relocation
-open Elf_section_header_table
-open Elf_program_header_table
-open Elf_types_native_uint
-
-(** Validity checks *)
-
-(** [is_elf32_valid_program_header_table_for_dynamic_linking pht] checks whether
-  * a program header table [pht] is a valid program header table for an ELF file
-  * that will be potentially dynamically linked.  Returns true if there is exactly
-  * one segment header of type [elf_pt_interp], i.e. contains a string pointing
-  * to the requested dynamic interpreter.
-  *)
-(*val is_elf32_valid_program_header_table_for_dynamic_linking : elf32_program_header_table ->
-  bool*)
-let is_elf32_valid_program_header_table_for_dynamic_linking pht:bool=  
- (List.length (List.filter (fun x -> Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string x.elf32_p_type)) elf_pt_interp) pht) = 1)
-  
-(** [is_elf64_valid_program_header_table_for_dynamic_linking pht] checks whether
-  * a program header table [pht] is a valid program header table for an ELF file
-  * that will be potentially dynamically linked.  Returns true if there is exactly
-  * one segment header of type [elf_pt_interp], i.e. contains a string pointing
-  * to the requested dynamic interpreter.
-  *)
-(*val is_elf64_valid_program_header_table_for_dynamic_linking : elf64_program_header_table ->
-  bool*)
-let is_elf64_valid_program_header_table_for_dynamic_linking pht:bool=  
- (List.length (List.filter (fun x -> Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string x.elf64_p_type)) elf_pt_interp) pht) = 1)
-
-(** Dynamic section entry *)
-
-(** [dyn_union] represents the C-union type used in the definition of [elf32_dyn]
-  * and [elf64_dyn] types below.  Some section tags correspond to entries where
-  * the fields are either unspecified or ignored, hence the presence of the
-  * [D_Ignored] constructor.
-  *)
-type( 'a, 'b) dyn_union
-  = D_Val of 'a
-  | D_Ptr of 'b
-  | D_Ignored of byte_sequence
-  
-(** [elf32_dyn] captures the notion of an ELF32 dynamic section entry.
-  * Specialises the [dyn_union] type above to using [elf32_word] values and
-  * [elf32_addr] pointers.
-  *)
-type elf32_dyn =
-  { elf32_dyn_tag  : Int32.t                     (** The type of the entry. *)
-   ; elf32_dyn_d_un : (Uint32.uint32, Uint32.uint32) dyn_union (** The value of the entry, stored as a union. *)
-   }
-   
-(** [elf64_dyn] captures the notion of an ELF32 dynamic section entry.
-  * Specialises the [dyn_union] type above to using [elf64_xword] values and
-  * [elf64_addr] pointers.
-  *)
-type elf64_dyn =
-  { elf64_dyn_tag  : Int64.t                     (** The type of the entry. *)
-   ; elf64_dyn_d_un : (Uint64.uint64, Uint64.uint64) dyn_union (** The value of the entry, stored as a union. *)
-   }
-
-(** Dynamic section tags *)
-
-(** [dt_null] marks the end of the dynamic array *)
-let dt_null : Nat_big_num.num= (Nat_big_num.of_int 0)
-(** [dt_needed] holds the string table offset of a string containing the name of
-  * a needed library.
-  *)
-let dt_needed : Nat_big_num.num= (Nat_big_num.of_int 1)
-(** [dt_pltrelsz] holds the size in bytes of relocation entries associated with
-  * the PLT.
-  *)
-let dt_pltrelsz : Nat_big_num.num= (Nat_big_num.of_int 2)
-(** [dt_pltgot] holds an address associated with the PLT or GOT. *)
-let dt_pltgot : Nat_big_num.num= (Nat_big_num.of_int 3)
-(** [dt_hash] holds the address of a symbol-table hash. *)
-let dt_hash : Nat_big_num.num= (Nat_big_num.of_int 4)
-(** [dt_strtab] holds the address of the string table. *)
-let dt_strtab : Nat_big_num.num= (Nat_big_num.of_int 5)
-(** [dt_symtab] holds the address of a symbol table. *)
-let dt_symtab : Nat_big_num.num= (Nat_big_num.of_int 6)
-(** [dt_rela] holds the address of a relocation table. *)
-let dt_rela : Nat_big_num.num= (Nat_big_num.of_int 7)
-(** [dt_relasz] holds the size in bytes of the relocation table. *)
-let dt_relasz : Nat_big_num.num= (Nat_big_num.of_int 8)
-(** [dt_relaent] holds the size in bytes of a relocation table entry. *)
-let dt_relaent : Nat_big_num.num= (Nat_big_num.of_int 9)
-(** [dt_strsz] holds the size in bytes of the string table. *)
-let dt_strsz : Nat_big_num.num= (Nat_big_num.of_int 10)
-(** [dt_syment] holds the size in bytes of a symbol table entry. *)
-let dt_syment : Nat_big_num.num= (Nat_big_num.of_int 11)
-(** [dt_init] holds the address of the initialisation function. *)
-let dt_init : Nat_big_num.num= (Nat_big_num.of_int 12)
-(** [dt_fini] holds the address of the finalisation function. *)
-let dt_fini : Nat_big_num.num= (Nat_big_num.of_int 13)
-(** [dt_soname] holds the string table offset of a string containing the shared-
-  * object name.
-  *)
-let dt_soname : Nat_big_num.num= (Nat_big_num.of_int 14)
-(** [dt_rpath] holds the string table offset of a string containing the library
-  * search path.
-  *)
-let dt_rpath : Nat_big_num.num= (Nat_big_num.of_int 15)
-(** [dt_symbolic] alters the linker's symbol resolution algorithm so that names
-  * are resolved first from the shared object file itself, rather than the
-  * executable file.
-  *)
-let dt_symbolic : Nat_big_num.num= (Nat_big_num.of_int 16)
-(** [dt_rel] is similar to [dt_rela] except its table has implicit addends. *)
-let dt_rel : Nat_big_num.num= (Nat_big_num.of_int 17)
-(** [dt_relsz] holds the size in bytes of the [dt_rel] relocation table. *)
-let dt_relsz : Nat_big_num.num= (Nat_big_num.of_int 18)
-(** [dt_relent] holds the size in bytes of a [dt_rel] relocation entry. *)
-let dt_relent : Nat_big_num.num= (Nat_big_num.of_int 19)
-(** [dt_pltrel] specifies the type of relocation entry to which the PLT refers. *)
-let dt_pltrel : Nat_big_num.num= (Nat_big_num.of_int 20)
-(** [dt_debug] is used for debugging and its purpose is not specified in the ABI.
-  * Programs using this entry are not ABI-conformant.
-  *)
-let dt_debug : Nat_big_num.num= (Nat_big_num.of_int 21)
-(** [dt_textrel] absence of this entry indicates that no relocation entry should
-  * cause a modification to a non-writable segment.  Otherwise, if present, one
-  * or more relocation entries may request modifications to a non-writable
-  * segment.
-  *)
-let dt_textrel : Nat_big_num.num= (Nat_big_num.of_int 22)
-(** [dt_jmprel]'s member holds the address of relocation entries associated with
-  * the PLT.
-  *)
-let dt_jmprel : Nat_big_num.num= (Nat_big_num.of_int 23)
-(** [dt_bindnow] instructs the linker to process all relocations for the object
-  * containing the entry before transferring control to the program.
-  *)
-let dt_bindnow : Nat_big_num.num= (Nat_big_num.of_int 24)
-(** [dt_init_array] holds the address to the array of pointers to initialisation
-  * functions.
-  *)
-let dt_init_array : Nat_big_num.num= (Nat_big_num.of_int 25)
-(** [dt_fini_array] holds the address to the array of pointers to finalisation
-  * functions.
-  *)
-let dt_fini_array : Nat_big_num.num= (Nat_big_num.of_int 26)
-(** [dt_init_arraysz] holds the size in bytes of the array of pointers to
-  * initialisation functions.
-  *)
-let dt_init_arraysz : Nat_big_num.num= (Nat_big_num.of_int 27)
-(** [dt_fini_arraysz] holds the size in bytes of the array of pointers to
-  * finalisation functions.
-  *)
-let dt_fini_arraysz : Nat_big_num.num= (Nat_big_num.of_int 28)
-(** [dt_runpath] holds an offset into the string table holding a string containing
-  * the library search path.
-  *)
-let dt_runpath : Nat_big_num.num= (Nat_big_num.of_int 29)
-(** [dt_flags] holds flag values specific to the object being loaded. *)
-let dt_flags : Nat_big_num.num= (Nat_big_num.of_int 30)
-let dt_encoding : Nat_big_num.num= (Nat_big_num.of_int 32)
-(** [dt_preinit_array] holds the address to the array of pointers of pre-
-  * initialisation functions.
-  *)
-let dt_preinit_array : Nat_big_num.num= (Nat_big_num.of_int 32)
-(** [dt_preinit_arraysz] holds the size in bytes of the array of pointers of
-  * pre-initialisation functions.
-  *)
-let dt_preinit_arraysz : Nat_big_num.num= (Nat_big_num.of_int 33)
-(** [dt_loos] and [dt_hios]: this inclusive range is reserved for OS-specific
-  * semantics.
-  *)
-let dt_loos : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 805306374))(Nat_big_num.of_int 1)) (* 0x6000000D *)
-let dt_hios : Nat_big_num.num=  ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939522048)) (* 0x6ffff000 *)
-(** [dt_loproc] and [dt_hiproc]: this inclusive range is reserved for processor
-  * specific semantics.
-  *)
-let dt_loproc : Nat_big_num.num=  ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 939524096)) (* 0x70000000 *)
-let dt_hiproc : Nat_big_num.num=  (Nat_big_num.add ( Nat_big_num.mul(Nat_big_num.of_int 2)(Nat_big_num.of_int 1073741823))(Nat_big_num.of_int 1)) (* 0x7fffffff *)
-
-(** [string_of_dynamic_tag so t os proc] produces a string-based representation of
-  * dynamic section tag [t].  For tag values between LO_OS and HI_OS [os] is
-  * used to produce the resulting value.  For tag values between LO_PROC and
-  * HI_PROC [proc] is used to produce the resulting value.  Boolean flag [so]
-  * indicates whether the flag in question is derived from a shared object file,
-  * which alters the printing of ENCODING and PRE_INITARRAY flags.
-  *)
-(*val string_of_dynamic_tag : bool -> natural -> (natural -> bool) -> (natural -> string) -> (natural -> string)
-  -> string*)
-let string_of_dynamic_tag shared_object tag os_additional_ranges os proc:string=  
- (if Nat_big_num.equal tag dt_null then
-    "NULL"
-  else if Nat_big_num.equal tag dt_needed then
-    "NEEDED"
-  else if Nat_big_num.equal tag dt_pltrelsz then
-    "PLTRELSZ"
-  else if Nat_big_num.equal tag dt_pltgot then
-    "PLTGOT"
-  else if Nat_big_num.equal tag dt_hash then
-    "HASH"
-  else if Nat_big_num.equal tag dt_strtab then
-    "STRTAB"
-  else if Nat_big_num.equal tag dt_symtab then
-    "SYMTAB"
-  else if Nat_big_num.equal tag dt_rela then
-    "RELA"
-  else if Nat_big_num.equal tag dt_relasz then
-    "RELASZ"
-  else if Nat_big_num.equal tag dt_relaent then
-    "RELAENT"
-  else if Nat_big_num.equal tag dt_strsz then
-    "STRSZ"
-  else if Nat_big_num.equal tag dt_syment then
-    "SYMENT"
-  else if Nat_big_num.equal tag dt_init then
-    "INIT"
-  else if Nat_big_num.equal tag dt_fini then
-    "FINI"
-  else if Nat_big_num.equal tag dt_soname then
-    "SONAME"
-  else if Nat_big_num.equal tag dt_rpath then
-    "RPATH"
-  else if Nat_big_num.equal tag dt_symbolic then
-    "SYMBOLIC"
-  else if Nat_big_num.equal tag dt_rel then
-    "REL"
-  else if Nat_big_num.equal tag dt_relsz then
-    "RELSZ"
-  else if Nat_big_num.equal tag dt_relent then
-    "RELENT"
-  else if Nat_big_num.equal tag dt_pltrel then
-    "PLTREL"
-  else if Nat_big_num.equal tag dt_debug then
-    "DEBUG"
-  else if Nat_big_num.equal tag dt_textrel then
-    "TEXTREL"
-  else if Nat_big_num.equal tag dt_jmprel then
-    "JMPREL"
-  else if Nat_big_num.equal tag dt_bindnow then
-    "BIND_NOW"
-  else if Nat_big_num.equal tag dt_init_array then
-    "INIT_ARRAY"
-  else if Nat_big_num.equal tag dt_fini_array then
-    "FINI_ARRAY"
-  else if Nat_big_num.equal tag dt_init_arraysz then
-    "INIT_ARRAYSZ"
-  else if Nat_big_num.equal tag dt_fini_arraysz then
-    "FINI_ARRAYSZ"
-  else if Nat_big_num.equal tag dt_runpath then
-    "RUNPATH"
-  else if Nat_big_num.equal tag dt_flags then
-    "FLAGS"
-  else if Nat_big_num.equal tag dt_encoding then
-    if not shared_object then
-      "ENCODING"
-    else
-      "PREINIT_ARRAY"
-  else if Nat_big_num.equal tag dt_preinit_arraysz then
-    "PREINIT_ARRAYSZ"
-  else if Nat_big_num.greater_equal tag dt_loproc && Nat_big_num.less_equal tag dt_hiproc then
-    proc tag
-  else if Nat_big_num.greater_equal tag dt_loos && Nat_big_num.less_equal tag dt_hios then
-    os tag
-  else if os_additional_ranges tag then
-    os tag
-  else
-    "Invalid dynamic section tag")
-    
-(** [tag_correspondence] is a type used to emulate the functionality of a C-union
-  * in Lem.  The type records whether the union should be interpreted as a value,
-  * a pointer, or a "do not care" value.  An accompanying function will map a
-  * dynamic section tag to a [tag_correspondence], so that transcription functions
-  * know how to properly use the [dyn_union] value in a dynamic section entry.
-  *)
-type tag_correspondence
-  = C_Val     (** [dyn_union] should be interpreted as a value. *)
-  | C_Ptr     (** [dyn_union] should be interpreted as a pointer. *)
-  | C_Ignored (** [dyn_union] is irrelevant, so we do not care. *)
-  
-(** [tag_correspondence_of_tag tag os_additional_ranges os proc] produces a
-  * [tag_correspondence] value for a given dynamic tag, [tag].  Some tag values
-  * are reserved for interpretation by the OS or processor supplement (i.e. the
-  * ABI).  We therefore also take in a predicate, [os_additional_ranges], that
-  * recognises when a tag is "special" for a given ABI, and a means of interpreting
-  * that tag, using [os] and [proc] functions.
-  *)
-(*val tag_correspondence_of_tag : bool -> natural -> (natural -> bool) -> (natural -> error tag_correspondence) ->
-  (natural -> error tag_correspondence) -> error tag_correspondence*)
-let tag_correspondence_of_tag shared_object tag os_additional_ranges os proc:(tag_correspondence)error=  
- (if Nat_big_num.equal tag dt_null then
-    return C_Ignored
-  else if Nat_big_num.equal tag dt_needed then
-    return C_Val
-  else if Nat_big_num.equal tag dt_pltrelsz then
-    return C_Val
-  else if Nat_big_num.equal tag dt_pltgot then
-    return C_Ptr
-  else if Nat_big_num.equal tag dt_hash then
-    return C_Ptr
-  else if Nat_big_num.equal tag dt_strtab then
-    return C_Ptr
-  else if Nat_big_num.equal tag dt_symtab then
-    return C_Ptr
-  else if Nat_big_num.equal tag dt_rela then
-    return C_Ptr
-  else if Nat_big_num.equal tag dt_relasz then
-    return C_Val
-  else if Nat_big_num.equal tag dt_relaent then
-    return C_Val
-  else if Nat_big_num.equal tag dt_strsz then
-    return C_Val
-  else if Nat_big_num.equal tag dt_syment then
-    return C_Val
-  else if Nat_big_num.equal tag dt_init then
-    return C_Ptr
-  else if Nat_big_num.equal tag dt_fini then
-    return C_Ptr
-  else if Nat_big_num.equal tag dt_soname then
-    return C_Val
-  else if Nat_big_num.equal tag dt_rpath then
-    return C_Val
-  else if Nat_big_num.equal tag dt_symbolic then
-    return C_Ignored
-  else if Nat_big_num.equal tag dt_rel then
-    return C_Ptr
-  else if Nat_big_num.equal tag dt_relsz then
-    return C_Val
-  else if Nat_big_num.equal tag dt_relent then
-    return C_Val
-  else if Nat_big_num.equal tag dt_pltrel then
-    return C_Val
-  else if Nat_big_num.equal tag dt_debug then
-    return C_Ptr
-  else if Nat_big_num.equal tag dt_textrel then
-    return C_Ignored
-  else if Nat_big_num.equal tag dt_jmprel then
-    return C_Ptr
-  else if Nat_big_num.equal tag dt_bindnow then
-    return C_Ignored
-  else if Nat_big_num.equal tag dt_init_array then
-    return C_Ptr
-  else if Nat_big_num.equal tag dt_fini_array then
-    return C_Ptr
-  else if Nat_big_num.equal tag dt_init_arraysz then
-    return C_Val
-  else if Nat_big_num.equal tag dt_fini_arraysz then
-    return C_Val
-  else if Nat_big_num.equal tag dt_runpath then
-    return C_Val
-  else if Nat_big_num.equal tag dt_flags then
-    return C_Val
-  else if Nat_big_num.equal tag dt_encoding then
-    if not shared_object then
-      return C_Ignored
-    else
-      return C_Ptr
-  else if Nat_big_num.equal tag dt_preinit_arraysz then
-    return C_Val
-  else if Nat_big_num.greater_equal tag dt_loproc && Nat_big_num.less_equal tag dt_hiproc then
-    proc tag
-  else if Nat_big_num.greater_equal tag dt_loos && Nat_big_num.less_equal tag dt_hios then
-    os tag
-  else if os_additional_ranges tag then
-    os tag
-  else
-    fail ("tag_correspondence_of_tag: invalid dynamic section tag"))
-    
-(** [read_elf32_dyn endian bs0 so os_additional_ranges os proc] reads an [elf32_dyn]
-  * record from byte sequence [bs0], assuming endianness [endian].  As mentioned
-  * above some ABIs reserve additional tag values for their own purposes.  These
-  * are recognised by the predicate [os_additional_ranges] and interpreted by
-  * the functions [os] and [proc].  Fails if the transcription of the record from
-  * [bs0] fails, or if [os] or [proc] fail.
-  *)
-(*val read_elf32_dyn : endianness -> byte_sequence -> bool -> (natural -> bool) -> (natural -> error tag_correspondence) ->
-  (natural -> error tag_correspondence) -> error (elf32_dyn * byte_sequence)*)
-let read_elf32_dyn endian bs0 shared_object os_additional_ranges os proc:(elf32_dyn*byte_sequence)error=  
- (read_elf32_sword endian bs0 >>= (fun (tag0, bs1) ->
-  let tag = (Nat_big_num.abs (Nat_big_num.of_int32 tag0)) in
-  tag_correspondence_of_tag shared_object tag os_additional_ranges os proc >>= (fun corr ->
-    (match corr with
-      | C_Ptr ->
-        read_elf32_addr endian bs1 >>= (fun (ptr, bs2) ->
-        return ({ elf32_dyn_tag = tag0 ; elf32_dyn_d_un = (D_Ptr ptr) }, bs2))
-      | C_Val ->
-        read_elf32_word endian bs1 >>= (fun (vl, bs2) ->
-        return ({ elf32_dyn_tag = tag0 ; elf32_dyn_d_un = (D_Val vl) }, bs2))
-      | C_Ignored ->
-        (match endian with
-          | Big    ->
-            read_4_bytes_be bs1 >>= (fun ((b1, b2, b3, b4), bs2) ->
-            let cut = (Byte_sequence.from_byte_lists [[b1; b2; b3; b4]]) in
-            return ({ elf32_dyn_tag = tag0 ; elf32_dyn_d_un = (D_Ignored cut) }, bs2))
-          | Little ->
-            read_4_bytes_le bs1 >>= (fun ((b1, b2, b3, b4), bs2) ->
-            let cut = (Byte_sequence.from_byte_lists [[b1; b2; b3; b4]]) in
-            return ({ elf32_dyn_tag = tag0 ; elf32_dyn_d_un = (D_Ignored cut) }, bs2))
-        )
-    ))))
-    
-(** [read_elf64_dyn endian bs0 os_additional_ranges os proc] reads an [elf64_dyn]
-  * record from byte sequence [bs0], assuming endianness [endian].  As mentioned
-  * above some ABIs reserve additional tag values for their own purposes.  These
-  * are recognised by the predicate [os_additional_ranges] and interpreted by
-  * the functions [os] and [proc].  Fails if the transcription of the record from
-  * [bs0] fails, or if [os] or [proc] fail.
-  *)
-(*val read_elf64_dyn : endianness -> byte_sequence -> bool -> (natural -> bool) ->
-  (natural -> error tag_correspondence) -> (natural -> error tag_correspondence) ->
-    error (elf64_dyn * byte_sequence)*)
-let read_elf64_dyn endian bs0 shared_object os_additional_ranges os proc:(elf64_dyn*byte_sequence)error=  
- (read_elf64_sxword endian bs0 >>= (fun (tag0, bs1) ->
-  let tag = (Nat_big_num.abs (Nat_big_num.of_int64 tag0)) in
-  tag_correspondence_of_tag shared_object tag os_additional_ranges os proc >>= (fun corr ->
-    (match corr with
-      | C_Ptr ->
-        read_elf64_addr endian bs1 >>= (fun (ptr, bs2) ->
-        return ({ elf64_dyn_tag = tag0 ; elf64_dyn_d_un = (D_Ptr ptr) }, bs2))
-      | C_Val ->
-        read_elf64_xword endian bs1 >>= (fun (vl, bs2) ->
-        return ({ elf64_dyn_tag = tag0 ; elf64_dyn_d_un = (D_Val vl) }, bs2))
-      | C_Ignored ->
-        (match endian with
-          | Big    ->
-            read_8_bytes_be bs1 >>= (fun ((b1, b2, b3, b4, b5, b6, b7, b8), bs2) ->
-            let cut = (Byte_sequence.from_byte_lists [[b1; b2; b3; b4; b5; b6; b7; b8]]) in
-            return ({ elf64_dyn_tag = tag0 ; elf64_dyn_d_un = (D_Ignored cut) }, bs2))
-          | Little ->
-            read_8_bytes_le bs1 >>= (fun ((b1, b2, b3, b4, b5, b6, b7, b8), bs2) ->
-            let cut = (Byte_sequence.from_byte_lists [[b1; b2; b3; b4; b5; b6; b7; b8]]) in
-            return ({ elf64_dyn_tag = tag0 ; elf64_dyn_d_un = (D_Ignored cut) }, bs2))
-        )
-    ))))
-    
-(** [obtain_elf32_dynamic_section_contents' endian bs0 os_additional_ranges os
-  * proc] exhaustively reads in [elf32_dyn] values from byte sequence [bs0],
-  * interpreting ABI-specific dynamic tags with [os_additional_ranges], [os], and
-  * [proc] as mentioned above.  Fails if [bs0]'s length modulo the size of an
-  * [elf32_dyn] entry is not 0.
-  *)
-(*val obtain_elf32_dynamic_section_contents' : endianness -> byte_sequence ->
-  bool -> (natural -> bool) -> (natural -> error tag_correspondence) ->
-  (natural -> error tag_correspondence) -> error (list elf32_dyn)*)
-let rec obtain_elf32_dynamic_section_contents' endian bs0 shared_object os_additional_ranges os proc:((elf32_dyn)list)error=  
- (if Nat_big_num.equal (Byte_sequence.length0 bs0)(Nat_big_num.of_int 0) then
-    return []
-  else
-    read_elf32_dyn endian bs0 shared_object os_additional_ranges os proc >>= (fun (head, bs0) ->
-    if Nat_big_num.equal (Nat_big_num.of_int32 head.elf32_dyn_tag) ( dt_null) then (* DT_NULL marks end of array *)
-      return [head]
-    else
-    obtain_elf32_dynamic_section_contents' endian bs0 shared_object os_additional_ranges os proc >>= (fun tail ->
-    return (head::tail))))
-    
-(** [obtain_elf64_dynamic_section_contents' endian bs0 os_additional_ranges os
-  * proc] exhaustively reads in [elf64_dyn] values from byte sequence [bs0],
-  * interpreting ABI-specific dynamic tags with [os_additional_ranges], [os], and
-  * [proc] as mentioned above.  Fails if [bs0]'s length modulo the size of an
-  * [elf64_dyn] entry is not 0.
-  *)
-(*val obtain_elf64_dynamic_section_contents' : endianness -> byte_sequence ->
-  bool -> (natural -> bool) -> (natural -> error tag_correspondence) ->
-  (natural -> error tag_correspondence) -> error (list elf64_dyn)*)
-let rec obtain_elf64_dynamic_section_contents' endian bs0 shared_object os_additional_ranges os proc:((elf64_dyn)list)error=  
- (if Nat_big_num.equal (Byte_sequence.length0 bs0)(Nat_big_num.of_int 0) then
-    return []
-  else
-    read_elf64_dyn endian bs0 shared_object os_additional_ranges os proc >>= (fun (head, bs0) ->
-    if Nat_big_num.equal (Nat_big_num.of_int64 head.elf64_dyn_tag) ( dt_null) then (* DT_NULL marks end of array *)
-      return [head]
-    else
-      obtain_elf64_dynamic_section_contents' endian bs0 shared_object os_additional_ranges os proc >>= (fun tail ->
-      return (head::tail))))
-
-(** [obtain_elf32_dynamic_section_contents' f1 os_additional_ranges os
-  * proc bs0] exhaustively reads in [elf32_dyn] values from byte sequence [bs0],
-  * obtaining endianness and the section header table from [elf32_file] f1,
-  * interpreting ABI-specific dynamic tags with [os_additional_ranges], [os], and
-  * [proc] as mentioned above.  Fails if [bs0]'s length modulo the size of an
-  * [elf32_dyn] entry is not 0.
-  *)
-(*val obtain_elf32_dynamic_section_contents : elf32_file ->
-  (natural -> bool) -> (natural -> error tag_correspondence) ->
-  (natural -> error tag_correspondence) -> byte_sequence -> error (list elf32_dyn)*)
-let obtain_elf32_dynamic_section_contents f1 os_additional_ranges os proc bs0:((elf32_dyn)list)error=  
- (let endian = (get_elf32_header_endianness f1.elf32_file_header) in
-  let sht = (f1.elf32_file_section_header_table) in
-  let shared_object = (is_elf32_shared_object_file f1.elf32_file_header) in
-    (match List.filter (fun ent -> Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string ent.elf32_sh_type)) sht_dynamic) sht with
-      | [] -> fail "obtain_elf32_dynamic_section_contents: no SHT_DYNAMIC section header entries"
-      | [dyn] ->
-        let off = (Nat_big_num.of_string (Uint32.to_string dyn.elf32_sh_offset)) in
-        let siz = (Nat_big_num.of_string (Uint32.to_string dyn.elf32_sh_size)) in
-        Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel ->
-        obtain_elf32_dynamic_section_contents' endian rel shared_object os_additional_ranges os proc)
-      | _ -> fail "obtain_elf32_dynamic_section_contents: multiple SHT_DYNAMIC section header entries"
-    ))
-
-(** [obtain_elf64_dynamic_section_contents' f1 os_additional_ranges os
-  * proc bs0] exhaustively reads in [elf64_dyn] values from byte sequence [bs0],
-  * obtaining endianness and the section header table from [elf64_file] f1,
-  * interpreting ABI-specific dynamic tags with [os_additional_ranges], [os], and
-  * [proc] as mentioned above.  Fails if [bs0]'s length modulo the size of an
-  * [elf64_dyn] entry is not 0.
-  *)
-(*val obtain_elf64_dynamic_section_contents : elf64_file ->
-  (natural -> bool) -> (natural -> error tag_correspondence) ->
-  (natural -> error tag_correspondence) -> byte_sequence -> error (list elf64_dyn)*)
-let obtain_elf64_dynamic_section_contents f1 os_additional_ranges os proc bs0:((elf64_dyn)list)error=  
- (let endian = (get_elf64_header_endianness f1.elf64_file_header) in
-  let sht = (f1.elf64_file_section_header_table) in
-  let shared_object = (is_elf64_shared_object_file f1.elf64_file_header) in
-    (match List.filter (fun ent -> Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string ent.elf64_sh_type)) sht_dynamic) sht with
-      | [] -> fail "obtain_elf64_dynamic_section_contents: no SHT_DYNAMIC section header entries"
-      | [dyn] ->
-        let off = (Nat_big_num.of_string (Uint64.to_string dyn.elf64_sh_offset)) in
-        let siz = (Ml_bindings.nat_big_num_of_uint64 dyn.elf64_sh_size) in
-        Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel ->
-        obtain_elf64_dynamic_section_contents' endian rel shared_object os_additional_ranges os proc)
-      | _ -> fail "obtain_elf64_dynamic_section_contents: multiple SHT_DYNAMIC section header entries"
-    ))
-
-(** DT Flags values *)
-
-(** [df_origin] specific that the object being loaded may make reference to the
-  * $(ORIGIN) substitution string.
-  *)
-let df_origin : Nat_big_num.num= (Nat_big_num.of_int 1) (* 0x1 *)
-(** [df_symbolic] changes the linker's symbol resolution algorithm, resolving
-  * symbols first from the shared object file rather than the executable file.
-  *)
-let df_symbolic : Nat_big_num.num= (Nat_big_num.of_int 2) (* 0x2 *)
-(** [df_textrel] if this flag is not set then no relocation entry should cause
-  * modification to a non-writable segment.
-  *)
-let df_textrel : Nat_big_num.num= (Nat_big_num.of_int 4) (* 0x4 *)
-(** [df_bindnow] if set this instructs the linker to process all relocation entries
-  * of the containing object before transferring control to the program.
-  *)
-let df_bindnow : Nat_big_num.num= (Nat_big_num.of_int 8) (* 0x8 *)
-(** [df_static_tls] if set instructs the linker to reject all attempts to load
-  * the containing file dynamically.
-  *)
-let df_static_tls : Nat_big_num.num= (Nat_big_num.of_int 16) (* 0x10 *)
-
-(** [check_flag] is a utility function for testing whether a flag is set.
-  * TODO: so simple it is probably unneccessary now.
-  *)
-(*val check_flag : natural -> natural -> bool*)
-let check_flag m pos:bool=  ( Nat_big_num.equal m pos)
-
-(** [string_of_dt_flag f] produces a string-based representation of dynamic
-  * section flag [f].
-  *)
-(*val string_of_dt_flag : natural -> string*)
-let string_of_dt_flag flag:string=  
- (if check_flag flag(Nat_big_num.of_int 0) then
-    "None"
-  else if check_flag flag df_origin then
-    "ORIGIN"
-  else if check_flag flag df_bindnow then
-    "BIND_NOW"
-  else if check_flag flag df_symbolic then
-    "SYMBOLIC"
-  else if check_flag flag df_textrel then
-    "TEXTREL"
-  else if check_flag flag df_static_tls then
-    "STATIC_TLS"
-  else if check_flag flag ( Nat_big_num.add df_bindnow df_static_tls) then
-    "BIND_NOW STATIC_TLS"
-  else if check_flag flag ( Nat_big_num.add df_static_tls df_symbolic) then
-    "SYMBOLIC STATIC_TLS"
-  else (* XXX: add more as needed *)
-    "Invalid dynamic section flag")
-    
-(** [rel_type] represents the two types of relocation records potentially present
-  * in an ELF file: relocation, and relocation with addends.
-  *)
-type rel_type
-  = Rel  (** Plain relocation type. *)
-  | RelA (** Relocation with addends type. *)
-  
-(** [string_of_rel_type r] produces a string-based representation of [rel_type],
-  * [r].
-  *)
-(*val string_of_rel_type : rel_type -> string*)
-let string_of_rel_type r:string=  
- ((match r with
-    | Rel  -> "REL"
-    | RelA -> "RELA"
-  ))
-    
-(** Type [dyn_value] represents the value of an ELF dynamic section entry.  Values
-  * can represent various different types of objects (e.g. paths to libraries, or
-  * flags, or sizes of other entries in a file), and this type collates them all.
-  * Parameterised over two type variables so the type can be shared between ELF32
-  * and ELF64.
-  *)
-type( 'addr, 'size) dyn_value
-  = Address   of 'addr    (** An address. *)
-  | Size      of 'size    (** A size (in bytes). *)
-  | FName     of string   (** A filename. *)
-  | SOName    of string   (** A shared object name. *)
-  | Path      of string   (** A path to some directory. *)
-  | RPath     of string   (** A "run path". *)
-  | RunPath   of string   (** A "run path". *)
-  | Library   of string   (** A library path. *)
-  | Flags1    of Nat_big_num.num  (** Flags. *)
-  | Flags     of Nat_big_num.num  (** Flags. *)
-  | Numeric   of Nat_big_num.num  (** An uninterpreted numeric value. *)
-  | Checksum  of Nat_big_num.num  (** A checksum value *)
-  | RelType   of rel_type (** A relocation entry type. *)
-  | Timestamp of Nat_big_num.num  (** A timestamp value. *)
-  | Null                  (** A null (0) value. *)
-  | Ignored               (** An ignored value. *)
-  
-(** [elf32_dyn_value] and [elf64_dyn_value] are specialisations of [dyn_value]
-  * fixing the correct types for the ['addr] and ['size] type variables.
-  *)
-type elf32_dyn_value = (Uint32.uint32, Uint32.uint32) dyn_value
-type elf64_dyn_value = (Uint64.uint64, Uint64.uint64) dyn_value
-
-(** [get_string_table_of_elf32_dyn_section endian dyns sht bs0] searches through
-  * dynamic section entries [dyns] looking for one pointing to a string table, looks
-  * up the corresponding section header [sht] pointed to by that dynamic
-  * section entry, finds the section in [bs0] and decodes a string table from that
-  * section assuming endianness [endian].  May fail.
-  *)
-(*val get_string_table_of_elf32_dyn_section : endianness -> list elf32_dyn ->
-  elf32_section_header_table -> byte_sequence -> error string_table*)
-let get_string_table_of_elf32_dyn_section endian dyns sht bs0:(string_table)error=  
- (let strtabs =    
-(List.filter (fun x -> Nat_big_num.equal      
-(Nat_big_num.of_int32 x.elf32_dyn_tag) ( dt_strtab)
-    ) dyns)
-  in
-    (match strtabs with
-      | [strtab] ->
-        (match strtab.elf32_dyn_d_un with
-          | D_Val     v -> fail "get_string_table_of_elf32_dyn_section: STRTAB must be a PTR"
-          | D_Ptr     p ->
-            let sect =              
-(List.filter (fun s ->                
-(s.elf32_sh_addr = p) &&                  
-(s.elf32_sh_type = Uint32.of_string (Nat_big_num.to_string sht_strtab))
-              ) sht)
-            in
-              (match sect with
-                | []  -> fail "get_string_table_of_elf32_dyn_section: no section entry with same address as STRTAB"
-                | [s] ->
-                  let off = (Nat_big_num.of_string (Uint32.to_string s.elf32_sh_offset)) in
-                  let siz = (Nat_big_num.of_string (Uint32.to_string s.elf32_sh_size)) in
-                  Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel ->
-                  let strings  = (Byte_sequence.string_of_byte_sequence rel) in
-                  return (String_table.mk_string_table strings (Missing_pervasives.null_char)))
-                | _   -> fail "get_string_table_of_elf32_dyn_section: multiple section entries with same address as STRTAB"
-              )
-          | D_Ignored i -> fail "get_string_table_of_elf32_dyn_section: STRTAB must be a PTR"
-        )
-      | []       -> fail "get_string_table_of_elf32_dyn_section: no string table entry"
-      | _        -> fail "get_string_table_of_elf32_dyn_section: multiple string table entries"
-    ))
-    
-(** [get_string_table_of_elf64_dyn_section endian dyns sht bs0] searches through
-  * dynamic section entries [dyns] looking for one pointing to a string table, looks
-  * up the corresponding section header [sht] pointed to by that dynamic
-  * section entry, finds the section in [bs0] and decodes a string table from that
-  * section assuming endianness [endian].  May fail.
-  *)
-(*val get_string_table_of_elf64_dyn_section : endianness -> list elf64_dyn ->
-  elf64_section_header_table -> byte_sequence -> error string_table*)
-let get_string_table_of_elf64_dyn_section endian dyns sht bs0:(string_table)error=  
- (let strtabs =    
-(List.filter (fun x -> Nat_big_num.equal      
-(Nat_big_num.of_int64 x.elf64_dyn_tag) ( dt_strtab)
-    ) dyns)
-  in
-    (match strtabs with
-      | [strtab] ->
-        (match strtab.elf64_dyn_d_un with
-          | D_Val     v -> fail "get_string_table_of_elf64_dyn_section: STRTAB must be a PTR"
-          | D_Ptr     p ->
-            let sect =              
-(List.filter (fun s ->                
-(s.elf64_sh_addr = p) &&                  
-(s.elf64_sh_type = Uint32.of_string (Nat_big_num.to_string sht_strtab))
-              ) sht)
-            in
-              (match sect with
-                | []  -> fail "get_string_table_of_elf64_dyn_section: no section entry with same address as STRTAB"
-                | [s] ->
-                  let off = (Nat_big_num.of_string (Uint64.to_string s.elf64_sh_offset)) in
-                  let siz = (Ml_bindings.nat_big_num_of_uint64 s.elf64_sh_size) in
-                  Byte_sequence.offset_and_cut off siz bs0 >>= (fun rel ->
-                  let strings  = (Byte_sequence.string_of_byte_sequence rel) in
-                  return (String_table.mk_string_table strings Missing_pervasives.null_char))
-                | _   -> fail "get_string_table_of_elf64_dyn_section: multiple section entries with same address as STRTAB"
-              )
-          | D_Ignored i -> fail "get_string_table_of_elf64_dyn_section: STRTAB must be a PTR"
-        )
-      | []       -> fail "get_string_table_of_elf64_dyn_section: no string table entry"
-      | _        -> fail "get_string_table_of_elf64_dyn_section: multiple string table entries"
-    ))
-    
-(** [get_value_of_elf32_dyn so dyn os_additional_ranges os proc stab] returns the value
-  * stored in a dynamic section entry [dyn], using [os_additional_ranges] and
-  * [os] to decode ABI-reserved tags.  String table [stab] is used to correctly
-  * decode library and run paths, etc.
-  * May fail.
-  *)
-(*val get_value_of_elf32_dyn : bool -> elf32_dyn -> (natural -> bool) ->
-  (elf32_dyn -> string_table -> error elf32_dyn_value) ->
-    (elf32_dyn -> string_table -> error elf32_dyn_value) ->
-    string_table -> error elf32_dyn_value*)
-let get_value_of_elf32_dyn shared_object dyn os_additional_ranges os proc stab:(((Uint32.uint32),(Uint32.uint32))dyn_value)error=  
- (let tag = (Nat_big_num.abs (Nat_big_num.of_int32 dyn.elf32_dyn_tag)) in
-    if Nat_big_num.equal tag dt_null then
-      return Null
-    else if Nat_big_num.equal tag dt_needed then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val v     -> return v
-        | D_Ptr p     -> fail "get_value_of_elf32_dyn_entry: NEEDED must be a Val"
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: NEEDED must be a Val"
-      ) >>= (fun off ->
-        let off = (Nat_big_num.of_string (Uint32.to_string off)) in
-        String_table.get_string_at off stab >>= (fun str ->
-        return (Library str)))
-    else if Nat_big_num.equal tag dt_pltrelsz then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf32_dyn_entry: PLTRELSZ must be a Val"
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: PLTRELSZ must be a Val"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_pltgot then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf32_dyn_entry: PLTGOT must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: PLTGOT must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_hash then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf32_dyn_entry: HASH must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: HASH must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_strtab then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf32_dyn_entry: STRTAB must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: STRTAB must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_symtab then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf32_dyn_entry: SYMTAB must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: SYMTAB must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_rela then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf32_dyn_entry: RELA must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RELA must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_relasz then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf32_dyn_entry: RELASZ must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RELASZ must be a VAL"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_relaent then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf32_dyn_entry: RELAENT must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RELAENT must be a VAL"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_strsz then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf32_dyn_entry: STRSZ must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: STRSZ must be a VAL"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_syment then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf32_dyn_entry: SYMENT must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: SYMENT must be a VAL"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_init then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf32_dyn_entry: INIT must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: INIT must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_fini then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf32_dyn_entry: FINI must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: FINI must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_soname then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val v     -> return v
-        | D_Ptr p     -> fail "get_value_of_elf32_dyn_entry: SONAME must be a Val"
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: SONAME must be a Val"
-      ) >>= (fun off ->
-        let off = (Nat_big_num.of_string (Uint32.to_string off)) in
-        String_table.get_string_at off stab >>= (fun str ->
-        return (SOName str)))
-    else if Nat_big_num.equal tag dt_rpath then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val v     -> return v
-        | D_Ptr p     -> fail "get_value_of_elf32_dyn_entry: RPATH must be a Val"
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RPATH must be a Val"
-      ) >>= (fun off ->
-        let off = (Nat_big_num.of_string (Uint32.to_string off)) in
-        String_table.get_string_at off stab >>= (fun str ->
-        return (RPath str)))
-    else if Nat_big_num.equal tag dt_symbolic then
-      return Null
-    else if Nat_big_num.equal tag dt_rel then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf32_dyn_entry: REL must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: REL must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_relsz then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf32_dyn_entry: RELSZ must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RELSZ must be a VAL"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_relent then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf32_dyn_entry: RELENT must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RELENT must be a VAL"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_pltrel then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf32_dyn_entry: PLTREL must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: PLTREL must be a VAL"
-      ) >>= (fun r ->
-        if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string r)) dt_rel then
-          return (RelType Rel)
-        else if Nat_big_num.equal (Nat_big_num.of_string (Uint32.to_string r)) dt_rela then
-          return (RelType RelA)
-        else
-          fail "get_value_of_elf32_dyn_entry: PLTREL neither REL nor RELA")
-    else if Nat_big_num.equal tag dt_debug then
-      return Null
-    else if Nat_big_num.equal tag dt_textrel then
-      return Null
-    else if Nat_big_num.equal tag dt_jmprel then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf32_dyn_entry: JMPREL must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: JMPREL must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_bindnow then
-      return Ignored
-    else if Nat_big_num.equal tag dt_init_array then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf32_dyn_entry: INIT_ARRAY must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: INIT_ARRAY must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_fini_array then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf32_dyn_entry: FINI_ARRAY must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: FINI_ARRAY must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_init_arraysz then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf32_dyn_entry: INIT_ARRAYSZ must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: INIT_ARRAYSZ must be a VAL"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_fini_arraysz then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf32_dyn_entry: FINI_ARRAYSZ must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: FINI_ARRAYSZ must be a VAL"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_runpath then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val v     -> return v
-        | D_Ptr p     -> fail "get_value_of_elf32_dyn_entry: RUNPATH must be a Val"
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: RUNPATH must be a Val"
-      ) >>= (fun off ->
-        let off = (Nat_big_num.of_string (Uint32.to_string off)) in
-        String_table.get_string_at off stab >>= (fun str ->
-        return (RunPath str)))
-    else if Nat_big_num.equal tag dt_flags then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val v     -> return v
-        | D_Ptr p     -> fail "get_value_of_elf32_dyn_entry: FLAGS must be a Val"
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: FLAGS must be a Val"
-      ) >>= (fun flags ->
-        return (Flags (Nat_big_num.of_string (Uint32.to_string flags))))
-    else if Nat_big_num.equal tag dt_encoding then
-      if not shared_object then
-        return Ignored
-      else
-        (match dyn.elf32_dyn_d_un with
-          | D_Val     v -> fail "get_value_of_elf32_dyn_entry: PREINIT_ARRAY must be a PTR"
-          | D_Ptr     p -> return p
-          | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: PREINIT_ARRAY must be a PTR"
-        ) >>= (fun ptr ->
-        return (Address ptr))
-    else if Nat_big_num.equal tag dt_preinit_arraysz then
-      (match dyn.elf32_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf32_dyn_entry: PREINIT_ARRAYSZ must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf32_dyn_entry: PREINIT_ARRAYSZ must be a VAL"
-      ) >>= (fun sz ->
-      return (Checksum (Nat_big_num.of_string (Uint32.to_string sz)))) (** XXX: bug in readelf does not print this as a size! *)
-    else if Nat_big_num.greater_equal tag dt_loproc && Nat_big_num.less_equal tag dt_hiproc then
-      proc dyn stab
-    else if Nat_big_num.greater_equal tag dt_loos && Nat_big_num.less_equal tag dt_hios then
-      os dyn stab
-    else if os_additional_ranges tag then
-      os dyn stab
-    else
-      fail "get_value_of_elf32_dyn: unrecognised tag type")
-      
-(** [get_value_of_elf64_dyn dyn os_additional_ranges os proc stab] returns the value
-  * stored in a dynamic section entry [dyn], using [os_additional_ranges] and
-  * [os] to decode ABI-reserved tags.  String table [stab] is used to correctly
-  * decode library and run paths, etc.
-  * May fail.
-  *)
-(*val get_value_of_elf64_dyn : bool -> elf64_dyn -> (natural -> bool) ->
-  (elf64_dyn -> string_table -> error elf64_dyn_value) ->
-    (elf64_dyn -> string_table -> error elf64_dyn_value) ->
-    string_table -> error elf64_dyn_value*)
-let get_value_of_elf64_dyn shared_object dyn os_additional_ranges os_dyn proc_dyn stab:(((Uint64.uint64),(Uint64.uint64))dyn_value)error=  
- (let tag = (Nat_big_num.abs (Nat_big_num.of_int64 dyn.elf64_dyn_tag)) in
-    if Nat_big_num.equal tag dt_null then
-      return Null
-    else if Nat_big_num.equal tag dt_needed then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val v     -> return v
-        | D_Ptr p     -> fail "get_value_of_elf64_dyn_entry: NEEDED must be a Val"
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: NEEDED must be a Val"
-      ) >>= (fun off ->
-        let off = (Ml_bindings.nat_big_num_of_uint64 off) in
-        String_table.get_string_at off stab >>= (fun str ->
-        return (Library str)))
-    else if Nat_big_num.equal tag dt_pltrelsz then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf64_dyn_entry: PLTRELSZ must be a Val"
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: PLTRELSZ must be a Val"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_pltgot then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf64_dyn_entry: PLTGOT must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: PLTGOT must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_hash then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf64_dyn_entry: HASH must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: HASH must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_strtab then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf64_dyn_entry: STRTAB must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: STRTAB must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_symtab then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf64_dyn_entry: SYMTAB must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: SYMTAB must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_rela then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf64_dyn_entry: RELA must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RELA must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_relasz then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf64_dyn_entry: RELASZ must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RELASZ must be a VAL"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_relaent then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf64_dyn_entry: RELAENT must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RELAENT must be a VAL"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_strsz then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf64_dyn_entry: STRSZ must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: STRSZ must be a VAL"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_syment then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf64_dyn_entry: SYMENT must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: SYMENT must be a VAL"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_init then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf64_dyn_entry: INIT must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: INIT must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_fini then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf64_dyn_entry: FINI must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: FINI must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_soname then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val v     -> return v
-        | D_Ptr p     -> fail "get_value_of_elf64_dyn_entry: SONAME must be a Val"
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: SONAME must be a Val"
-      ) >>= (fun off ->
-        let off = (Ml_bindings.nat_big_num_of_uint64 off) in
-        String_table.get_string_at off stab >>= (fun str ->
-        return (SOName str)))
-    else if Nat_big_num.equal tag dt_rpath then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val v     -> return v
-        | D_Ptr p     -> fail "get_value_of_elf64_dyn_entry: RPATH must be a Val"
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RPATH must be a Val"
-      ) >>= (fun off ->
-        let off = (Ml_bindings.nat_big_num_of_uint64 off) in
-        String_table.get_string_at off stab >>= (fun str ->
-        return (RPath str)))
-    else if Nat_big_num.equal tag dt_symbolic then
-      return Null
-    else if Nat_big_num.equal tag dt_rel then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf64_dyn_entry: REL must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: REL must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_relsz then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf64_dyn_entry: RELSZ must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RELSZ must be a VAL"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_relent then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf64_dyn_entry: RELENT must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RELENT must be a VAL"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_pltrel then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf64_dyn_entry: PLTREL must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: PLTREL must be a VAL"
-      ) >>= (fun r ->
-        if Nat_big_num.equal (Ml_bindings.nat_big_num_of_uint64 r) dt_rel then
-          return (RelType Rel)
-        else if Nat_big_num.equal (Ml_bindings.nat_big_num_of_uint64 r) dt_rela then
-          return (RelType RelA)
-        else
-          fail "get_value_of_elf64_dyn_entry: PLTREL neither REL nor RELA")
-    else if Nat_big_num.equal tag dt_debug then
-      return Null
-    else if Nat_big_num.equal tag dt_textrel then
-      return Null
-    else if Nat_big_num.equal tag dt_jmprel then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf64_dyn_entry: JMPREL must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: JMPREL must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_bindnow then
-      return Ignored
-    else if Nat_big_num.equal tag dt_init_array then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf64_dyn_entry: INIT_ARRAY must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: INIT_ARRAY must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_fini_array then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> fail "get_value_of_elf64_dyn_entry: FINI_ARRAY must be a PTR"
-        | D_Ptr     p -> return p
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: FINI_ARRAY must be a PTR"
-      ) >>= (fun ptr ->
-      return (Address ptr))
-    else if Nat_big_num.equal tag dt_init_arraysz then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf64_dyn_entry: INIT_ARRAYSZ must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: INIT_ARRAYSZ must be a VAL"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_fini_arraysz then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf64_dyn_entry: FINI_ARRAYSZ must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: FINI_ARRAYSZ must be a VAL"
-      ) >>= (fun sz ->
-      return (Size sz))
-    else if Nat_big_num.equal tag dt_runpath then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val v     -> return v
-        | D_Ptr p     -> fail "get_value_of_elf64_dyn_entry: RUNPATH must be a Val"
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: RUNPATH must be a Val"
-      ) >>= (fun off ->
-        let off = (Ml_bindings.nat_big_num_of_uint64 off) in
-        String_table.get_string_at off stab >>= (fun str ->
-        return (RunPath str)))
-    else if Nat_big_num.equal tag dt_flags then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val v     -> return v
-        | D_Ptr p     -> fail "get_value_of_elf64_dyn_entry: FLAGS must be a Val"
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: FLAGS must be a Val"
-      ) >>= (fun flags ->
-        return (Flags (Ml_bindings.nat_big_num_of_uint64 flags)))
-    else if Nat_big_num.equal tag dt_encoding then
-      if not shared_object then
-        return Ignored
-      else
-        (match dyn.elf64_dyn_d_un with
-          | D_Val     v -> fail "get_value_of_elf64_dyn_entry: PREINIT_ARRAY must be a PTR"
-          | D_Ptr     p -> return p
-          | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: PREINIT_ARRAY must be a PTR"
-        ) >>= (fun ptr ->
-        return (Address ptr))
-    else if Nat_big_num.equal tag dt_preinit_arraysz then
-      (match dyn.elf64_dyn_d_un with
-        | D_Val     v -> return v
-        | D_Ptr     p -> fail "get_value_of_elf64_dyn_entry: PREINIT_ARRAYSZ must be a VAL"
-        | D_Ignored i -> fail "get_value_of_elf64_dyn_entry: PREINIT_ARRAYSZ must be a VAL"
-      ) >>= (fun sz ->
-      return (Checksum (Ml_bindings.nat_big_num_of_uint64 sz))) (** XXX: bug in readelf does not print this as a size! *)
-    else if Nat_big_num.greater_equal tag dt_loproc && Nat_big_num.less_equal tag dt_hiproc then
-      proc_dyn dyn stab
-    else if Nat_big_num.greater_equal tag dt_loos && Nat_big_num.less_equal tag dt_hios then
-      os_dyn dyn stab
-    else if os_additional_ranges tag then
-      os_dyn dyn stab
-    else
-      fail "get_value_of_elf64_dyn: unrecognised tag type")