[wp] dedicated dir/config for CE tests

src/plugins/wp/tests/ptests_config

-DEFAULT_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
+DEFAULT_SUITES= wp wp_acsl wp_plugin wp_ce wp_bts wp_store wp_hoare
 DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_region wp_tip
 
 qualif_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
 qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_region wp_tip
 qualif_SUITES= why3
+
+ce_SUITES= wp_ce

src/plugins/wp/tests/wp_plugin/cvc4_ce.i → src/plugins/wp/tests/wp_ce/cvc4_ce.i

-/* run.config_qualif
+/* run.config_ce
    OPT: -wp -wp-counter-examples -wp-prover cvc4 -wp-status
- */
+*/
+/* run.config_qualif
+   DONTRUN:
+*/
+
 
 //@ check lemma wrong: \forall integer x; \abs(x) == x;
 

src/plugins/wp/tests/wp_plugin/oracle/cvc4_ce.res.oracle → src/plugins/wp/tests/wp_ce/oracle/cvc4_ce.res.oracle

@@ -16,7 +16,7 @@ Prove: IAbs.abs(x) = x.
   Function wrong
 ------------------------------------------------------------
 
-Goal Post-condition (file cvc4_ce.i, line 7) in 'wrong':
+Goal Post-condition (file cvc4_ce.i, line 11) in 'wrong':
 Assume { Type: is_sint32(wrong_0). }
 Prove: IAbs.abs(wrong_0) = wrong_0.
 

src/plugins/wp/tests/wp_plugin/oracle/probes.res.oracle → src/plugins/wp/tests/wp_ce/oracle/probes.res.oracle

@@ -8,7 +8,7 @@
   Function get
 ------------------------------------------------------------
 
-Goal Post-condition (file probes.i, line 9) in 'get':
+Goal Post-condition (file probes.i, line 12) in 'get':
 Let x = -i_2.
 Assume {
   Type: is_sint32(i) /\ is_sint32(i_1) /\ is_sint32(i_2) /\ is_sint32(i_3) /\
@@ -32,19 +32,19 @@ Prove: false.
 ------------------------------------------------------------
 
 Goal Assigns nothing in 'get' (1/3):
-Effect at line 13
+Effect at line 16
 Prove: true.
 
 ------------------------------------------------------------
 
 Goal Assigns nothing in 'get' (2/3):
-Effect at line 15
+Effect at line 18
 Prove: true.
 
 ------------------------------------------------------------
 
 Goal Assigns nothing in 'get' (3/3):
-Effect at line 17
+Effect at line 20
 Prove: true.
 
 ------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/oracle_qualif/cvc4_ce.res.oracle → src/plugins/wp/tests/wp_ce/oracle_ce/cvc4_ce.res.oracle

@@ -5,8 +5,8 @@
 [wp] [Valid] Goal wrong_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled
-[wp] [Unsuccess] typed_check_lemma_wrong (CVC4) (No Cache) (Model)
-[wp] [Unsuccess] typed_wrong_ensures (CVC4) (No Cache) (Model)
+[wp] [Unsuccess] typed_check_lemma_wrong (CVC4) (Model)
+[wp] [Unsuccess] typed_wrong_ensures (CVC4) (Model)
 [wp] [Valid] typed_wrong_assigns (Qed)
 [wp] Proved goals:    3 / 5
   Terminating:     1
@@ -28,7 +28,7 @@ Model x = -1
   Function wrong
 ------------------------------------------------------------
 
-Goal Post-condition (file cvc4_ce.i, line 7) in 'wrong':
+Goal Post-condition (file cvc4_ce.i, line 11) in 'wrong':
 Assume { Type: is_sint32(wrong_0). Probe x = wrong_0. }
 Prove: IAbs.abs(wrong_0) = wrong_0.
 Prover CVC4 returns Unsuccess (Model)

src/plugins/wp/tests/wp_plugin/probes.i → src/plugins/wp/tests/wp_ce/probes.i

 /* run.config_qualif
    DONTRUN:
- */
+*/
+/* run.config_ce
+   DONTRUN:
+*/
 
 // Matrix addessing
 

src/plugins/wp/tests/wp_ce/test_config_ce

+PLUGIN: wp
+CMD: @frama-c@ -wp -wp-par 1 -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report %{dep:@PTEST_SUITE_DIR@/../qualif.report} -wp-cache none
+OPT: