diff --git a/src/callMoCHi.ml b/src/callMoCHi.ml deleted file mode 100644 index e69de29b..00000000 diff --git a/src/consort.ml b/src/consort.ml index 28c8b5ca..7d06a88d 100644 --- a/src/consort.ml +++ b/src/consort.ml @@ -242,5 +242,8 @@ let convmochi ~opts file = ((function Some x -> x | None -> assert false) ownership_res) ast in - ConvMoCHi.Mochi.print_prog prog; + (* ConvMoCHi.Mochi.print_prog prog; *) + let file = open_out "./test/to_mochi.ml" in + ConvMoCHi.Mochi.write_to_channel_prog prog file; + Out_channel.close file; match ownership_res with None -> Unverified Aliasing | Some _ -> Verified diff --git a/src/convMoCHi.ml b/src/convMoCHi.ml index e970d8f0..cef56f90 100644 --- a/src/convMoCHi.ml +++ b/src/convMoCHi.ml @@ -265,6 +265,10 @@ module Mochi = struct let print_prog prog = print_endline builtin; pp_prog prog std_formatter + + let write_to_channel_prog prog file = + Printf.fprintf file "%s\n" builtin; + pp_prog prog (Format.formatter_of_out_channel file); end let pull_type ty con i = diff --git a/src/test/list/reverse2.imp b/src/test/list/reverse2.imp index d15e56db..adb79657 100644 --- a/src/test/list/reverse2.imp +++ b/src/test/list/reverse2.imp @@ -10,6 +10,7 @@ mklist(n) { _reverse(l, l_next) { match l_next with Nil -> { + // FIXME: this alias statement is (maybe) wrong // alias(*(l.Cons.2) = l_next); return l } @@ -51,4 +52,4 @@ len(l) { let len_l = len(l) in let rev_l = reverse(l) in assert(len_l = len(rev_l)) -} \ No newline at end of file +}