From d1ebfb7317853b4d2654332b8850b64aec8d80ef Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 24 Jan 2019 15:28:40 +0100
Subject: [PATCH] [WP] added tests with incomplete consolidation
---
src/plugins/wp/tests/wp_plugin/dynamic.i | 17 +++++--
.../tests/wp_plugin/dynamic.i.0.report.json | 35 ++++++++++++--
.../tests/wp_plugin/oracle/dynamic.res.oracle | 48 ++++++++++++++++---
.../oracle_qualif/dynamic.res.oracle | 17 +++++--
4 files changed, 99 insertions(+), 18 deletions(-)
diff --git a/src/plugins/wp/tests/wp_plugin/dynamic.i b/src/plugins/wp/tests/wp_plugin/dynamic.i
index e1c5eed1bda..3f9e7b87a8b 100644
--- a/src/plugins/wp/tests/wp_plugin/dynamic.i
+++ b/src/plugins/wp/tests/wp_plugin/dynamic.i
@@ -6,10 +6,10 @@
OPT: -wp-dynamic -wp
*/
//-----------------------------------------------------------------------------
-/*@
+/*@
requires -10<=x<=10;
- ensures \result == x+1;
- assigns \nothing;
+ ensures \result == x+1;
+ assigns \nothing;
*/
int f1(int x);
@@ -22,7 +22,7 @@ typedef struct S {
} ;
/*@
- requires (closure->f == &f1 && \abs(closure->param)<=5) || closure->f == &f2 ;
+ requires (closure->f == &f1 && \abs(closure->param)<=5) || closure->f == &f2 ;
ensures \abs(\result - closure->param) <= 1 ;
*/
int call(struct S * closure) {
@@ -78,6 +78,15 @@ int some_behaviors (int (*p)(void)) {
return (*p)();
}
+/*@
+ ensures X1==1;
+ assigns X1 ;
+*/
+int missing_context (int (*p)(void)) {
+ //@ calls h1 ;
+ return (*p)();
+}
+
//-----------------------------------------------------------------------------
//@ requires \false; ensures \false; exits \false; assigns \nothing;
int unreachable_g(int x);
diff --git a/src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json b/src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json
index 928d6afe79e..6f08ea23f4e 100644
--- a/src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json
+++ b/src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json
@@ -1,6 +1,8 @@
-{ "wp:global": { "alt-ergo": { "total": 3, "valid": 3, "rank": 16 },
- "qed": { "total": 43, "valid": 43 },
- "wp:main": { "total": 46, "valid": 46, "rank": 16 } },
+{ "wp:global": { "alt-ergo": { "total": 4, "valid": 3, "unknown": 1,
+ "rank": 16 },
+ "qed": { "total": 47, "valid": 47 },
+ "wp:main": { "total": 51, "valid": 50, "unknown": 1,
+ "rank": 16 } },
"wp:functions": { "call": { "specialization_f1_pre_at_call_stmt_3":
{ "alt-ergo": { "total": 1, "valid": 1,
"rank": 16 },
@@ -104,7 +106,32 @@
"valid": 24 },
"wp:main": { "total": 24,
"valid": 24 } } },
- "no_call": { "specialization_unreachable_g_pre_at_no_call_stmt_27":
+ "missing_context": { "missing_context_stmt_calls_h1":
+ { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "missing_context_assign": { "qed":
+ { "total": 3,
+ "valid": 3 },
+ "wp:main":
+ { "total": 3,
+ "valid": 3 } },
+ "missing_context_post": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "qed": { "total": 4,
+ "valid": 4 },
+ "wp:main": { "total": 5,
+ "valid": 4,
+ "unknown": 1 } } },
+ "no_call": { "specialization_unreachable_g_pre_at_no_call_stmt_32":
{ "qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 1, "valid": 1 } },
"no_call_stmt_calls_unreachable_g":
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
index 6b119b905ab..6a9d0d76d5b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
@@ -7,8 +7,9 @@
[wp] tests/wp_plugin/dynamic.i:65: Calls h1 h2
[wp] tests/wp_plugin/dynamic.i:78: Calls (for bhv1) h1 h2 h0
[wp] tests/wp_plugin/dynamic.i:78: Calls (for bhv0) h1 h2 h0
-[wp] tests/wp_plugin/dynamic.i:91: Calls unreachable_g
-[wp:calls] Dynamic call(s): 5.
+[wp] tests/wp_plugin/dynamic.i:87: Calls h1
+[wp] tests/wp_plugin/dynamic.i:100: Calls unreachable_g
+[wp:calls] Dynamic call(s): 6.
[wp] Loading driver 'share/wp.driver'
[wp] tests/wp_plugin/dynamic.i:78: Warning:
Missigns 'calls' clause dedicated to dynamic calls (see WP manual)
@@ -158,28 +159,60 @@ Goal Post-condition (file tests/wp_plugin/dynamic.i, line 39) in 'guarded_call'
Tags: Call g.
Prove: true.
+------------------------------------------------------------
+------------------------------------------------------------
+ Function missing_context
+------------------------------------------------------------
+
+Goal Calls h1 in 'missing_context' at instruction (file tests/wp_plugin/dynamic.i, line 87):
+Assume { (* Heap *) Have: region(p.base) <= 0. }
+Prove: global(G_h1_57) = p.
+
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_plugin/dynamic.i, line 82) in 'missing_context':
+Tags: Call h1.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/dynamic.i, line 83) in 'missing_context':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/dynamic.i, line 83) in 'missing_context' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/dynamic.i, line 83) in 'missing_context' (2/2):
+Call Result at line 87
+Tags: Call h1.
+Prove: true.
+
------------------------------------------------------------
------------------------------------------------------------
Function no_call
------------------------------------------------------------
-Goal Calls unreachable_g in 'no_call' at instruction (file tests/wp_plugin/dynamic.i, line 91):
+Goal Calls unreachable_g in 'no_call' at instruction (file tests/wp_plugin/dynamic.i, line 100):
Prove: true.
------------------------------------------------------------
-Goal Post-condition (file tests/wp_plugin/dynamic.i, line 85) in 'no_call' (1/2):
+Goal Post-condition (file tests/wp_plugin/dynamic.i, line 94) in 'no_call' (1/2):
Prove: true.
------------------------------------------------------------
-Goal Post-condition (file tests/wp_plugin/dynamic.i, line 85) in 'no_call' (2/2):
+Goal Post-condition (file tests/wp_plugin/dynamic.i, line 94) in 'no_call' (2/2):
Tags: Call unreachable_g.
Prove: true.
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_plugin/dynamic.i, line 82) in 'unreachable_g'' in 'no_call' at instruction (file tests/wp_plugin/dynamic.i, line 91)
+Goal Instance of 'Pre-condition (file tests/wp_plugin/dynamic.i, line 91) in 'unreachable_g'' in 'no_call' at instruction (file tests/wp_plugin/dynamic.i, line 100)
:
Tags: Call unreachable_g.
Prove: true.
@@ -350,3 +383,6 @@ Prove: true.
[wp] Warning: Memory model hypotheses for function 'some_behaviors':
/*@ behavior typed: requires \separated(&X1,p); */
int some_behaviors(int (*p)(void));
+[wp] Warning: Memory model hypotheses for function 'missing_context':
+ /*@ behavior typed: requires \separated(&X1,p); */
+ int missing_context(int (*p)(void));
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
index 42d0aad2267..8bccdefb12e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
@@ -5,7 +5,7 @@
[wp] tests/wp_plugin/dynamic.i:78: Warning:
Missigns 'calls' clause dedicated to dynamic calls (see WP manual)
[wp] Warning: Missing RTE guards
-[wp] 46 goals scheduled
+[wp] 51 goals scheduled
[wp] [Qed] Goal typed_behavior_stmt_calls_h1_h2_for_bhv1 : Valid
[wp] [Qed] Goal typed_behavior_bhv1_post_part1 : Valid
[wp] [Qed] Goal typed_behavior_bhv1_post_part2 : Valid
@@ -24,6 +24,11 @@
[wp] [Qed] Goal typed_guarded_call_post_part2 : Valid
[wp] [Qed] Goal typed_guarded_call_post_2_part1 : Valid
[wp] [Qed] Goal typed_guarded_call_post_2_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_missing_context_stmt_calls_h1 : Unknown
+[wp] [Qed] Goal typed_missing_context_post : Valid
+[wp] [Qed] Goal typed_missing_context_assign_exit : Valid
+[wp] [Qed] Goal typed_missing_context_assign_normal_part1 : Valid
+[wp] [Qed] Goal typed_missing_context_assign_normal_part2 : Valid
[wp] [Qed] Goal typed_no_call_stmt_calls_unreachable_g : Valid
[wp] [Qed] Goal typed_no_call_post_part1 : Valid
[wp] [Qed] Goal typed_no_call_post_part2 : Valid
@@ -52,9 +57,9 @@
[wp] [Qed] Goal typed_some_behaviors_bhv1_assign_normal_part3 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv1_assign_normal_part4 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv1_assign_normal_part5 : Valid
-[wp] Proved goals: 46 / 46
- Qed: 43
- Alt-Ergo: 3
+[wp] Proved goals: 50 / 51
+ Qed: 47
+ Alt-Ergo: 3 (unknown: 1)
[wp] Report 'tests/wp_plugin/dynamic.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
@@ -62,6 +67,7 @@ call 2 2 (56..80) 4 100%
guarded_call 4 1 (16..28) 5 100%
behavior 9 - 9 100%
some_behaviors 24 - 24 100%
+missing_context 4 - 5 80.0%
no_call 4 - 4 100%
-------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'guarded_call':
@@ -73,3 +79,6 @@ no_call 4 - 4 100%
[wp] Warning: Memory model hypotheses for function 'some_behaviors':
/*@ behavior typed: requires \separated(&X1,p); */
int some_behaviors(int (*p)(void));
+[wp] Warning: Memory model hypotheses for function 'missing_context':
+ /*@ behavior typed: requires \separated(&X1,p); */
+ int missing_context(int (*p)(void));
--
GitLab