From bb0d6454db7db68f8c6f79b31b00773977127bfc Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 1 Jun 2021 17:23:21 +0200
Subject: [PATCH] [wp] More tests for smoking assumes
---
src/plugins/wp/tests/wp_plugin/doomed_pre.i | 33 ++++++-
.../wp_plugin/oracle/doomed_pre.res.oracle | 88 +++++++++++++++++--
.../oracle_qualif/doomed_pre.res.oracle | 43 ++++++---
3 files changed, 146 insertions(+), 18 deletions(-)
diff --git a/src/plugins/wp/tests/wp_plugin/doomed_pre.i b/src/plugins/wp/tests/wp_plugin/doomed_pre.i
index 104c9ec932c..d7be0aa8c9a 100644
--- a/src/plugins/wp/tests/wp_plugin/doomed_pre.i
+++ b/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){}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/doomed_pre.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/doomed_pre.res.oracle
index b472440a78e..fe70e5a3f43 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/doomed_pre.res.oracle
+++ b/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.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle
index 80e10bd4d49..34eb51d822f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle
+++ b/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%
------------------------------------------------------------
--
GitLab