diff --git a/src/plugins/wp/tests/wp_acsl/classify_float.c b/src/plugins/wp/tests/wp_acsl/classify_float.c
index 8c4932391e6248f70ca55fb5d29ae2b59cb0d332..9a1e8e74b4239aaf28bc2497cf0659cea9b6027f 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 efbf0e0a5e995775beccb153f9ac586f1301faaf..8d89bf6103e89d700c551ea565d3cd4a814e3d35 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 8d89bf6103e89d700c551ea565d3cd4a814e3d35..286b26bfd5491319fddcef10db56cffae1838565 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 d56892bed73e2320f69ba98f7d23a947f7420d22..0000000000000000000000000000000000000000
--- 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 97bcd60eadc035dc88e07d7176196f32c897b3c0..691ecd65e6a56e4e30c9201e273e2bbd6707b9f8 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 321483c54b8ade7cb3782870de9e9a5cc49b0445..2992f8953e5d03a9fdfb65808d32cb82476ae185 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 2dce3a4622568c9e1a54a0b8e00ecf5d4b4301a6..c1cd5e0b31ebd6d52ad1a7a358b05d820fae632c 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 3a0caaa7b5aa77e404741f3fb27e0d8bd0f47609..0000000000000000000000000000000000000000
--- 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 957b7a677555f5350e219743644a4507973b389b..f289baa8d10249b415dec0f9db6673c39c77b7de 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 9196ec9571aacbb4e95249cd9e79a57184b829bb..90ab84348e0d05df1b59ba21f7ba9390c958c512 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 2d8a45bfb6c52f340992c99113318b4df4c8aba0..0000000000000000000000000000000000000000
--- 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 cdca1c6d758b266bfcef3b4a3727f19a234f8500..1aedc8151c7a89d30e89588646ac46f5db65d229 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 d2a3d2ce303de8ef3b5c4f48ce0bcfa4b426570a..53a3106b4c5a605686807ae0bf937daa3a0c65db 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 34c366ca1cffba4cf705fc0c994faccac7529d81..0000000000000000000000000000000000000000
--- 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 7bd9172a0194f3c00e9b0a7735d563aa01a970fd..0000000000000000000000000000000000000000
--- 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 8419319f579d41c559a2b1a06ca94882a297dbeb..09997a7fac3dfc41bd52eb294988b1d2bdc12825 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 09997a7fac3dfc41bd52eb294988b1d2bdc12825..0000000000000000000000000000000000000000
--- 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 035a7253a8796855be87d1e57b2c7182febefb46..d27cc13ed05839d0ddf88a3ed38c7c36ef17cf66 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 0b38dce72acbbe0166038cebb9c17e7bb744cfdb..484b4e1bb0ef8cfe1c9cffa2b0a8a4aa599c97a0 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 876b56b73ef0f3a6041262e3113ca6d40502a1f5..0000000000000000000000000000000000000000
--- 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 773a5245836281bda1c4734cac463b776176e985..69ac94a86894ed67b60991613cedc80023e2b4ad 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 69ac94a86894ed67b60991613cedc80023e2b4ad..0000000000000000000000000000000000000000
--- 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 d0872807ed58e412921ecbda4ffd377fb27c85eb..0000000000000000000000000000000000000000
--- 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%
--------------------------------------------------------------