From 130d1ec1eb80cf6ad45b92a05866a08fa07b5cb7 Mon Sep 17 00:00:00 2001 From: artoy Date: Thu, 21 Mar 2024 15:51:59 +0900 Subject: [PATCH] call mochi --- src/callMoCHi.ml | 6 ------ src/consort.ml | 3 --- src/dune | 2 +- 3 files changed, 1 insertion(+), 10 deletions(-) delete mode 100644 src/callMoCHi.ml diff --git a/src/callMoCHi.ml b/src/callMoCHi.ml deleted file mode 100644 index 57a9a00e..00000000 --- a/src/callMoCHi.ml +++ /dev/null @@ -1,6 +0,0 @@ -let call_mochi = - let cmd = "~/git/MoCHi/src/mochi.exe ./test/to_mochi.ml" in - let p = Process.spawn cmd in - let res = (String.trim @@ input_line p.Process.proc_stdout, String.trim @@ input_line p.Process.proc_stderr) in - Process.dispose p; - res \ No newline at end of file diff --git a/src/consort.ml b/src/consort.ml index 6b13ee30..7d06a88d 100644 --- a/src/consort.ml +++ b/src/consort.ml @@ -246,7 +246,4 @@ let convmochi ~opts file = let file = open_out "./test/to_mochi.ml" in ConvMoCHi.Mochi.write_to_channel_prog prog file; Out_channel.close file; - (* let (res_out, res_err) = CallMoCHi.call_mochi in - print_endline res_out; - print_endline res_err; *) match ownership_res with None -> Unverified Aliasing | Some _ -> Verified diff --git a/src/dune b/src/dune index 32fa851f..bb8c9fa4 100644 --- a/src/dune +++ b/src/dune @@ -44,7 +44,7 @@ Z3BasedBackend Consort HoiceBackend NullSolver ExternalFileBackend EldaricaBackend ParallelBackend - ConvMoCHi CallMoCHi)) + ConvMoCHi)) (executable (name test)