From 0e75d25756d9d788e64940671546f3458cf789b1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 16 Feb 2021 15:06:59 +0100
Subject: [PATCH] [wp] do not use stmt-contract
---
.../wp_typed/oracle/unit_tset.0.res.oracle | 15 ++++++++------
.../wp_typed/oracle/unit_tset.1.res.oracle | 15 ++++++++------
.../oracle_qualif/unit_tset.res.oracle | 11 +++++-----
src/plugins/wp/tests/wp_typed/unit_tset.i | 20 +++++++++----------
4 files changed, 33 insertions(+), 28 deletions(-)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle
index fd636bbb09f..2bf4af29a7c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle
@@ -6,17 +6,20 @@
Function complex
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_typed/unit_tset.i, line 6) in 'job'' in 'complex' at call 'job' (file tests/wp_typed/unit_tset.i, line 20)
-:
+Goal Assigns (file tests/wp_typed/unit_tset.i, line 14) in 'complex':
+Call Effect at line 18
Prove: true.
------------------------------------------------------------
-------------------------------------------------------------
- Function complex with behavior default_for_stmt_2
+
+Goal Assigns (file tests/wp_typed/unit_tset.i, line 14) in 'complex':
+Call Effect at line 18
+Prove: true.
+
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/unit_tset.i, line 19) at call 'job' (file tests/wp_typed/unit_tset.i, line 20):
-Call Effect at line 20
+Goal Instance of 'Pre-condition (file tests/wp_typed/unit_tset.i, line 2) in 'job'' in 'complex' at call 'job' (file tests/wp_typed/unit_tset.i, line 18)
+:
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle
index 7af88b3ded6..60beed97a62 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle
@@ -6,17 +6,20 @@
Function complex
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_typed/unit_tset.i, line 6) in 'job'' in 'complex' at call 'job' (file tests/wp_typed/unit_tset.i, line 20)
-:
+Goal Assigns (file tests/wp_typed/unit_tset.i, line 14) in 'complex':
+Call Effect at line 18
Prove: true.
------------------------------------------------------------
-------------------------------------------------------------
- Function complex with behavior default_for_stmt_2
+
+Goal Assigns (file tests/wp_typed/unit_tset.i, line 14) in 'complex':
+Call Effect at line 18
+Prove: true.
+
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/unit_tset.i, line 19) at call 'job' (file tests/wp_typed/unit_tset.i, line 20):
-Call Effect at line 20
+Goal Instance of 'Pre-condition (file tests/wp_typed/unit_tset.i, line 2) in 'job'' in 'complex' at call 'job' (file tests/wp_typed/unit_tset.i, line 18)
+:
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle
index 73c76c092af..a28d76ae998 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle
@@ -2,12 +2,13 @@
[kernel] Parsing tests/wp_typed/unit_tset.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 2 goals scheduled
-[wp] [Qed] Goal typed_complex_assigns : Valid
+[wp] 3 goals scheduled
+[wp] [Qed] Goal typed_complex_assigns_exit : Valid
+[wp] [Qed] Goal typed_complex_assigns_normal : Valid
[wp] [Qed] Goal typed_complex_call_job_requires : Valid
-[wp] Proved goals: 2 / 2
- Qed: 2
+[wp] Proved goals: 3 / 3
+ Qed: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- complex 2 - 2 100%
+ complex 3 - 3 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/unit_tset.i b/src/plugins/wp/tests/wp_typed/unit_tset.i
index deaf2545a0d..d08be34855d 100644
--- a/src/plugins/wp/tests/wp_typed/unit_tset.i
+++ b/src/plugins/wp/tests/wp_typed/unit_tset.i
@@ -1,21 +1,19 @@
-/* run.config_qualif
- OPT:
-*/
-
-/*@
- requires \valid( p + (0..n-1) );
+/*@
+ requires \valid( p + (0..n-1) );
assigns p[0..n-1];
*/
void job(int *p,int n);
-typedef struct S {
+struct S {
int size ;
int value[50] ;
-} ;
+} s ;
-/*@ requires s.size < 50; */
-void complex(struct S s)
+/*@
+ requires s.size < 50;
+ assigns s.value[1..s.size];
+*/
+void complex(void)
{
- /*@ assigns s.value[1..s.size]; */
job( & s.value[1] , s.size );
}
--
GitLab