Modified ocaml backend to use ocamlfind for linksem and lem

Fixed test cases for ocaml backend and interpreter

1 files changed, 0 insertions, 150 deletions

diff --git a/lib/ocaml_rts/linksem/archive.ml b/lib/ocaml_rts/linksem/archive.ml
deleted file mode 100644
index cd4480b4..00000000
--- a/lib/ocaml_rts/linksem/archive.ml
+++ /dev/null
@@ -1,150 +0,0 @@
-(*Generated by Lem from archive.lem.*)
-open Lem_basic_classes
-open Lem_bool
-open Lem_list
-open Lem_num
-open Lem_maybe
-open Lem_string
-open Show
-open Lem_assert_extra
-
-open Missing_pervasives
-open Byte_sequence
-open Error
-
-type archive_entry_header =
-  { name      : string
-   ; timestamp : Nat_big_num.num
-   ; uid       : int
-   ; gid       : int
-   ; mode      : int
-   ; size      : int (* 1GB should be enough *)
-   }
-
-type archive_global_header = char
-  list
-
-(*val string_of_byte_sequence : byte_sequence -> string*)
-let string_of_byte_sequence0 seq:string=  
- ((match seq with
-    | Sequence bs -> Xstring.implode (Lem_list.map (fun x-> x) bs)
-  ))
-
-(*val read_archive_entry_header : natural -> byte_sequence -> error (archive_entry_header * natural * byte_sequence)*)
-let read_archive_entry_header seq_length seq:(archive_entry_header*Nat_big_num.num*byte_sequence)error=  
- (let magic_bytes = ([Char.chr (Nat_big_num.to_int (Nat_big_num.of_int 96)) (* 0x60 *); Char.chr (Nat_big_num.to_int (Nat_big_num.of_int 10)) (* 0x0a *)]) in
-        let header_length =(Nat_big_num.of_int 60) in
-        (* let _ = Missing_pervasives.errs ("Archive entry header? " ^ (show (take 16 bs)) ^ "? ") in *)
-        partition_with_length header_length seq_length seq >>= (fun (header, rest) -> 
-        offset_and_cut(Nat_big_num.of_int 58)(Nat_big_num.of_int 2) header >>= (fun magic -> 
-        offset_and_cut(Nat_big_num.of_int 0)(Nat_big_num.of_int 16) header >>= (fun name1 -> 
-        offset_and_cut(Nat_big_num.of_int 16)(Nat_big_num.of_int 12) header >>= (fun timestamp_str -> 
-        offset_and_cut(Nat_big_num.of_int 28)(Nat_big_num.of_int 6)  header >>= (fun uid_str -> 
-        offset_and_cut(Nat_big_num.of_int 34)(Nat_big_num.of_int 6)  header >>= (fun gid_str -> 
-        offset_and_cut(Nat_big_num.of_int 40)(Nat_big_num.of_int 8)  header >>= (fun mode_str -> 
-        offset_and_cut(Nat_big_num.of_int 48)(Nat_big_num.of_int 10) header >>= (fun size_str -> 
-        let size2 = (natural_of_decimal_string (string_of_byte_sequence0 size_str)) in 
-                (* let _ = Missing_pervasives.errln (": yes, size " ^ (show size)) in *)
-        return ({ name = (string_of_byte_sequence0 name1); timestamp = ((Nat_big_num.of_int 0 : Nat_big_num.num)) (* FIXME *);
-          uid =( 0) (* FIXME *) ; gid =( 0) (* FIXME *) ; mode =( 0) (* FIXME *);
-            size = (Nat_big_num.to_int size2) (* FIXME *) }, Nat_big_num.sub_nat seq_length header_length, rest))))))))))
-
-(*val read_archive_global_header : byte_sequence -> error (archive_global_header * byte_sequence)*)
-let read_archive_global_header seq:((char)list*byte_sequence)error=  
- ((match seq with
-    | Sequence bs ->
-            (* let _ = Missing_pervasives.errs ("Archive? " ^ (show (take 16 bs)) ^ "? ")
-            in*)
-      let chars = (Lem_list.map (fun x-> x) (take0(Nat_big_num.of_int 8) bs)) in 
-        if Xstring.implode chars = "!<arch>\n" then
-          (* let _ = Missing_pervasives.errln ": yes" in *)
-          return (chars, Sequence(drop0(Nat_big_num.of_int 8) bs))
-        else
-          (* let _ = Missing_pervasives.errln ": no" in *)
-          fail "read_archive_global_header: not an archive"
-    ))
-
-(*val accum_archive_contents : (list (string * byte_sequence)) -> maybe string -> natural -> byte_sequence -> error (list (string * byte_sequence))*)
-let rec accum_archive_contents accum extended_filenames whole_seq_length whole_seq:((string*byte_sequence)list)error=  
-(  
-  (* let _ = Missing_pervasives.errs "Can read a header? " in *)if not (Nat_big_num.equal (Byte_sequence.length0 whole_seq) whole_seq_length) then    
-(assert false) (* invariant: whole_seq_length always equal to length of whole_seq, so the length is only
-      computed one.  This "fail" needed for Isabelle termination proofs... *)
-  else
-  (match (read_archive_entry_header whole_seq_length whole_seq) with
-    | Fail _ -> return accum
-    | Success (hdr, (seq_length : Nat_big_num.num), seq) ->
-    (match seq with
-      | Sequence next_bs ->
-        (* let _ = Missing_pervasives.errln ("yes; next_bs has length " ^ (show (List.length next_bs))) in *)
-        let amount_to_drop =          
-(if (hdr.size mod  2) = 0 then
-            (Nat_big_num.of_int hdr.size)
-          else Nat_big_num.add
-            (Nat_big_num.of_int hdr.size)(Nat_big_num.of_int 1))
-        in
-        if Nat_big_num.equal amount_to_drop(Nat_big_num.of_int 0) then
-          fail "accum_archive_contents: amount to drop from byte sequence is 0"
-        else
-        (*let _ = Missing_pervasives.errln ("amount_to_drop is " ^ (show amount_to_drop)) in*)
-        let chunk = (Sequence(Lem_list.take hdr.size next_bs))
-        in
-        (*let _ = Missing_pervasives.errs ("Processing archive header named " ^ hdr.name)
-        in*)
-        let (new_accum, (new_extended_filenames :  string option)) =          
-(let name1 = (Xstring.explode hdr.name) in
-            if (listEqualBy (=) name1 ['/'; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' '; ' ']) then
-              (* SystemV symbol lookup table; we skip this *) (accum, extended_filenames)
-            else
-              (match name1 with
-                | x::xs ->
-                  if x = '/' then
-                    (match xs with
-                      | y::ys ->
-                        if y = '/' then
-                          (accum, Some (string_of_byte_sequence0 chunk))
-                        else
-                          let index = (natural_of_decimal_string (Xstring.implode xs)) in
-                            (match extended_filenames with 
-                              | None -> failwith "corrupt archive: reference to non-existent extended filenames"
-                              | Some s -> 
-                                let table_suffix = ((match Ml_bindings.string_suffix index s with Some x -> x | None -> "" )) in
-                                let index = ((match Ml_bindings.string_index_of '/' table_suffix with Some x -> x | None -> (Nat_big_num.of_int (String.length table_suffix)) )) in 
-                                let ext_name = ((match Ml_bindings.string_prefix index table_suffix with Some x -> x | None -> "" )) in
-                                  (*let _ = Missing_pervasives.errln ("Got ext_name " ^ ext_name) in*)
-                                  (((ext_name, chunk) :: accum), extended_filenames)
-                           )
-                      | [] ->
-                        let index = (natural_of_decimal_string (Xstring.implode xs)) in
-                          (match extended_filenames with 
-                            | None -> failwith "corrupt archive: reference to non-existent extended filenames"
-                            | Some s -> 
-                              let table_suffix = ((match Ml_bindings.string_suffix index s with Some x -> x | None -> "" )) in
-                              let index = ((match Ml_bindings.string_index_of '/' table_suffix with Some x -> x | None -> (Nat_big_num.of_int (String.length table_suffix)) )) in 
-                              let ext_name = ((match Ml_bindings.string_prefix index table_suffix with Some x -> x | None -> "" )) in
-                                (*let _ = Missing_pervasives.errln ("Got ext_name " ^ ext_name) in*)
-                                (((ext_name, chunk) :: accum), extended_filenames)
-                         )
-                    )
-                  else
-                    (((hdr.name, chunk) :: accum), extended_filenames)
-                | [] -> (((hdr.name, chunk) :: accum), extended_filenames)
-              ))
-        in
-          (match (Byte_sequence.dropbytes amount_to_drop seq) with
-            | Fail _ -> return accum
-            | Success new_seq ->
-              accum_archive_contents new_accum new_extended_filenames ( Nat_big_num.sub_nat seq_length amount_to_drop) new_seq
-          )
-    )
-  ))
-
-(*val read_archive : byte_sequence -> error (list (string * byte_sequence))*)
-let read_archive bs:((string*byte_sequence)list)error=    
-  (read_archive_global_header bs >>= (fun (hdr, seq) -> 
-    let result = (accum_archive_contents [] None (Byte_sequence.length0 seq) seq)  in 
-    (* let _ = Missing_pervasives.errln "Finished reading archive" in *)
-    (match result with
-        Success r -> Success (List.rev r)
-        | Fail x -> Fail x
-    )))