Skip to content
Snippets Groups Projects
Commit ea917f7e authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[wp] exhibits lacks into dynamic calls

parent 11d95eab
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/tests/wp_plugin/dynamic.i
+ 34
− 0
View file @ ea917f7e
...@@ -44,6 +44,40 @@ void guarded_call (struct S * p) { ...@@ -44,6 +44,40 @@ void guarded_call (struct S * p) {
(* (p->f))(1); (* (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; //@ requires \false; ensures \false; exits \false; assigns \nothing;
int unreachable_g(int x); int unreachable_g(int x);
......
src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json
+ 51
− 7
View file @ ea917f7e
{ "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 }, "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": "wp:functions": { "call": { "specialization_f1_pre_at_call_stmt_3":
{ "alt-ergo": { "total": 1, "valid": 1, { "alt-ergo": { "total": 1, "valid": 1,
"rank": 14 }, "rank": 14 },
...@@ -40,22 +42,64 @@ ...@@ -40,22 +42,64 @@
"guarded_call_post": { "alt-ergo": "guarded_call_post": { "alt-ergo":
{ "total": 1, { "total": 1,
"valid": 1, "valid": 1,
"rank": 3 }, "rank": 5 },
"qed": { "total": 1, "qed": { "total": 1,
"valid": 1 }, "valid": 1 },
"wp:main": "wp:main":
{ "total": 2, { "total": 2,
"valid": 2, "valid": 2,
"rank": 3 } }, "rank": 5 } },
"wp:section": { "alt-ergo": { "total": 1, "wp:section": { "alt-ergo": { "total": 1,
"valid": 1, "valid": 1,
"rank": 3 }, "rank": 5 },
"qed": { "total": 4, "qed": { "total": 4,
"valid": 4 }, "valid": 4 },
"wp:main": { "total": 5, "wp:main": { "total": 5,
"valid": 5, "valid": 5,
"rank": 3 } } }, "rank": 5 } } },
"no_call": { "specialization_unreachable_g_pre_at_no_call_stmt_17": "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 }, { "qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 1, "valid": 1 } }, "wp:main": { "total": 1, "valid": 1 } },
"no_call_stmt_calls_unreachable_g": "no_call_stmt_calls_unreachable_g":
......
src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+ 92
− 5
View file @ ea917f7e
...@@ -2,9 +2,40 @@ ...@@ -2,9 +2,40 @@
[kernel] Parsing tests/wp_plugin/dynamic.i (no preprocessing) [kernel] Parsing tests/wp_plugin/dynamic.i (no preprocessing)
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Computing dynamic calls. [wp] Computing dynamic calls.
[wp] Dynamic call(s): 3. [wp] Dynamic call(s): 5.
[wp] Loading driver 'share/wp.driver' [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] 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 Function call
------------------------------------------------------------ ------------------------------------------------------------
...@@ -96,28 +127,84 @@ Prove: true. ...@@ -96,28 +127,84 @@ Prove: true.
Function no_call 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. 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. 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. Tags: Call unreachable_g.
Prove: true. 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. Tags: Call unreachable_g.
Prove: true. 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': [wp] Warning: Memory model hypotheses for function 'guarded_call':
/*@ behavior typed: requires \separated(&X,p); */ /*@ behavior typed: requires \separated(&X,p); */
void guarded_call(struct S *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));
src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
+ 30
− 5
View file @ ea917f7e
...@@ -2,10 +2,21 @@ ...@@ -2,10 +2,21 @@
[kernel] Parsing tests/wp_plugin/dynamic.i (no preprocessing) [kernel] Parsing tests/wp_plugin/dynamic.i (no preprocessing)
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Computing dynamic calls. [wp] Computing dynamic calls.
[wp] Dynamic call(s): 3. [wp] Dynamic call(s): 5.
[wp] Loading driver 'share/wp.driver' [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] 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] [Alt-Ergo] Goal typed_call_stmt_calls_f1_f2 : Valid
[wp] [Qed] Goal typed_call_post_part1 : Valid [wp] [Qed] Goal typed_call_post_part1 : Valid
[wp] [Qed] Goal typed_call_post_part2 : Valid [wp] [Qed] Goal typed_call_post_part2 : Valid
...@@ -19,16 +30,30 @@ ...@@ -19,16 +30,30 @@
[wp] [Qed] Goal typed_no_call_post_part1 : Valid [wp] [Qed] Goal typed_no_call_post_part1 : Valid
[wp] [Qed] Goal typed_no_call_post_part2 : Valid [wp] [Qed] Goal typed_no_call_post_part2 : Valid
[wp] [Qed] Goal typed_no_call_call_unreachable_g_pre : 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 Qed: 10
Alt-Ergo: 3 Alt-Ergo: 3 (unknown: 9)
[wp] Report 'tests/wp_plugin/dynamic.i.0.report.json' [wp] Report 'tests/wp_plugin/dynamic.i.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
call 2 2 (52..64) 4 100% 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% no_call 4 - 4 100%
------------------------------------------------------------- -------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'guarded_call': [wp] Warning: Memory model hypotheses for function 'guarded_call':
/*@ behavior typed: requires \separated(&X,p); */ /*@ behavior typed: requires \separated(&X,p); */
void guarded_call(struct S *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));
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment