[wp] More tests for smoking assumes

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

@@ -7,13 +7,34 @@
 */
 
 //@ requires a < 0 && a > 0 ;
-void default_requires(int a){}
+void requires(int a){}
 
 /*@ requires a < 0 ;
     behavior B:
       assumes a > 0 ;
 */
-void default_reqs_assumes(int a){}
+void reqs_assumes(int a){}
+
+/*@ requires a < 0 ;
+    behavior B:
+      assumes a > 0 ;
+      assumes a > 1 ;
+*/
+void reqs_2_2_assumes(int a){}
+
+/*@ requires a < 0 ;
+    behavior B:
+      assumes a > 0 ;
+      assumes a < -42 ;
+*/
+void reqs_1_2_assumes(int a){}
+
+/*@ requires a >= 0 ;
+    behavior B:
+      assumes a > 10 ;
+      assumes a < 10 ;
+*/
+void reqs_combined_assumes(int a){}
 
 /*@ behavior B:
       assumes a < 0 && a > 0 ; // not detected
@@ -25,3 +46,11 @@ void only_assumes(int a){}
       requires a < 0 ;
 */
 void bhv_requires_assumes(int a){}
+
+/*@ requires a < 0 ;
+    behavior B1:
+      assumes a > 0 ;
+    behavior B2:
+      assumes a > 1 ;
+*/
+void reqs_massumes(int a){}

src/plugins/wp/tests/wp_plugin/oracle/doomed_pre.res.oracle

@@ -11,27 +11,103 @@ Prove: true.
 
 ------------------------------------------------------------
 ------------------------------------------------------------
-  Function default_reqs_assumes
+  Function reqs_1_2_assumes
 ------------------------------------------------------------
 
-Goal Wp_smoke_default_requires in 'default_reqs_assumes':
+Goal Wp_smoke_default_requires in 'reqs_1_2_assumes':
 Assume { Type: is_sint32(a). (* Pre-condition *) Have: a < 0. }
 Prove: false.
 
 ------------------------------------------------------------
 ------------------------------------------------------------
-  Function default_reqs_assumes with behavior B
+  Function reqs_1_2_assumes with behavior B
 ------------------------------------------------------------
 
-Goal Wp_smoke_B_assumes in 'default_reqs_assumes':
+Goal Wp_smoke_B_assumes in 'reqs_1_2_assumes':
 Prove: true.
 
 ------------------------------------------------------------
 ------------------------------------------------------------
-  Function default_requires
+  Function reqs_2_2_assumes
 ------------------------------------------------------------
 
-Goal Wp_smoke_default_requires in 'default_requires':
+Goal Wp_smoke_default_requires in 'reqs_2_2_assumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: a < 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_2_2_assumes with behavior B
+------------------------------------------------------------
+
+Goal Wp_smoke_B_assumes in 'reqs_2_2_assumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_assumes
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'reqs_assumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: a < 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_assumes with behavior B
+------------------------------------------------------------
+
+Goal Wp_smoke_B_assumes in 'reqs_assumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_combined_assumes
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'reqs_combined_assumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: 0 <= a. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_combined_assumes with behavior B
+------------------------------------------------------------
+
+Goal Wp_smoke_B_assumes in 'reqs_combined_assumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_massumes
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'reqs_massumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: a < 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_massumes with behavior B1
+------------------------------------------------------------
+
+Goal Wp_smoke_B1_assumes in 'reqs_massumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function reqs_massumes with behavior B2
+------------------------------------------------------------
+
+Goal Wp_smoke_B2_assumes in 'reqs_massumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function requires
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'requires':
 Prove: true.
 
 ------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle

@@ -2,23 +2,46 @@
 [kernel] Parsing tests/wp_plugin/doomed_pre.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 4 goals scheduled
-[wp] [Failed] Smoke-test typed_default_requires_wp_smoke_default_requires
+[wp] 13 goals scheduled
+[wp] [Failed] Smoke-test typed_requires_wp_smoke_default_requires
        Qed: Valid
 [wp] tests/wp_plugin/doomed_pre.i:10: Warning: Failed smoke-test
-[wp] [Passed] Smoke-test typed_default_reqs_assumes_wp_smoke_default_requires
-[wp] [Failed] Smoke-test typed_default_reqs_assumes_wp_smoke_B_assumes
+[wp] [Passed] Smoke-test typed_reqs_assumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_assumes_wp_smoke_B_assumes
        Qed: Valid
 [wp] tests/wp_plugin/doomed_pre.i:16: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_2_2_assumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_2_2_assumes_wp_smoke_B_assumes
+       Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:23: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_1_2_assumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_1_2_assumes_wp_smoke_B_assumes
+       Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:30: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_combined_assumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_combined_assumes_wp_smoke_B_assumes
+       Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:37: Warning: Failed smoke-test
 [wp] [Failed] Smoke-test typed_bhv_requires_assumes_wp_smoke_B_requires
        Qed: Valid
-[wp] tests/wp_plugin/doomed_pre.i:27: Warning: Failed smoke-test
-[wp] Proved goals:    1 / 4
-  Qed:             0  (failed: 3)
-  Alt-Ergo:        1
+[wp] tests/wp_plugin/doomed_pre.i:48: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_massumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_massumes_wp_smoke_B1_assumes
+       Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:56: Warning: Failed smoke-test
+[wp] [Failed] Smoke-test typed_reqs_massumes_wp_smoke_B2_assumes
+       Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:56: Warning: Failed smoke-test
+[wp] Proved goals:    5 / 13
+  Qed:             0  (failed: 8)
+  Alt-Ergo:        5
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  default_requires          -        -        1       0.0%
-  default_reqs_assumes      -        1        2      50.0%
+  requires                  -        -        1       0.0%
+  reqs_assumes              -        1        2      50.0%
+  reqs_2_2_assumes          -        1        2      50.0%
+  reqs_1_2_assumes          -        1        2      50.0%
+  reqs_combined_assumes     -        1        2      50.0%
   bhv_requires_assumes      -        -        1       0.0%
+  reqs_massumes             -        1        3      33.3%
 ------------------------------------------------------------