Properly check veriT exit code and warnings (#48)

* Report veriT warnings

5 files changed, 17 insertions, 9 deletions

diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 2fd7d2d..57fd0cc 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -166,7 +166,7 @@ let export out_channel rt ro lsmt =
 
   Format.fprintf fmt "(check-sat)\n(exit)@."
 
-exception Non_empty_warnings
+exception Unknown
 
 let call_verit _ rt ro ra' rf' first lsmt =
   let (filename, outchan) = Filename.open_temp_file "verit_coq" ".smt2" in
@@ -184,21 +184,25 @@ let call_verit _ rt ro ra' rf' first lsmt =
 
   let win = open_in wname in
 
-  let assert_empty_warnings () =
-    try let _ = input_line win in raise Non_empty_warnings
+  let raise_warnings () =
+    try
+      while true do
+        let l = input_line win in
+        if l = "warning : proof_done: status is still open" then
+          raise Unknown
+        else
+          Structures.warning "verit-warning" ("Verit.call_verit: command " ^ command ^ " outputs the warning: " ^ l);
+      done
     with End_of_file -> () in
 
   try
-    assert (exit_code = 0);
-    assert_empty_warnings ();
+    if exit_code <> 0 then Structures.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code);
+    raise_warnings ();
     let res = import_trace ra' rf' logfilename (Some first) lsmt in
     close_in win; Sys.remove wname; res
   with x -> close_in win; Sys.remove wname;
             match x with
-            | Assert_failure _ ->
-                failwith ("Verit.call_verit: command " ^ command ^
-	                    " exited with code " ^ string_of_int exit_code)
-            | Non_empty_warnings -> Structures.error "veriT returns 'unknown'"
+            | Unknown -> Structures.error "veriT returns 'unknown'"
             | VeritSyntax.Sat -> Structures.error "veriT found a counter-example"
             | _ -> raise x
 
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index ee4bf96..94d68c1 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -168,6 +168,7 @@ let set_evars_tac _ = Tacticals.tclIDTAC
 (* Other differences between the two versions of Coq *)
 type constr_expr = Topconstr.constr_expr
 let error = Errors.error
+let warning _ s = Pp.warning s
 let extern_constr = Constrextern.extern_constr true Environ.empty_env
 let destruct_rel_decl (n, _, t) = n, t
 let interp_constr env sigma = Constrintern.interp_constr sigma env
diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli
index 939ffc7..775f7be 100644
--- a/src/versions/native/structures.mli
+++ b/src/versions/native/structures.mli
@@ -106,6 +106,7 @@ val set_evars_tac : 'a -> Proof_type.tactic
 (* Other differences between the two versions of Coq *)
 type constr_expr = Topconstr.constr_expr
 val error : string -> 'a
+val warning : string -> string -> unit
 val extern_constr : constr -> Topconstr.constr_expr
 val destruct_rel_decl : Term.rel_declaration -> name * types
 val interp_constr : Environ.env -> Evd.evar_map -> Topconstr.constr_expr -> constr
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index ea35a35..d7e7f96 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -205,6 +205,7 @@ let set_evars_tac noc =
 (* Other differences between the two versions of Coq *)
 type constr_expr = Constrexpr.constr_expr
 let error s = CErrors.user_err (Pp.str s)
+let warning n s = CWarnings.create ~name:n ~category:"SMTCoq plugin" Pp.str s
 
 let extern_constr c = Constrextern.extern_constr true Environ.empty_env Evd.empty (EConstr.of_constr c)
 
diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli
index 3aa8b3b..cde4f4f 100644
--- a/src/versions/standard/structures.mli
+++ b/src/versions/standard/structures.mli
@@ -109,6 +109,7 @@ val set_evars_tac : constr -> tactic
 (* Other differences between the two versions of Coq *)
 type constr_expr = Constrexpr.constr_expr
 val error : string -> 'a
+val warning : string -> string -> unit
 val extern_constr : constr -> constr_expr
 val destruct_rel_decl : (constr, types) Context.Rel.Declaration.pt -> name * types
 val interp_constr : Environ.env -> Evd.evar_map -> constr_expr -> constr