diff --git a/src/main.ml b/src/main.ml
index 53efcc8fd38cba1b0c77f26e4d48713125c7d326..68d86548191017ec3e8a397b43e2451e9cd2f327 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -71,7 +71,7 @@ let log_level_is_debug () =
let config detect () =
if detect
then (
- Logs.debug (fun m -> m "Automatic detection.");
+ Logs.debug (fun m -> m "Automatic detection");
let config =
let debug = log_level_is_debug () in
Autodetect.autodetection ~debug ()
@@ -95,7 +95,7 @@ let verify format loadpath memlimit timeout prover dataset_csv files =
files
let exec_cmd cmdname cmd =
- Logs.debug (fun m -> m "Command `%s'." cmdname);
+ Logs.debug (fun m -> m "Command `%s'" cmdname);
cmd ()
(* -- Command line. *)
@@ -165,10 +165,9 @@ let verify_cmd =
let all_provers = Prover.list_available () in
let doc =
Fmt.str
- "Prover to use. Support is provided for the following provers: %s."
- (Fmt.str "%a"
- (Fmt.list ~sep:Fmt.comma Fmt.string)
- (List.map ~f:Prover.to_string all_provers))
+ "Prover to use. Support is provided for the following provers: %a."
+ (Fmt.list ~sep:Fmt.comma Fmt.string)
+ (List.map ~f:Prover.to_string all_provers)
in
let provers =
Arg.enum (List.map ~f:(fun p -> (Prover.to_string p, p)) all_provers)
@@ -215,9 +214,18 @@ let default_info =
let default_cmd = Term.(ret (const (fun _ -> `Help (`Pager, None)) $ const ()))
+let () =
+ (* We register custom printers for a selection of exceptions otherwise Why3
+ will print the related messages as "anomaly: <exception with message>". *)
+ Why3.Exn_printer.register (fun fmt exn ->
+ match exn with
+ | Invalid_argument msg -> Fmt.pf fmt "Invalid argument: %s" msg
+ | Failure msg -> Fmt.pf fmt "Failure: %s" msg
+ | _ -> raise exn)
+
let () =
try
Cmd.group ~default:default_cmd default_info [ config_cmd; verify_cmd ]
|> Cmd.eval ~catch:false |> Caml.exit
with exn when not (log_level_is_debug ()) ->
- Fmt.epr "%a@." Why3.Exn_printer.exn_printer exn
+ Logs.err (fun m -> m "@[%a@]" Why3.Exn_printer.exn_printer exn)
diff --git a/src/verification.ml b/src/verification.ml
index 3139df410cb82ebb58e6f4fccaccee73eaec09e9..18931fdb719e04ba3f0b0d843ddd98ea7b097251 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -77,7 +77,7 @@ let answer_saver limit config task env prover dataset_csv =
let handle_task_saver task env dataset_csv command =
let dataset_filename =
match dataset_csv with
- | None -> failwith "Error, no dataset provided for SAVer."
+ | None -> invalid_arg "No dataset provided for SAVer"
| Some s -> s
in
let goal = Task.task_goal_fmla task in
@@ -104,13 +104,14 @@ let answer_saver limit config task env prover dataset_csv =
let svm_filename =
match Language.lookup_loaded_svms svm_app_sym with
| Some t -> t.filename
- | None -> failwith "SVM file not found in environment."
+ | None -> invalid_arg "No SVM model found in task"
in
(eps, svm_filename)
- else failwith "Wrong predicate found."
- (* no other predicate than robust_to is supported *)
- | _ -> failwith "Unsupported by SAVer.")
- | _ -> failwith "Unsupported by SAVer."
+ else failwith "Wrong predicate found"
+ | _ ->
+ (* no other predicate than robust_to is supported *)
+ failwith "Unsupported predicate by SAVer")
+ | _ -> failwith "Unsupported predicate by SAVer"
in
let svm_file = Unix.realpath svm_filename in
let dataset_file = Unix.realpath dataset_filename in
@@ -175,7 +176,7 @@ let answer_generic limit config task driver (prover : Whyconf.config_prover) =
match Task.on_meta_excl Native_nn_prover.meta_nn_filename task_prepared with
| Some [ MAstr nn_file ] -> nn_file
| Some _ -> assert false (* By construction of the meta. *)
- | None -> invalid_arg (Fmt.str "No neural network model found in task")
+ | None -> invalid_arg "No neural network model found in task"
in
let nn_file = Unix.realpath nn_file in
let command = Re__Core.replace_string nnet_or_onnx ~by:nn_file command in
@@ -198,8 +199,9 @@ let call_prover ~limit config (prover : Whyconf.config_prover) driver env
then answer_saver limit config task env prover dataset_csv
else answer_generic limit config task driver prover
in
- Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
- Call_provers.print_prover_answer prover_answer
+ Logs.app (fun m ->
+ m "@[Goal %a:@ %a@]" Pretty.print_pr (Task.task_goal task)
+ Call_provers.print_prover_answer prover_answer)
let verify ?(debug = false) format loadpath ?memlimit ?timeout prover
?dataset_csv file =
diff --git a/tests/autodetect.t b/tests/autodetect.t
index ff2c0b385985bd913d27889c8dd577bbfd4f1dd1..f184ddd6e2a9b06703e6b5b08f590555805411c1 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -21,8 +21,8 @@ Test autodetect
$ PATH=$(pwd)/bin:$PATH
$ caisar config -d -vv 2>&1 | ./filter_tmpdir.sh
- [caisar][DEBUG] Command `config'.
- [caisar][DEBUG] Automatic detection.
+ [caisar][DEBUG] Command `config'
+ [caisar][DEBUG] Automatic detection
<autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
<autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
diff --git a/tests/marabou.t b/tests/marabou.t
index d0e071ce568abe5d1cffba5f1b5ad25d1aee89bf..7379622e4bc5f10d156e130443f0b868bf4f66cc 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -34,7 +34,5 @@ Test verify
> ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
> end
> EOF
- Goal G: Unknown
- ()
- Goal H: Unknown
- ()
+ [caisar] Goal G: Unknown ()
+ [caisar] Goal H: Unknown ()
diff --git a/tests/simple.t b/tests/simple.t
index 8bc9aa3f18f4e52272066cb5ef738f36baee17d9..e908b61d8fa8eda7d2c269e9f335586750c070ad 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -37,7 +37,5 @@ Test verify
> ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
> end
> EOF
- Goal G: Unknown
- ()
- Goal H: Unknown
- ()
+ [caisar] Goal G: Unknown ()
+ [caisar] Goal H: Unknown ()
diff --git a/tests/simple_onnx.t b/tests/simple_onnx.t
index 90e92776592749fd819ced349420f7f209202b8a..30d2d720a3c7850e6ef9267d9e733472f66f1683 100644
--- a/tests/simple_onnx.t
+++ b/tests/simple_onnx.t
@@ -29,5 +29,4 @@ Test verify
> (0.0:t) .< y1 .< (0.5:t)
> end
> EOF
- Goal G: Unknown
- ()
+ [caisar] Goal G: Unknown ()
diff --git a/tests/simple_ovo.t b/tests/simple_ovo.t
index 2561471424f309a88e24e8b976d50f9f1989951e..34a460815ce62de6965ca880ee0d908c055336a1 100644
--- a/tests/simple_ovo.t
+++ b/tests/simple_ovo.t
@@ -34,4 +34,4 @@ Test verify
> goal G: forall a : input_type. robust_to svm_apply a (8.0:t)
> end
> EOF
- Goal G: High failure
+ [caisar] Goal G: High failure