From 7241fa2584765f72bd014338f563fc7c852ea070 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 10 Apr 2024 14:18:40 +0200
Subject: [PATCH] [wp] clarifies fallback message
---
src/plugins/wp/Why3Provers.ml | 7 ++++---
src/plugins/wp/tests/wp_plugin/dune | 4 ++++
.../script/job_ensures.json | 1 +
src/plugins/wp/tests/wp_plugin/fallback.i | 10 ++++++----
.../wp/tests/wp_plugin/oracle/fallback.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/fallback.res.oracle | 14 ++++++++++----
6 files changed, 26 insertions(+), 12 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_plugin/fallback.0.session_qualif/script/job_ensures.json
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 276f4890834..2ff1dcf688f 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -139,8 +139,8 @@ let select ~name ?version () =
List.sort by_version @@ List.filter (filter ~name ?version) @@ provers ()
with p::_ -> Some p | [] -> None
-let lookup ?(fallback=false) name =
- match String.split_on_char ':' @@ String.lowercase_ascii name with
+let lookup ?(fallback=false) prover_name =
+ match String.split_on_char ':' @@ String.lowercase_ascii prover_name with
| [name] -> select ~name ()
| [name;version] ->
begin
@@ -152,7 +152,8 @@ let lookup ?(fallback=false) name =
| None -> None
| Some p as res ->
Wp_parameters.warning ~once:true
- "Prover %s not found, fallback to %s" name (ident_wp p) ; res
+ "Prover %s not found, fallback to %s" prover_name (ident_wp p) ;
+ res
else None
end
| _ -> None
diff --git a/src/plugins/wp/tests/wp_plugin/dune b/src/plugins/wp/tests/wp_plugin/dune
index 7323baff07f..77a700def17 100644
--- a/src/plugins/wp/tests/wp_plugin/dune
+++ b/src/plugins/wp/tests/wp_plugin/dune
@@ -2,6 +2,10 @@
result_qualif/bitmask0x8000.0.session_qualif/script
(copy_files ../../../bitmask0x8000.0.session_qualif/script/*))
+(subdir
+ result_qualif/fallback.0.session_qualif/script
+ (copy_files ../../../fallback.0.session_qualif/script/*))
+
(subdir
result_qualif/unroll.0.session_qualif/script
(copy_files ../../../unroll.0.session_qualif/script/*))
diff --git a/src/plugins/wp/tests/wp_plugin/fallback.0.session_qualif/script/job_ensures.json b/src/plugins/wp/tests/wp_plugin/fallback.0.session_qualif/script/job_ensures.json
new file mode 100644
index 00000000000..d180c4c3a1e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/fallback.0.session_qualif/script/job_ensures.json
@@ -0,0 +1 @@
+[ { "prover": "Alt-Ergo:1.2.0", "verdict": "timeout", "time": 2. } ]
diff --git a/src/plugins/wp/tests/wp_plugin/fallback.i b/src/plugins/wp/tests/wp_plugin/fallback.i
index dc9e3482885..8cdadf45897 100644
--- a/src/plugins/wp/tests/wp_plugin/fallback.i
+++ b/src/plugins/wp/tests/wp_plugin/fallback.i
@@ -1,7 +1,9 @@
/* run.config_qualif
- EXIT: 1
- OPT: -wp-prover=Alt-Ergo:1.2.0
+ DEPS: @PTEST_DEPS@ @WP_SESSION@/script/job_ensures.json
+ OPT: -wp-prover script @USING_WP_SESSION@
*/
-/*@ ensures \result == a * b ; */
-int job(int a,int b) { return (a - 1)*b + b ; }
+/*@ ensures \result <= 1000 ; */
+int job(int a,int b){
+ return (a - 1) * b + b ;
+}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle
index c31f09c80a4..80aa41bf36e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle
@@ -11,6 +11,6 @@
Goal Post-condition (file fallback.i, line 6) in 'job':
Let x = b + (b * (a - 1)).
Assume { Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(x). }
-Prove: (a * b) = x.
+Prove: x <= 1000.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
index 757ff0c0135..6f5e911d7ab 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
@@ -4,11 +4,17 @@
[wp] [Valid] Goal job_exits (Cfg) (Unreachable)
[wp] [Valid] Goal job_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
-[wp] User Error: Prover 'Alt-Ergo:1.2.0' not found in why3.conf
-[wp] Goal typed_job_ensures : not tried
+[wp] 1 goal scheduled
+[wp] :0: Warning: Prover Alt-Ergo:1.2.0 not found, fallback to Alt-Ergo:2.5.3
+[wp] [NoResult] typed_job_ensures (Qed)
+[wp] Proved goals: 2 / 3
+ Terminating: 1
+ Unreachable: 1
+ Unsuccess: 1
+ Missing: 1
+[wp] Session can be updated
+ - 1 script unused (now automated)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job - - 1 0.0%
------------------------------------------------------------
-[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
-[kernel] Plug-in wp aborted: invalid user input.
--
GitLab