From 85496e45e0b89ae2c8693a3331f970e6b90ab4e6 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Tue, 25 Jun 2024 19:09:09 +0200
Subject: [PATCH] [test] Updated AIMOS and SAVER prover answer to match Why3
1.7 prover output
---
src/aimos.ml | 9 ++++++---
src/saver.ml | 4 ++--
2 files changed, 8 insertions(+), 5 deletions(-)
diff --git a/src/aimos.ml b/src/aimos.ml
index a74f2a2..1cec3ca 100644
--- a/src/aimos.ml
+++ b/src/aimos.ml
@@ -23,6 +23,7 @@
open Why3
open Base
+let src = Logs.Src.create "AIMOS" ~doc:"AIMOS verifier"
let re_aimos_file = Re__Core.(compile (str "%{aimos_file}"))
let write_config inputs_path models_path perturbation perturbation_path out_mode
@@ -109,7 +110,7 @@ let build_answer predicate_kind prover_result =
| _ -> failwith "Unsupported property"
in
match prover_result.Call_provers.pr_answer with
- | Call_provers.HighFailure -> (
+ | Call_provers.Unknown _ -> (
let pr_output = prover_result.pr_output in
match Re__Core.exec_opt re_aimos_output pr_output with
| Some re_group ->
@@ -126,10 +127,12 @@ let build_answer predicate_kind prover_result =
in
prover_answer
| None -> failwith "Cannot interpret the output provided by AIMOS")
- | _ ->
+ | unexpected_pr_answer ->
(* Any other answer than HighFailure should never happen as we do not define
anything in AIMOS's driver. *)
- assert false
+ Logging.code_error ~src (fun m ->
+ m "Unexpected AIMOS prover answer '%a'"
+ Why3.Call_provers.print_prover_answer unexpected_pr_answer)
let call_prover limit config config_prover
(predicate : (Language.nn_shape, string) Dataset.predicate) =
diff --git a/src/saver.ml b/src/saver.ml
index 2aef858..09cf70d 100644
--- a/src/saver.ml
+++ b/src/saver.ml
@@ -105,7 +105,7 @@ let negative_answer = function
let build_answer_on_dataset_predicate predicate_kind prover_result =
match prover_result.Call_provers.pr_answer with
- | Call_provers.HighFailure -> (
+ | Call_provers.Unknown _ -> (
let pr_output = prover_result.pr_output in
match Re__Core.exec_opt re_saver_output pr_output with
| Some re_group ->
@@ -165,7 +165,7 @@ let call_prover_on_dataset_predicate limit config config_prover predicate =
let build_answer prover_result =
match prover_result.Call_provers.pr_answer with
- | Call_provers.HighFailure -> (
+ | Call_provers.Unknown _ -> (
let pr_output = prover_result.pr_output in
match Re__Core.exec_opt re_saver_output pr_output with
| Some re_group ->
--
GitLab