From 0ba086f46e6552d868e4d843ae113d19e8a0894c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 11 Apr 2024 20:13:21 +0200
Subject: [PATCH] [wp] fix fallback test
---
src/plugins/wp/Why3Provers.ml | 2 +-
.../fallback.0.session_qualif/script/job_ensures.json | 2 +-
src/plugins/wp/tests/wp_plugin/fallback.i | 4 ++--
.../wp/tests/wp_plugin/oracle/fallback.res.oracle | 2 +-
.../tests/wp_plugin/oracle_qualif/fallback.res.oracle | 11 +++++------
5 files changed, 10 insertions(+), 11 deletions(-)
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 2ff1dcf688f..204a593d6d3 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -151,7 +151,7 @@ let lookup ?(fallback=false) prover_name =
match select ~name () with
| None -> None
| Some p as res ->
- Wp_parameters.warning ~once:true
+ Wp_parameters.warning ~once:true ~current:false
"Prover %s not found, fallback to %s" prover_name (ident_wp p) ;
res
else None
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
index d180c4c3a1e..2f92c64659e 100644
--- 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
@@ -1 +1 @@
-[ { "prover": "Alt-Ergo:1.2.0", "verdict": "timeout", "time": 2. } ]
+[ { "prover": "Alt-Ergo:1.2.0", "verdict": "valid", "time": 0.1 } ]
diff --git a/src/plugins/wp/tests/wp_plugin/fallback.i b/src/plugins/wp/tests/wp_plugin/fallback.i
index 8cdadf45897..b4ec19b80df 100644
--- a/src/plugins/wp/tests/wp_plugin/fallback.i
+++ b/src/plugins/wp/tests/wp_plugin/fallback.i
@@ -1,9 +1,9 @@
/* run.config_qualif
DEPS: @PTEST_DEPS@ @WP_SESSION@/script/job_ensures.json
- OPT: -wp-prover script @USING_WP_SESSION@
+ OPT: -wp-prover script,alt-ergo @USING_WP_SESSION@
*/
-/*@ ensures \result <= 1000 ; */
+/*@ ensures \result == a * b ; */
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 80aa41bf36e..c31f09c80a4 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: x <= 1000.
+Prove: (a * b) = x.
------------------------------------------------------------
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 6f5e911d7ab..6c923007a18 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
@@ -5,16 +5,15 @@
[wp] [Valid] Goal job_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[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
+[wp] Warning: Prover Alt-Ergo:1.2.0 not found, fallback to Alt-Ergo:2.5.3
+[wp] [Valid] typed_job_ensures (Alt-Ergo) (Cached)
+[wp] Proved goals: 3 / 3
Terminating: 1
Unreachable: 1
- Unsuccess: 1
- Missing: 1
+ Alt-Ergo: 1
[wp] Session can be updated
- 1 script unused (now automated)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- job - - 1 0.0%
+ job - 1 1 100%
------------------------------------------------------------
--
GitLab