[wp] Update qualif oracles and remove drivers

src/plugins/wp/tests/wp_acsl/classify_float.c

 /* 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
  */

src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle

 # 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%

src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle

 # 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%
 ------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle

-# 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%
-------------------------------------------------------------

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";

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) ; } */
 

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}
 */
 
 // --------------------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/flash-ergo.driver

-library INDEX: const
-logic index INDEX_init = {coq="dumb"; altergo="const(0)"; why3="Flash.init"; } ;

src/plugins/wp/tests/wp_plugin/flash.c

 /* 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;

src/plugins/wp/tests/wp_plugin/flash.driver

 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

src/plugins/wp/tests/wp_plugin/flash.mlw

-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

src/plugins/wp/tests/wp_plugin/float_format.i

 /* 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
 */
 

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 );
 
 // --------------------------------------------------------------------------
 

src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle

-# 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%
-------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle

-# 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%
--------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle

 # 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%
 ------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle

-# 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%
-------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle

 # 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...

src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle

 # 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%