From 694d9564b63f34bde6102f978b2f62c69967a8b8 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 5 Jan 2022 13:59:21 +0100
Subject: [PATCH] [wp] Update qualif oracles and remove drivers
---
src/plugins/wp/tests/wp_acsl/classify_float.c | 1 -
.../oracle_qualif/classify_float.1.res.oracle | 15 +++--
.../oracle_qualif/classify_float.2.res.oracle | 15 ++---
.../oracle_qualif/classify_float.3.res.oracle | 13 ----
src/plugins/wp/tests/wp_plugin/abs.driver | 1 -
src/plugins/wp/tests/wp_plugin/abs.i | 1 -
src/plugins/wp/tests/wp_plugin/convert.i | 1 -
.../wp/tests/wp_plugin/flash-ergo.driver | 2 -
src/plugins/wp/tests/wp_plugin/flash.c | 10 +--
src/plugins/wp/tests/wp_plugin/flash.driver | 6 +-
src/plugins/wp/tests/wp_plugin/flash.mlw | 13 ----
src/plugins/wp/tests/wp_plugin/float_format.i | 1 -
src/plugins/wp/tests/wp_plugin/math.i | 8 +--
.../wp_plugin/oracle_qualif/abs.2.res.oracle | 14 -----
.../oracle_qualif/convert.1.res.oracle | 18 ------
...onvert.0.res.oracle => convert.res.oracle} | 0
.../oracle_qualif/flash.1.res.oracle | 18 +++---
.../oracle_qualif/flash.2.res.oracle | 17 ------
.../oracle_qualif/float_format.0.res.oracle | 2 +-
.../oracle_qualif/float_format.1.res.oracle | 7 +--
.../oracle_qualif/float_format.2.res.oracle | 15 -----
.../wp_plugin/oracle_qualif/math.1.res.oracle | 61 +++++--------------
.../wp_plugin/oracle_qualif/math.2.res.oracle | 20 ------
.../wp_plugin/oracle_qualif/math.3.res.oracle | 25 --------
24 files changed, 49 insertions(+), 235 deletions(-)
delete mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_plugin/flash-ergo.driver
delete mode 100644 src/plugins/wp/tests/wp_plugin/flash.mlw
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
rename src/plugins/wp/tests/wp_plugin/oracle_qualif/{convert.0.res.oracle => convert.res.oracle} (100%)
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
diff --git a/src/plugins/wp/tests/wp_acsl/classify_float.c b/src/plugins/wp/tests/wp_acsl/classify_float.c
index 8c4932391e6..9a1e8e74b42 100644
--- a/src/plugins/wp/tests/wp_acsl/classify_float.c
+++ b/src/plugins/wp/tests/wp_acsl/classify_float.c
@@ -1,6 +1,5 @@
/* run.config_qualif
OPT: -wp-prover alt-ergo
- OPT: -wp-prover native:alt-ergo
OPT: -wp-prover native:coq -wp-coq-script %{dep:@PTEST_DIR@/classify_float.script}
OPT: -wp-model real
*/
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
index efbf0e0a5e9..8d89bf6103e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
@@ -1,14 +1,17 @@
# frama-c -wp [...]
[kernel] Parsing classify_float.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
+[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 3 goals scheduled
-[wp] [Alt-Ergo (native)] Goal typed_lemma_InfN_not_finite : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_InfP_not_finite : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_NaN_not_finite : Valid
+[wp] [Coq] Goal typed_lemma_InfN_not_finite : Saved script
+[wp] [Coq (native)] Goal typed_lemma_InfN_not_finite : Valid
+[wp] [Coq] Goal typed_lemma_InfP_not_finite : Saved script
+[wp] [Coq (native)] Goal typed_lemma_InfP_not_finite : Valid
+[wp] [Coq] Goal typed_lemma_NaN_not_finite : Saved script
+[wp] [Coq (native)] Goal typed_lemma_NaN_not_finite : Valid
[wp] Proved goals: 3 / 3
- Qed: 0
- Alt-Ergo (native): 3
+ Qed: 0
+ Coq (native): 3
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Lemma - - 3 100%
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle
index 8d89bf6103e..286b26bfd54 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle
@@ -1,18 +1,13 @@
# frama-c -wp [...]
[kernel] Parsing classify_float.c (with preprocessing)
[wp] Running WP plugin...
-[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 3 goals scheduled
-[wp] [Coq] Goal typed_lemma_InfN_not_finite : Saved script
-[wp] [Coq (native)] Goal typed_lemma_InfN_not_finite : Valid
-[wp] [Coq] Goal typed_lemma_InfP_not_finite : Saved script
-[wp] [Coq (native)] Goal typed_lemma_InfP_not_finite : Valid
-[wp] [Coq] Goal typed_lemma_NaN_not_finite : Saved script
-[wp] [Coq (native)] Goal typed_lemma_NaN_not_finite : Valid
+[wp] [Qed] Goal typed_real_lemma_InfN_not_finite : Valid
+[wp] [Qed] Goal typed_real_lemma_InfP_not_finite : Valid
+[wp] [Qed] Goal typed_real_lemma_NaN_not_finite : Valid
[wp] Proved goals: 3 / 3
- Qed: 0
- Coq (native): 3
+ Qed: 3
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
- Lemma - - 3 100%
+ Lemma 3 - 3 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle
deleted file mode 100644
index d56892bed73..00000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle
+++ /dev/null
@@ -1,13 +0,0 @@
-# frama-c -wp -wp-model 'Typed (Real)' [...]
-[kernel] Parsing classify_float.c (with preprocessing)
-[wp] Running WP plugin...
-[wp] 3 goals scheduled
-[wp] [Qed] Goal typed_real_lemma_InfN_not_finite : Valid
-[wp] [Qed] Goal typed_real_lemma_InfP_not_finite : Valid
-[wp] [Qed] Goal typed_real_lemma_NaN_not_finite : Valid
-[wp] Proved goals: 3 / 3
- Qed: 3
-------------------------------------------------------------
- Axiomatics WP Alt-Ergo Total Success
- Lemma 3 - 3 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/abs.driver b/src/plugins/wp/tests/wp_plugin/abs.driver
index 97bcd60eadc..691ecd65e6a 100644
--- a/src/plugins/wp/tests/wp_plugin/abs.driver
+++ b/src/plugins/wp/tests/wp_plugin/abs.driver
@@ -2,5 +2,4 @@ library "abs":
logic integer ABS (integer) = "my_abs" ;
coq.file := "Abs.v";
-altergo.file := "abs.mlw";
why3.file := "abs.why";
diff --git a/src/plugins/wp/tests/wp_plugin/abs.i b/src/plugins/wp/tests/wp_plugin/abs.i
index 321483c54b8..2992f8953e5 100644
--- a/src/plugins/wp/tests/wp_plugin/abs.i
+++ b/src/plugins/wp/tests/wp_plugin/abs.i
@@ -8,7 +8,6 @@
DEPS: abs.why abs.mlw abs.script Abs.v
OPT: -wp -wp-driver %{dep:@PTEST_DIR@/abs.driver} -wp-prover alt-ergo
OPT: -wp -wp-driver %{dep:@PTEST_DIR@/abs.driver} -wp-prover native:coq -wp-coq-script %{dep:@PTEST_DIR@/abs.script}
- OPT: -wp -wp-driver %{dep:@PTEST_DIR@/abs.driver} -wp-prover native:alt-ergo
*/
/*@ axiomatic Absolute { logic integer ABS(integer x) ; } */
diff --git a/src/plugins/wp/tests/wp_plugin/convert.i b/src/plugins/wp/tests/wp_plugin/convert.i
index 2dce3a46225..c1cd5e0b31e 100644
--- a/src/plugins/wp/tests/wp_plugin/convert.i
+++ b/src/plugins/wp/tests/wp_plugin/convert.i
@@ -4,7 +4,6 @@
/* run.config_qualif
OPT:
- OPT: -wp-prover native:alt-ergo -wp-report=%{dep:@PTEST_SUITE_DIR@/../native.report}
*/
// --------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/flash-ergo.driver b/src/plugins/wp/tests/wp_plugin/flash-ergo.driver
deleted file mode 100644
index 3a0caaa7b5a..00000000000
--- a/src/plugins/wp/tests/wp_plugin/flash-ergo.driver
+++ /dev/null
@@ -1,2 +0,0 @@
-library INDEX: const
-logic index INDEX_init = {coq="dumb"; altergo="const(0)"; why3="Flash.init"; } ;
diff --git a/src/plugins/wp/tests/wp_plugin/flash.c b/src/plugins/wp/tests/wp_plugin/flash.c
index 957b7a67755..f289baa8d10 100644
--- a/src/plugins/wp/tests/wp_plugin/flash.c
+++ b/src/plugins/wp/tests/wp_plugin/flash.c
@@ -1,15 +1,11 @@
/* run.config
OPT:
- DEPS: flash.mlw
- OPT: -wp-driver %{dep:@PTEST_DIR@/flash.driver},%{dep:@PTEST_DIR@/flash-ergo.driver}
SCRIPT: flash
OPT: -wp-driver %{dep:@PTEST_DIR@/flash.driver}
*/
/* run.config_qualif
OPT: -wp-timeout 1
- DEPS: flash.mlw
- OPT: -wp-driver %{dep:@PTEST_DIR@/flash.driver},%{dep:@PTEST_DIR@/flash-ergo.driver}
SCRIPT: @PTEST_NAME@
OPT: -wp-driver %{dep:@PTEST_DIR@/flash.driver}
*/
@@ -22,7 +18,7 @@ SCRIPT: @PTEST_NAME@
/*@
axiomatic EVENT {
- type event =
+ type event =
| RdAt_int(int *)
| WrAt_int(int *)
;
@@ -47,7 +43,7 @@ SCRIPT: @PTEST_NAME@
//@ghost int RD_time ;
-/*@
+/*@
axiomatic RD {
logic index RD_current{L} reads RD_time;
logic index RD_update( index idx , int *p ) reads \nothing;
@@ -73,7 +69,7 @@ int RD(int *p);
//@ ghost int WR_time ;
-/*@
+/*@
axiomatic WR {
logic index WR_current{L} reads WR_time;
logic index WR_update( index idx , int *p ) reads \nothing;
diff --git a/src/plugins/wp/tests/wp_plugin/flash.driver b/src/plugins/wp/tests/wp_plugin/flash.driver
index 9196ec9571a..90ab84348e0 100644
--- a/src/plugins/wp/tests/wp_plugin/flash.driver
+++ b/src/plugins/wp/tests/wp_plugin/flash.driver
@@ -1,8 +1,8 @@
library INDEX: memory
why3.file += "flash.mlw";
-type index = {coq="dumb"; altergo="(addr,int)farray"; why3="Flash.t"; } ;
-logic integer INDEX_access( index , addr ) = {coq="dumb"; altergo="(%1)[%2]"; why3="Flash.get"; } ;
-logic index INDEX_update( index , addr ) = {coq="dumb"; altergo="((%1)[(%2) <- (%1)[%2]+1])"; why3="Flash.update"};
+type index = {coq="dumb"; why3="Flash.t"; } ;
+logic integer INDEX_access( index , addr ) = {coq="dumb"; why3="Flash.get"; } ;
+logic index INDEX_update( index , addr ) = {coq="dumb"; why3="Flash.update"};
logic index INDEX_init := "INDEX_init" ;
library RD: INDEX
diff --git a/src/plugins/wp/tests/wp_plugin/flash.mlw b/src/plugins/wp/tests/wp_plugin/flash.mlw
deleted file mode 100644
index 2d8a45bfb6c..00000000000
--- a/src/plugins/wp/tests/wp_plugin/flash.mlw
+++ /dev/null
@@ -1,13 +0,0 @@
-module Flash
- use map.Map
- use map.Const
- use int.Int
- use frama_c_wp.memory.Memory
-
- type t = map addr int
-
- function get (m:t) (x:addr) : int = m[x]
- function update (m:t) (x:addr) : t = m[ x <- (m[x] + 1) ]
-
- function init : t = const 0
-end
diff --git a/src/plugins/wp/tests/wp_plugin/float_format.i b/src/plugins/wp/tests/wp_plugin/float_format.i
index cdca1c6d758..1aedc8151c7 100644
--- a/src/plugins/wp/tests/wp_plugin/float_format.i
+++ b/src/plugins/wp/tests/wp_plugin/float_format.i
@@ -1,6 +1,5 @@
/* run.config_qualif
OPT: -wp-prover native:coq
- OPT: -wp-prover native:alt-ergo -wp-steps 5 -wp-timeout 100
OPT: -wp-prover alt-ergo -wp-steps 5 -wp-timeout 100
*/
diff --git a/src/plugins/wp/tests/wp_plugin/math.i b/src/plugins/wp/tests/wp_plugin/math.i
index d2a3d2ce303..53a3106b4c5 100644
--- a/src/plugins/wp/tests/wp_plugin/math.i
+++ b/src/plugins/wp/tests/wp_plugin/math.i
@@ -3,10 +3,8 @@
*/
/* run.config_qualif
- OPT: -wp-prover alt-ergo -wp-prop=-ko -wp-timeout 100 -wp-steps 1500
- OPT: -wp-prover native:alt-ergo -wp-report=%{dep:@PTEST_SUITE_DIR@/../native.report} -wp-prop=-ko -wp-timeout 100 -wp-steps 1500
- OPT: -wp-prover alt-ergo -wp-prop=ko -wp-timeout 100 -wp-steps 10
- OPT: -wp-prover native:alt-ergo -wp-report=%{dep:@PTEST_SUITE_DIR@/../native.report} -wp-prop=ko -wp-timeout 100 -wp-steps 10
+ OPT: -wp-prover alt-ergo -wp-prop=-ko -wp-timeout 100 -wp-steps 1500
+ OPT: -wp-prover alt-ergo -wp-prop=ko -wp-timeout 100 -wp-steps 10
*/
// --------------------------------------------------------------------------
@@ -63,7 +61,7 @@
// --- Polar
// --------------------------------------------------------------------------
-//@ lemma distance: \forall real x,y; \hypot(x,y) == \sqrt( x*x + y*y );
+//@ lemma distance: \forall real x,y; \hypot(x,y) == \sqrt( x*x + y*y );
// --------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
deleted file mode 100644
index 34c366ca1cf..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
+++ /dev/null
@@ -1,14 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing abs.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
-[wp] 1 goal scheduled
-[wp] [Alt-Ergo (native)] Goal typed_abs_abs_ensures : Valid
-[wp] Proved goals: 1 / 1
- Qed: 0
- Alt-Ergo (native): 1
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- abs - - 1 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
deleted file mode 100644
index 7bd9172a019..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
+++ /dev/null
@@ -1,18 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing convert.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
-[wp] 2 goals scheduled
-[wp] [Alt-Ergo (native)] Goal typed_lemma_ceil : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_floor : Valid
-[wp] Proved goals: 2 / 2
- Qed: 0
- Alt-Ergo (native): 2
-------------------------------------------------------------
- Axiomatics WP Alt-Ergo Total Success
- Lemma - - 2 100%
-------------------------------------------------------------
--------------------------------------------------------------
-Axiomatics WP Alt-Ergo (Native) Total Success
-Lemma - 2 2 100%
--------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.res.oracle
similarity index 100%
rename from src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle
rename to src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.res.oracle
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle
index 8419319f579..09997a7fac3 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle
@@ -1,19 +1,17 @@
# frama-c -wp [...]
[kernel] Parsing flash.c (with preprocessing)
[wp] Running WP plugin...
-[wp] flash-ergo.driver:2: Warning: Redefinition of logic INDEX_init
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
-[wp] [Qed] Goal typed_flash_flash-ergo_job_ensures_Events : Valid
-[wp] [Alt-Ergo] Goal typed_flash_flash-ergo_job_ensures_A_reads : Valid
-[wp] [Alt-Ergo] Goal typed_flash_flash-ergo_job_ensures_B_reads : Valid
-[wp] [Alt-Ergo] Goal typed_flash_flash-ergo_job_ensures_B_writes : Valid
-[wp] [Alt-Ergo] Goal typed_flash_flash-ergo_job_ensures_ReadValues : Valid
-[wp] [Alt-Ergo] Goal typed_flash_flash-ergo_job_ensures_WriteValues : Valid
+[wp] [Qed] Goal typed_flash_job_ensures_Events : Valid
+[wp] [Qed] Goal typed_flash_job_ensures_A_reads : Valid
+[wp] [Qed] Goal typed_flash_job_ensures_B_reads : Valid
+[wp] [Qed] Goal typed_flash_job_ensures_B_writes : Valid
+[wp] [Qed] Goal typed_flash_job_ensures_ReadValues : Valid
+[wp] [Qed] Goal typed_flash_job_ensures_WriteValues : Valid
[wp] Proved goals: 6 / 6
- Qed: 1
- Alt-Ergo: 5
+ Qed: 6
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- job 1 5 6 100%
+ job 6 - 6 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle
deleted file mode 100644
index 09997a7fac3..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle
+++ /dev/null
@@ -1,17 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing flash.c (with preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] 6 goals scheduled
-[wp] [Qed] Goal typed_flash_job_ensures_Events : Valid
-[wp] [Qed] Goal typed_flash_job_ensures_A_reads : Valid
-[wp] [Qed] Goal typed_flash_job_ensures_B_reads : Valid
-[wp] [Qed] Goal typed_flash_job_ensures_B_writes : Valid
-[wp] [Qed] Goal typed_flash_job_ensures_ReadValues : Valid
-[wp] [Qed] Goal typed_flash_job_ensures_WriteValues : Valid
-[wp] Proved goals: 6 / 6
- Qed: 6
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- job 6 - 6 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
index 035a7253a87..d27cc13ed05 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
@@ -1,6 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing float_format.i (no preprocessing)
-[kernel:parser:decimal-float] float_format.i:10: Warning:
+[kernel:parser:decimal-float] float_format.i:9: Warning:
Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[wp] Running WP plugin...
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
index 0b38dce72ac..484b4e1bb0e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
@@ -1,15 +1,14 @@
# frama-c -wp -wp-timeout 100 -wp-steps 5 [...]
[kernel] Parsing float_format.i (no preprocessing)
-[kernel:parser:decimal-float] float_format.i:10: Warning:
+[kernel:parser:decimal-float] float_format.i:9: Warning:
Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
[wp] 1 goal scheduled
-[wp] [Alt-Ergo (native)] Goal typed_output_ensures_KO : Unsuccess
+[wp] [Alt-Ergo] Goal typed_output_ensures_KO : Unsuccess
[wp] Proved goals: 0 / 1
- Alt-Ergo (native): 0 (unsuccess: 1)
+ Alt-Ergo: 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
output - - 1 0.0%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
deleted file mode 100644
index 876b56b73ef..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
+++ /dev/null
@@ -1,15 +0,0 @@
-# frama-c -wp -wp-timeout 100 -wp-steps 5 [...]
-[kernel] Parsing float_format.i (no preprocessing)
-[kernel:parser:decimal-float] float_format.i:10: Warning:
- Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
- (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] 1 goal scheduled
-[wp] [Alt-Ergo] Goal typed_output_ensures_KO : Unsuccess
-[wp] Proved goals: 0 / 1
- Alt-Ergo: 0 (unsuccess: 1)
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- output - - 1 0.0%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
index 773a5245836..69ac94a8689 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
@@ -1,53 +1,20 @@
-# frama-c -wp -wp-timeout 100 -wp-steps 1500 [...]
+# frama-c -wp -wp-timeout 100 -wp-steps 10 [...]
[kernel] Parsing math.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
-[wp] 30 goals scheduled
-[wp] [Alt-Ergo (native)] Goal typed_lemma_abs_neg : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_abs_pos : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_atan_sin_cos : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_cosh_opp : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_distance : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_exp_log_add_mul : Valid
-[wp] [Qed] Goal typed_lemma_exp_pos : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_log_exp_mul_add : Valid
-[wp] [Qed] Goal typed_lemma_max_ac : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_max_inf : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_max_or : Valid
-[wp] [Qed] Goal typed_lemma_min_ac : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_min_inf : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_min_or : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_pow_2 : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_sinh_opp : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_sqrt_mono : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_sqrt_pos : Valid
-[wp] [Alt-Ergo (native)] Goal typed_lemma_tanh_opp : Valid
-[wp] [Alt-Ergo (native)] Goal typed_ok_ensures_sin_asin : Valid
-[wp] [Alt-Ergo (native)] Goal typed_ok_ensures_sin_asin_in_range : Valid
-[wp] [Alt-Ergo (native)] Goal typed_ok_ensures_cos_acos : Valid
-[wp] [Alt-Ergo (native)] Goal typed_ok_ensures_cos_acos_in_range : Valid
-[wp] [Qed] Goal typed_ok_ensures_tan_atan : Valid
-[wp] [Alt-Ergo (native)] Goal typed_ok_ensures_log_pow : Valid
-[wp] [Qed] Goal typed_ok_ensures_log_exp : Valid
-[wp] [Alt-Ergo (native)] Goal typed_ok_ensures_exp_log : Valid
-[wp] [Alt-Ergo (native)] Goal typed_ok_ensures_min_plus_distrib : Valid
-[wp] [Alt-Ergo (native)] Goal typed_ok_ensures_sqrt_pos : Valid
-[wp] [Alt-Ergo (native)] Goal typed_ok_ensures_sqrt_pos0 : Valid
-[wp] Proved goals: 30 / 30
- Qed: 5
- Alt-Ergo (native): 25
-------------------------------------------------------------
- Axiomatics WP Alt-Ergo Total Success
- Lemma 3 - 19 100%
+[wp] 9 goals scheduled
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_sin_asin : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_cos_acos : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_asin_sin : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_acos_cos : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_atan_tan : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_log_pow : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_exp_log : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_exp_log_add_mul : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_sqrt_pos : Unsuccess
+[wp] Proved goals: 0 / 9
+ Alt-Ergo: 0 (unsuccess: 9)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- ok 2 - 11 100%
+ ko - - 9 0.0%
------------------------------------------------------------
--------------------------------------------------------------
-Axiomatics WP Alt-Ergo (Native) Total Success
-Lemma 3 16 19 100%
--------------------------------------------------------------
-Functions WP Alt-Ergo (Native) Total Success
-ok 2 9 11 100%
--------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle
deleted file mode 100644
index 69ac94a8689..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle
+++ /dev/null
@@ -1,20 +0,0 @@
-# frama-c -wp -wp-timeout 100 -wp-steps 10 [...]
-[kernel] Parsing math.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] 9 goals scheduled
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_sin_asin : Unsuccess
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_cos_acos : Unsuccess
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_asin_sin : Unsuccess
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_acos_cos : Unsuccess
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_atan_tan : Unsuccess
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_log_pow : Unsuccess
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_exp_log : Unsuccess
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_exp_log_add_mul : Unsuccess
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_sqrt_pos : Unsuccess
-[wp] Proved goals: 0 / 9
- Alt-Ergo: 0 (unsuccess: 9)
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- ko - - 9 0.0%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
deleted file mode 100644
index d0872807ed5..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
+++ /dev/null
@@ -1,25 +0,0 @@
-# frama-c -wp -wp-timeout 100 -wp-steps 10 [...]
-[kernel] Parsing math.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
-[wp] 9 goals scheduled
-[wp] [Alt-Ergo (native)] Goal typed_ko_ensures_ko_sin_asin : Unsuccess
-[wp] [Alt-Ergo (native)] Goal typed_ko_ensures_ko_cos_acos : Unsuccess
-[wp] [Alt-Ergo (native)] Goal typed_ko_ensures_ko_asin_sin : Unsuccess
-[wp] [Alt-Ergo (native)] Goal typed_ko_ensures_ko_acos_cos : Unsuccess
-[wp] [Alt-Ergo (native)] Goal typed_ko_ensures_ko_atan_tan : Unsuccess
-[wp] [Alt-Ergo (native)] Goal typed_ko_ensures_ko_log_pow : Unsuccess
-[wp] [Alt-Ergo (native)] Goal typed_ko_ensures_ko_exp_log : Unsuccess
-[wp] [Alt-Ergo (native)] Goal typed_ko_ensures_ko_exp_log_add_mul : Unsuccess
-[wp] [Alt-Ergo (native)] Goal typed_ko_ensures_ko_sqrt_pos : Unsuccess
-[wp] Proved goals: 0 / 9
- Alt-Ergo (native): 0 (unsuccess: 9)
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- ko - - 9 0.0%
-------------------------------------------------------------
--------------------------------------------------------------
-Functions WP Alt-Ergo (Native) Total Success
-ko - - 9 0.0%
--------------------------------------------------------------
--
GitLab