diff --git a/src/plugins/wp/tests/wp_plugin/dynamic.i b/src/plugins/wp/tests/wp_plugin/dynamic.i
index f76b892b4b05a3b398b3d46a0cac5a33e7be1e37..872ed73e913ce945d53c7410e111ea32ff6fb378 100644
--- a/src/plugins/wp/tests/wp_plugin/dynamic.i
+++ b/src/plugins/wp/tests/wp_plugin/dynamic.i
@@ -44,6 +44,40 @@ void guarded_call (struct S * p) {
(* (p->f))(1);
}
+//-----------------------------------------------------------------------------
+int X1;
+//@ assigns X1; ensures X1==1;
+int h1(void);
+
+int X2;
+//@ assigns X2; ensures X2==2;
+int h2(void);
+
+//@ assigns \nothing;
+int h0(void);
+
+/*@ behavior bhv1:
+ @ assumes p == &h1;
+ @ assigns X1;
+ @ ensures X1==1; */
+int behavior (int (*p)(void)) {
+ //@ calls h1, h2;
+ return (*p)();
+}
+
+/*@ behavior bhv1:
+ @ assumes p == &h1;
+ @ assigns X1;
+ @ ensures X1==1;
+ @ behavior bhv0:
+ @ assumes p == &h0;
+ @ assigns \nothing;
+ @ ensures X1==\old(X1); */
+int some_behaviors (int (*p)(void)) {
+ //@ calls h1, h2, h0;
+ 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 5bc84b3ea34cd84e44029eedc2e50d44af10ee4d..b97f0a37aa9cd97ea326e52cb900aa51991817a2 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": 14 },
+{ "wp:global": { "alt-ergo": { "total": 12, "valid": 3, "unknown": 9,
+ "rank": 14 },
"qed": { "total": 10, "valid": 10 },
- "wp:main": { "total": 13, "valid": 13, "rank": 14 } },
+ "wp:main": { "total": 22, "valid": 13, "unknown": 9,
+ "rank": 14 } },
"wp:functions": { "call": { "specialization_f1_pre_at_call_stmt_3":
{ "alt-ergo": { "total": 1, "valid": 1,
"rank": 14 },
@@ -40,22 +42,64 @@
"guarded_call_post": { "alt-ergo":
{ "total": 1,
"valid": 1,
- "rank": 3 },
+ "rank": 5 },
"qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 2,
"valid": 2,
- "rank": 3 } },
+ "rank": 5 } },
"wp:section": { "alt-ergo": { "total": 1,
"valid": 1,
- "rank": 3 },
+ "rank": 5 },
"qed": { "total": 4,
"valid": 4 },
"wp:main": { "total": 5,
"valid": 5,
- "rank": 3 } } },
- "no_call": { "specialization_unreachable_g_pre_at_no_call_stmt_17":
+ "rank": 5 } } },
+ "behavior": { "behavior_bhv1_assign": { "alt-ergo":
+ { "total": 2,
+ "unknown": 2 },
+ "wp:main":
+ { "total": 2,
+ "unknown": 2 } },
+ "behavior_bhv1_post": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 3,
+ "unknown": 3 },
+ "wp:main": { "total": 3,
+ "unknown": 3 } } },
+ "some_behaviors": { "some_behaviors_bhv1_assign":
+ { "alt-ergo": { "total": 2,
+ "unknown": 2 },
+ "wp:main": { "total": 2,
+ "unknown": 2 } },
+ "some_behaviors_bhv0_assign":
+ { "alt-ergo": { "total": 2,
+ "unknown": 2 },
+ "wp:main": { "total": 2,
+ "unknown": 2 } },
+ "some_behaviors_bhv0_post": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "some_behaviors_bhv1_post": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 6,
+ "unknown": 6 },
+ "wp:main": { "total": 6,
+ "unknown": 6 } } },
+ "no_call": { "specialization_unreachable_g_pre_at_no_call_stmt_27":
{ "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 6aac439104f2110cfb2cfc488641ebb43666c2dc..7ce392e0cd6bf887cbf86ecd817c99d14763c891 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
@@ -2,9 +2,40 @@
[kernel] Parsing tests/wp_plugin/dynamic.i (no preprocessing)
[wp] Running WP plugin...
[wp] Computing dynamic calls.
-[wp] Dynamic call(s): 3.
+[wp] Dynamic call(s): 5.
[wp] Loading driver 'share/wp.driver'
+[wp] tests/wp_plugin/dynamic.i:65: Warning:
+ Ignored function pointer (see -wp-dynamic)
+[wp] tests/wp_plugin/dynamic.i:78: Warning:
+ Ignored function pointer (see -wp-dynamic)
[wp] Warning: Missing RTE guards
+[wp] tests/wp_plugin/dynamic.i:65: Warning:
+ Missing assigns clause (assigns 'everything' instead)
+[wp] tests/wp_plugin/dynamic.i:78: Warning:
+ Missing assigns clause (assigns 'everything' instead)
+------------------------------------------------------------
+ Function behavior with behavior bhv1
+------------------------------------------------------------
+
+Goal Post-condition for 'bhv1' (file tests/wp_plugin/dynamic.i, line 62) in 'behavior':
+Assume { Type: is_sint32(X1_0). (* Heap *) Have: region(G_h1_57) <= 0. }
+Prove: X1_0 = 1.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 61) in 'behavior':
+Effect at line 65
+Assume { (* Heap *) Have: region(G_h1_57) <= 0. }
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 61) in 'behavior':
+Effect at line 65
+Assume { (* Heap *) Have: region(G_h1_57) <= 0. }
+Prove: false.
+
+------------------------------------------------------------
------------------------------------------------------------
Function call
------------------------------------------------------------
@@ -96,28 +127,84 @@ Prove: true.
Function no_call
------------------------------------------------------------
-Goal calls unreachable_g in 'no_call' at instruction (file tests/wp_plugin/dynamic.i, line 57):
+Goal calls unreachable_g in 'no_call' at instruction (file tests/wp_plugin/dynamic.i, line 91):
Prove: true.
------------------------------------------------------------
-Goal Post-condition (file tests/wp_plugin/dynamic.i, line 51) in 'no_call' (1/2):
+Goal Post-condition (file tests/wp_plugin/dynamic.i, line 85) in 'no_call' (1/2):
Prove: true.
------------------------------------------------------------
-Goal Post-condition (file tests/wp_plugin/dynamic.i, line 51) in 'no_call' (2/2):
+Goal Post-condition (file tests/wp_plugin/dynamic.i, line 85) in 'no_call' (2/2):
Tags: Call unreachable_g.
Prove: true.
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_plugin/dynamic.i, line 48) in 'unreachable_g'' in 'no_call' at instruction (file tests/wp_plugin/dynamic.i, line 57)
+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)
:
Tags: Call unreachable_g.
Prove: true.
+------------------------------------------------------------
+------------------------------------------------------------
+ Function some_behaviors with behavior bhv0
+------------------------------------------------------------
+
+Goal Post-condition for 'bhv0' (file tests/wp_plugin/dynamic.i, line 75) in 'some_behaviors':
+Assume {
+ Type: is_sint32(X1_1) /\ is_sint32(X1_0).
+ (* Heap *)
+ Have: region(G_h0_68) <= 0.
+}
+Prove: X1_0 = X1_1.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv0' nothing in 'some_behaviors':
+Effect at line 78
+Assume { (* Heap *) Have: region(G_h0_68) <= 0. }
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv0' nothing in 'some_behaviors':
+Effect at line 78
+Assume { (* Heap *) Have: region(G_h0_68) <= 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function some_behaviors with behavior bhv1
+------------------------------------------------------------
+
+Goal Post-condition for 'bhv1' (file tests/wp_plugin/dynamic.i, line 71) in 'some_behaviors':
+Assume { Type: is_sint32(X1_0). (* Heap *) Have: region(G_h1_57) <= 0. }
+Prove: X1_0 = 1.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 70) in 'some_behaviors':
+Effect at line 78
+Assume { (* Heap *) Have: region(G_h1_57) <= 0. }
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 70) in 'some_behaviors':
+Effect at line 78
+Assume { (* Heap *) Have: region(G_h1_57) <= 0. }
+Prove: false.
+
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'guarded_call':
/*@ behavior typed: requires \separated(&X,p); */
void guarded_call(struct S *p);
+[wp] Warning: Memory model hypotheses for function 'behavior':
+ /*@ behavior typed: requires \separated(&X1,p); */
+ int behavior(int (*p)(void));
+[wp] Warning: Memory model hypotheses for function 'some_behaviors':
+ /*@ behavior typed: requires \separated(&X1,p); */
+ int some_behaviors(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 56ccd9a1c6bde78f47a6ac79c3e07806204b9979..407920ab0a3e23273513f3ead111148c0e0d2579 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
@@ -2,10 +2,21 @@
[kernel] Parsing tests/wp_plugin/dynamic.i (no preprocessing)
[wp] Running WP plugin...
[wp] Computing dynamic calls.
-[wp] Dynamic call(s): 3.
+[wp] Dynamic call(s): 5.
[wp] Loading driver 'share/wp.driver'
+[wp] tests/wp_plugin/dynamic.i:65: Warning:
+ Ignored function pointer (see -wp-dynamic)
+[wp] tests/wp_plugin/dynamic.i:78: Warning:
+ Ignored function pointer (see -wp-dynamic)
[wp] Warning: Missing RTE guards
-[wp] 13 goals scheduled
+[wp] tests/wp_plugin/dynamic.i:65: Warning:
+ Missing assigns clause (assigns 'everything' instead)
+[wp] tests/wp_plugin/dynamic.i:78: Warning:
+ Missing assigns clause (assigns 'everything' instead)
+[wp] 22 goals scheduled
+[wp] [Alt-Ergo] Goal typed_behavior_bhv1_post : Unknown
+[wp] [Alt-Ergo] Goal typed_behavior_bhv1_assign_exit : Unknown
+[wp] [Alt-Ergo] Goal typed_behavior_bhv1_assign_normal : Unknown
[wp] [Alt-Ergo] Goal typed_call_stmt_calls_f1_f2 : Valid
[wp] [Qed] Goal typed_call_post_part1 : Valid
[wp] [Qed] Goal typed_call_post_part2 : Valid
@@ -19,16 +30,30 @@
[wp] [Qed] Goal typed_no_call_post_part1 : Valid
[wp] [Qed] Goal typed_no_call_post_part2 : Valid
[wp] [Qed] Goal typed_no_call_call_unreachable_g_pre : Valid
-[wp] Proved goals: 13 / 13
+[wp] [Alt-Ergo] Goal typed_some_behaviors_bhv0_post : Unknown
+[wp] [Alt-Ergo] Goal typed_some_behaviors_bhv0_assign_exit : Unknown
+[wp] [Alt-Ergo] Goal typed_some_behaviors_bhv0_assign_normal : Unknown
+[wp] [Alt-Ergo] Goal typed_some_behaviors_bhv1_post : Unknown
+[wp] [Alt-Ergo] Goal typed_some_behaviors_bhv1_assign_exit : Unknown
+[wp] [Alt-Ergo] Goal typed_some_behaviors_bhv1_assign_normal : Unknown
+[wp] Proved goals: 13 / 22
Qed: 10
- Alt-Ergo: 3
+ Alt-Ergo: 3 (unknown: 9)
[wp] Report 'tests/wp_plugin/dynamic.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
call 2 2 (52..64) 4 100%
-guarded_call 4 1 (8..20) 5 100%
+guarded_call 4 1 (16..28) 5 100%
+behavior - - 3 0.0%
+some_behaviors - - 6 0.0%
no_call 4 - 4 100%
-------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'guarded_call':
/*@ behavior typed: requires \separated(&X,p); */
void guarded_call(struct S *p);
+[wp] Warning: Memory model hypotheses for function 'behavior':
+ /*@ behavior typed: requires \separated(&X1,p); */
+ int behavior(int (*p)(void));
+[wp] Warning: Memory model hypotheses for function 'some_behaviors':
+ /*@ behavior typed: requires \separated(&X1,p); */
+ int some_behaviors(int (*p)(void));