Modified ocaml backend to use ocamlfind for linksem and lem

Fixed test cases for ocaml backend and interpreter

1 files changed, 0 insertions, 196 deletions

diff --git a/lib/ocaml_rts/linksem/elf_note.ml b/lib/ocaml_rts/linksem/elf_note.ml
deleted file mode 100644
index f9965d68..00000000
--- a/lib/ocaml_rts/linksem/elf_note.ml
+++ /dev/null
@@ -1,196 +0,0 @@
-(*Generated by Lem from elf_note.lem.*)
-(** [elf_note] contains data types and functions for interpreting the .note
-  * section/segment of an ELF file, and extracting information from that
-  * section/segment.
-  *)
-
-open Lem_basic_classes
-open Lem_list
-open Lem_num
-open Lem_string
-
-open Byte_sequence
-open Endianness
-open Error
-open Missing_pervasives
-open Show
-
-open Elf_program_header_table
-open Elf_section_header_table
-open Elf_types_native_uint
-
-(** [elf32_note] represents the contents of a .note section or segment.
-  *)
-type elf32_note =
-  { elf32_note_namesz : Uint32.uint32 (** The size of the name field. *)
-   ; elf32_note_descsz : Uint32.uint32 (** The size of the description field. *)
-   ; elf32_note_type   : Uint32.uint32 (** The type of the note. *)
-   ; elf32_note_name   : char list  (** The list of bytes (of length indicated above) corresponding to the name string. *)
-   ; elf32_note_desc   : char list  (** The list of bytes (of length indicated above) corresponding to the desc string. *)
-   }
-   
-(** [elf64_note] represents the contents of a .note section or segment.
-  *)
-type elf64_note =
-  { elf64_note_namesz : Uint64.uint64 (** The size of the name field. *)
-   ; elf64_note_descsz : Uint64.uint64 (** The size of the description field. *)
-   ; elf64_note_type   : Uint64.uint64 (** The type of the note. *)
-   ; elf64_note_name   : char list   (** The list of bytes (of length indicated above) corresponding to the name string. *)
-   ; elf64_note_desc   : char list   (** The list of bytes (of length indicated above) corresponding to the desc string. *)
-   }
-   
-(** [read_elf32_note endian bs0] transcribes an ELF note section from byte
-  * sequence [bs0] assuming endianness [endian].  May fail if transcription fails
-  * (i.e. if the byte sequence is not sufficiently long).
-  *)
-(*val read_elf32_note : endianness -> byte_sequence -> error (elf32_note * byte_sequence)*)
-let read_elf32_note endian bs0:(elf32_note*byte_sequence)error=  
- (read_elf32_word endian bs0 >>= (fun (namesz, bs0) ->
-  read_elf32_word endian bs0 >>= (fun (descsz, bs0) ->
-  read_elf32_word endian bs0 >>= (fun (typ, bs0) ->
-  repeatM' (Nat_big_num.of_string (Uint32.to_string namesz)) bs0 read_char >>= (fun (name1, bs0) ->
-  repeatM' (Nat_big_num.of_string (Uint32.to_string descsz)) bs0 read_char >>= (fun (desc, bs0) ->
-  return ({ elf32_note_namesz = namesz; elf32_note_descsz = descsz;
-    elf32_note_type = typ; elf32_note_name = name1; elf32_note_desc = desc },
-      bs0)))))))
-      
-(** [read_elf64_note endian bs0] transcribes an ELF note section from byte
-  * sequence [bs0] assuming endianness [endian].  May fail if transcription fails
-  * (i.e. if the byte sequence is not sufficiently long).
-  *)
-(*val read_elf64_note : endianness -> byte_sequence -> error (elf64_note * byte_sequence)*)
-let read_elf64_note endian bs0:(elf64_note*byte_sequence)error=  
- (read_elf64_xword endian bs0 >>= (fun (namesz, bs0) ->
-  read_elf64_xword endian bs0 >>= (fun (descsz, bs0) ->
-  read_elf64_xword endian bs0 >>= (fun (typ, bs0) ->
-  repeatM' (Ml_bindings.nat_big_num_of_uint64 namesz) bs0 read_char >>= (fun (name1, bs0) ->
-  repeatM' (Ml_bindings.nat_big_num_of_uint64 descsz) bs0 read_char >>= (fun (desc, bs0) ->
-  return ({ elf64_note_namesz = namesz; elf64_note_descsz = descsz;
-    elf64_note_type = typ; elf64_note_name = name1; elf64_note_desc = desc },
-      bs0)))))))
-      
-(** [obtain_elf32_note_sections endian sht bs0] returns all note sections present
-  * in an ELF file, as indicated by the file's section header table [sht], reading
-  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
-  * transcription of a note section fails.
-  *)
-(*val obtain_elf32_note_sections : endianness -> elf32_section_header_table ->
-  byte_sequence -> error (list elf32_note)*)
-let obtain_elf32_note_sections endian sht bs0:((elf32_note)list)error=  
- (let note_sects =    
-(List.filter (fun x ->
-      x.elf32_sh_type = Uint32.of_string (Nat_big_num.to_string sht_note)
-    ) sht)
-  in
-    mapM (fun x ->
-      let offset = (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_offset)) in
-      let size2   = (Nat_big_num.of_string (Uint32.to_string x.elf32_sh_size)) in
-      Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun rel ->
-      read_elf32_note endian rel >>= (fun (note, _) ->
-      return note))
-    ) note_sects)
-    
-(** [obtain_elf64_note_sections endian sht bs0] returns all note sections present
-  * in an ELF file, as indicated by the file's section header table [sht], reading
-  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
-  * transcription of a note section fails.
-  *)
-(*val obtain_elf64_note_sections : endianness -> elf64_section_header_table ->
-  byte_sequence -> error (list elf64_note)*)
-let obtain_elf64_note_sections endian sht bs0:((elf64_note)list)error=  
- (let note_sects =    
-(List.filter (fun x ->
-      x.elf64_sh_type = Uint32.of_string (Nat_big_num.to_string sht_note)
-    ) sht)
-  in
-    mapM (fun x ->
-      let offset = (Nat_big_num.of_string (Uint64.to_string x.elf64_sh_offset)) in
-      let size2   = (Ml_bindings.nat_big_num_of_uint64 x.elf64_sh_size) in
-      Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun rel ->
-      read_elf64_note endian rel >>= (fun (note, _) ->
-      return note))
-    ) note_sects)
-    
-(** [obtain_elf32_note_segments endian pht bs0] returns all note segments present
-  * in an ELF file, as indicated by the file's program header table [pht], reading
-  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
-  * transcription of a note section fails.
-  *)
-(*val obtain_elf32_note_segments : endianness -> elf32_program_header_table ->
-  byte_sequence -> error (list elf32_note)*)
-let obtain_elf32_note_segments endian pht bs0:((elf32_note)list)error=  
- (let note_segs =    
-(List.filter (fun x ->
-      x.elf32_p_type = Uint32.of_string (Nat_big_num.to_string elf_pt_note)
-    ) pht)
-  in
-    mapM (fun x ->
-      let offset = (Nat_big_num.of_string (Uint32.to_string x.elf32_p_offset)) in
-      let size2   = (Nat_big_num.of_string (Uint32.to_string x.elf32_p_filesz)) in
-      Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun rel ->
-      read_elf32_note endian rel >>= (fun (note, _) ->
-      return note))
-    ) note_segs)
-    
-(** [obtain_elf64_note_segments endian pht bs0] returns all note segments present
-  * in an ELF file, as indicated by the file's program header table [pht], reading
-  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
-  * transcription of a note section fails.
-  *)
-(*val obtain_elf64_note_segments : endianness -> elf64_program_header_table ->
-  byte_sequence -> error (list elf64_note)*)
-let obtain_elf64_note_segments endian pht bs0:((elf64_note)list)error=  
- (let note_segs =    
-(List.filter (fun x ->
-      x.elf64_p_type = Uint32.of_string (Nat_big_num.to_string elf_pt_note)
-    ) pht)
-  in
-    mapM (fun x ->
-      let offset = (Nat_big_num.of_string (Uint64.to_string x.elf64_p_offset)) in
-      let size2   = (Ml_bindings.nat_big_num_of_uint64 x.elf64_p_filesz) in
-      Byte_sequence.offset_and_cut offset size2 bs0 >>= (fun rel ->
-      read_elf64_note endian rel >>= (fun (note, _) ->
-      return note))
-    ) note_segs)
-    
-(** [obtain_elf32_note_section_and_segments endian pht sht bs0] returns all note
-  * sections and segments present in an ELF file, as indicated by the file's
-  * program header table [pht] and section header table [sht], reading
-  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
-  * transcription of a note section or segment fails.
-  *)
-(*val obtain_elf32_note_section_and_segments : endianness -> elf32_program_header_table ->
-  elf32_section_header_table -> byte_sequence -> error (list elf32_note)*)
-let obtain_elf32_note_section_and_segments endian pht sht bs0:((elf32_note)list)error=  
- (obtain_elf32_note_segments endian pht bs0 >>= (fun pht_notes ->
-  obtain_elf32_note_sections endian sht bs0 >>= (fun sht_notes ->
-  return ( List.rev_append (List.rev pht_notes) sht_notes))))
-  
-(** [obtain_elf64_note_section_and_segments endian pht sht bs0] returns all note
-  * sections and segments present in an ELF file, as indicated by the file's
-  * program header table [pht] and section header table [sht], reading
-  * them from byte sequence [bs0] assuming endianness [endian].  May fail if
-  * transcription of a note section or segment fails.
-  *)
-(*val obtain_elf64_note_section_and_segments : endianness -> elf64_program_header_table ->
-  elf64_section_header_table -> byte_sequence -> error (list elf64_note)*)
-let obtain_elf64_note_section_and_segments endian pht sht bs0:((elf64_note)list)error=  
- (obtain_elf64_note_segments endian pht bs0 >>= (fun pht_notes ->
-  obtain_elf64_note_sections endian sht bs0 >>= (fun sht_notes ->
-  return ( List.rev_append (List.rev pht_notes) sht_notes))))
-    
-(** [name_string_of_elf32_note note] extracts the name string of an ELF note
-  * section, interpreting the section's uninterpreted name field as a string.
-  *)
-(*val name_string_of_elf32_note : elf32_note -> string*)
-let name_string_of_elf32_note note:string=  
- (let bs0   = (Byte_sequence.from_byte_lists [note.elf32_note_name]) in
-    Byte_sequence.string_of_byte_sequence bs0)
-  
-(** [name_string_of_elf64_note note] extracts the name string of an ELF note
-  * section, interpreting the section's uninterpreted name field as a string.
-  *)  
-(*val name_string_of_elf64_note : elf64_note -> string*)
-let name_string_of_elf64_note note:string=  
- (let bs0   = (Byte_sequence.from_byte_lists [note.elf64_note_name]) in
-    Byte_sequence.string_of_byte_sequence bs0)