Skip to content
Snippets Groups Projects
Commit 150618d5 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Add tests for nesting with -wp-unfold-assigns

parent fcf35a4c
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/oracle/unfold_assigns.0.res.oracle
+ 170
− 5
View file @ 150618d5
...@@ -25,6 +25,66 @@ Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 56) in 'ASSIGN_NO_UNFO ...@@ -25,6 +25,66 @@ Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 56) in 'ASSIGN_NO_UNFO
Effect at line 59 Effect at line 59
Prove: true. Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function NESTED_ARRAY_STATIC
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 90) in 'NESTED_ARRAY_STATIC':
Call Effect at line 92
Assume {
(* Heap *)
Type: (region(s.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: !invalid(Malloc_0, s, 4).
}
Prove: false.
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 90) in 'NESTED_ARRAY_STATIC':
Call Effect at line 92
Assume {
(* Heap *)
Type: (region(s.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: !invalid(Malloc_0, s, 4).
}
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function NESTED_ARRAY_VARS
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 96) in 'NESTED_ARRAY_VARS':
Call Effect at line 98
Assume {
Type: is_uint32(n).
(* Heap *)
Type: (region(s.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: !invalid(Malloc_0, s, 4).
(* Pre-condition *)
Have: 3 <= n.
}
Prove: included(s, 4, shift_sint32(shiftfield_F2_With_array_t(s), 1), n).
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 96) in 'NESTED_ARRAY_VARS':
Call Effect at line 98
Assume {
Type: is_uint32(n).
(* Heap *)
Type: (region(s.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: !invalid(Malloc_0, s, 4).
(* Pre-condition *)
Have: 3 <= n.
}
Prove: included(s, 4, shift_sint32(shiftfield_F2_With_array_t(s), 1), n).
------------------------------------------------------------ ------------------------------------------------------------
------------------------------------------------------------ ------------------------------------------------------------
Function NO_UNFOLD_KO Function NO_UNFOLD_KO
...@@ -99,11 +159,38 @@ Prove: true. ...@@ -99,11 +159,38 @@ Prove: true.
------------------------------------------------------------ ------------------------------------------------------------
------------------------------------------------------------ ------------------------------------------------------------
Function PARTIAL_ASSIGNS Function PARTIAL_ASSIGNS_STATIC
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 71) in 'PARTIAL_ASSIGNS_STATIC':
Call Effect at line 73
Assume {
(* Heap *)
Type: (region(p.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: !invalid(Malloc_0, shift_sint32(p, 0), 5).
}
Prove: false.
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 71) in 'PARTIAL_ASSIGNS_STATIC':
Call Effect at line 73
Assume {
(* Heap *)
Type: (region(p.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: !invalid(Malloc_0, shift_sint32(p, 0), 5).
}
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function PARTIAL_ASSIGNS_VARS
------------------------------------------------------------ ------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 72) in 'PARTIAL_ASSIGNS': Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 77) in 'PARTIAL_ASSIGNS_VARS':
Call Effect at line 74 Call Effect at line 79
Let a = shift_sint32(p, 0). Let a = shift_sint32(p, 0).
Let x = 1 + n. Let x = 1 + n.
Assume { Assume {
...@@ -121,8 +208,8 @@ Prove: (n <= 0) \/ included(a, x, shift_sint32(p, 1), n - 1) \/ ...@@ -121,8 +208,8 @@ Prove: (n <= 0) \/ included(a, x, shift_sint32(p, 1), n - 1) \/
------------------------------------------------------------ ------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 72) in 'PARTIAL_ASSIGNS': Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 77) in 'PARTIAL_ASSIGNS_VARS':
Call Effect at line 74 Call Effect at line 79
Let a = shift_sint32(p, 0). Let a = shift_sint32(p, 0).
Let x = 1 + n. Let x = 1 + n.
Assume { Assume {
...@@ -138,6 +225,84 @@ Assume { ...@@ -138,6 +225,84 @@ Assume {
Prove: (n <= 0) \/ included(a, x, shift_sint32(p, 1), n - 1) \/ Prove: (n <= 0) \/ included(a, x, shift_sint32(p, 1), n - 1) \/
included(a, x, shift_sint32(p, n), 1). included(a, x, shift_sint32(p, n), 1).
------------------------------------------------------------
------------------------------------------------------------
Function RANGE_NESTED_ARRAY_STATIC
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 104) in 'RANGE_NESTED_ARRAY_STATIC':
Call Effect at line 109
Assume {
(* Heap *)
Type: (region(s.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: !invalid(Malloc_0, shift_S2_With_array(s, 0), 12).
}
Prove: false.
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 104) in 'RANGE_NESTED_ARRAY_STATIC':
Call Effect at line 109
Assume {
(* Heap *)
Type: (region(s.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: !invalid(Malloc_0, shift_S2_With_array(s, 0), 12).
}
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function RANGE_NESTED_ARRAY_VARS
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 113) in 'RANGE_NESTED_ARRAY_VARS':
Call Effect at line 118
Let a = shift_S2_With_array(s, 0).
Let x = 4 * n.
Let x_1 = 4 + x.
Let a_1 = shift_S2_With_array(s, 1).
Let a_2 = shiftfield_F2_With_array_t(a).
Assume {
Type: is_uint32(m) /\ is_uint32(n).
(* Heap *)
Type: (region(s.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: !invalid(Malloc_0, a, x_1).
(* Pre-condition *)
Have: (3 <= n) /\ (4 <= m).
}
Prove: (n < 0) \/ included(a, x_1, shift_S2_With_array(s, 2), x - 4) \/
included(a, x_1, shiftfield_F2_With_array_x(a_1), 1) \/
included(a, x_1, shift_sint32(a_2, 0), 1) \/
included(a, x_1, shift_sint32(a_2, 1), m) \/
included(a, x_1, shift_sint32(shiftfield_F2_With_array_t(a_1), 0), 1 + m).
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 113) in 'RANGE_NESTED_ARRAY_VARS':
Call Effect at line 118
Let a = shift_S2_With_array(s, 0).
Let x = 4 * n.
Let x_1 = 4 + x.
Let a_1 = shift_S2_With_array(s, 1).
Let a_2 = shiftfield_F2_With_array_t(a).
Assume {
Type: is_uint32(m) /\ is_uint32(n).
(* Heap *)
Type: (region(s.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: !invalid(Malloc_0, a, x_1).
(* Pre-condition *)
Have: (3 <= n) /\ (4 <= m).
}
Prove: (n < 0) \/ included(a, x_1, shift_S2_With_array(s, 2), x - 4) \/
included(a, x_1, shiftfield_F2_With_array_x(a_1), 1) \/
included(a, x_1, shift_sint32(a_2, 0), 1) \/
included(a, x_1, shift_sint32(a_2, 1), m) \/
included(a, x_1, shift_sint32(shiftfield_F2_With_array_t(a_1), 0), 1 + m).
------------------------------------------------------------ ------------------------------------------------------------
------------------------------------------------------------ ------------------------------------------------------------
Function USE_ASSIGN_UNFOLD_KO Function USE_ASSIGN_UNFOLD_KO
......
src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
+ 154
− 5
View file @ 150618d5
...@@ -19,6 +19,56 @@ Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 56) in 'ASSIGN_NO_UNFO ...@@ -19,6 +19,56 @@ Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 56) in 'ASSIGN_NO_UNFO
Effect at line 59 Effect at line 59
Prove: true. Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function NESTED_ARRAY_STATIC
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 90) in 'NESTED_ARRAY_STATIC':
Call Effect at line 92
Prove: true.
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 90) in 'NESTED_ARRAY_STATIC':
Call Effect at line 92
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function NESTED_ARRAY_VARS
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 96) in 'NESTED_ARRAY_VARS':
Call Effect at line 98
Let a = shiftfield_F2_With_array_t(s).
Assume {
Type: is_uint32(n).
(* Heap *)
Type: (region(s.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: !invalid(Malloc_0, s, 4).
(* Pre-condition *)
Have: 3 <= n.
}
Prove: (0 < n) /\ included(shift_sint32(a, 2), 1, shift_sint32(a, 1), n).
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 96) in 'NESTED_ARRAY_VARS':
Call Effect at line 98
Let a = shiftfield_F2_With_array_t(s).
Assume {
Type: is_uint32(n).
(* Heap *)
Type: (region(s.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: !invalid(Malloc_0, s, 4).
(* Pre-condition *)
Have: 3 <= n.
}
Prove: (0 < n) /\ included(shift_sint32(a, 2), 1, shift_sint32(a, 1), n).
------------------------------------------------------------ ------------------------------------------------------------
------------------------------------------------------------ ------------------------------------------------------------
Function NO_UNFOLD_KO Function NO_UNFOLD_KO
...@@ -81,11 +131,26 @@ Prove: true. ...@@ -81,11 +131,26 @@ Prove: true.
------------------------------------------------------------ ------------------------------------------------------------
------------------------------------------------------------ ------------------------------------------------------------
Function PARTIAL_ASSIGNS Function PARTIAL_ASSIGNS_STATIC
------------------------------------------------------------ ------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 72) in 'PARTIAL_ASSIGNS': Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 71) in 'PARTIAL_ASSIGNS_STATIC':
Call Effect at line 74 Call Effect at line 73
Prove: true.
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 71) in 'PARTIAL_ASSIGNS_STATIC':
Call Effect at line 73
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function PARTIAL_ASSIGNS_VARS
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 77) in 'PARTIAL_ASSIGNS_VARS':
Call Effect at line 79
Assume { Assume {
Type: is_uint32(n). Type: is_uint32(n).
(* Heap *) (* Heap *)
...@@ -101,8 +166,8 @@ Prove: (i = 0) \/ (n = i) \/ ...@@ -101,8 +166,8 @@ Prove: (i = 0) \/ (n = i) \/
------------------------------------------------------------ ------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 72) in 'PARTIAL_ASSIGNS': Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 77) in 'PARTIAL_ASSIGNS_VARS':
Call Effect at line 74 Call Effect at line 79
Assume { Assume {
Type: is_uint32(n). Type: is_uint32(n).
(* Heap *) (* Heap *)
...@@ -116,6 +181,90 @@ Assume { ...@@ -116,6 +181,90 @@ Assume {
Prove: (i = 0) \/ (n = i) \/ Prove: (i = 0) \/ (n = i) \/
included(shift_sint32(p, i), 1, shift_sint32(p, 1), n - 1). included(shift_sint32(p, i), 1, shift_sint32(p, 1), n - 1).
------------------------------------------------------------
------------------------------------------------------------
Function RANGE_NESTED_ARRAY_STATIC
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 104) in 'RANGE_NESTED_ARRAY_STATIC':
Call Effect at line 109
Prove: true.
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 104) in 'RANGE_NESTED_ARRAY_STATIC':
Call Effect at line 109
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function RANGE_NESTED_ARRAY_VARS
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 113) in 'RANGE_NESTED_ARRAY_VARS':
Call Effect at line 118
Let a = shift_S2_With_array(s, 0).
Let x = 4 * n.
Let a_1 = shift_S2_With_array(s, i).
Let a_2 = shiftfield_F2_With_array_t(a_1).
Let a_3 = shift_sint32(a_2, 1).
Let a_4 = shift_S2_With_array(s, 2).
Let x_1 = x - 4.
Let a_5 = shift_sint32(shiftfield_F2_With_array_t(a), 1).
Let a_6 = shift_sint32(shiftfield_F2_With_array_t(shift_S2_With_array(s, 1)),
0).
Let x_2 = 1 + m.
Let a_7 = shift_sint32(a_2, 2).
Let a_8 = shiftfield_F2_With_array_x(a_1).
Assume {
Type: is_uint32(m) /\ is_uint32(n).
(* Heap *)
Type: (region(s.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: (0 <= i) /\ (i <= n) /\ (!invalid(Malloc_0, a, 4 + x)).
(* Pre-condition *)
Have: (3 <= n) /\ (4 <= m).
}
Prove: (included(a_3, 1, a_4, x_1) \/ included(a_3, 1, a_5, m) \/
included(a_3, 1, a_6, x_2)) /\
(included(a_7, 1, a_4, x_1) \/ included(a_7, 1, a_5, m) \/
included(a_7, 1, a_6, x_2)) /\
((i = 0) \/ (i = 1) \/ included(a_8, 1, a_4, x_1) \/
included(a_8, 1, a_5, m) \/ included(a_8, 1, a_6, x_2)).
------------------------------------------------------------
Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 113) in 'RANGE_NESTED_ARRAY_VARS':
Call Effect at line 118
Let a = shift_S2_With_array(s, 0).
Let x = 4 * n.
Let a_1 = shift_S2_With_array(s, i).
Let a_2 = shiftfield_F2_With_array_t(a_1).
Let a_3 = shift_sint32(a_2, 1).
Let a_4 = shift_S2_With_array(s, 2).
Let x_1 = x - 4.
Let a_5 = shift_sint32(shiftfield_F2_With_array_t(a), 1).
Let a_6 = shift_sint32(shiftfield_F2_With_array_t(shift_S2_With_array(s, 1)),
0).
Let x_2 = 1 + m.
Let a_7 = shift_sint32(a_2, 2).
Let a_8 = shiftfield_F2_With_array_x(a_1).
Assume {
Type: is_uint32(m) /\ is_uint32(n).
(* Heap *)
Type: (region(s.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: (0 <= i) /\ (i <= n) /\ (!invalid(Malloc_0, a, 4 + x)).
(* Pre-condition *)
Have: (3 <= n) /\ (4 <= m).
}
Prove: (included(a_3, 1, a_4, x_1) \/ included(a_3, 1, a_5, m) \/
included(a_3, 1, a_6, x_2)) /\
(included(a_7, 1, a_4, x_1) \/ included(a_7, 1, a_5, m) \/
included(a_7, 1, a_6, x_2)) /\
((i = 0) \/ (i = 1) \/ included(a_8, 1, a_4, x_1) \/
included(a_8, 1, a_5, m) \/ included(a_8, 1, a_6, x_2)).
------------------------------------------------------------ ------------------------------------------------------------
------------------------------------------------------------ ------------------------------------------------------------
Function USE_ASSIGN_UNFOLD_KO Function USE_ASSIGN_UNFOLD_KO
......
src/plugins/wp/tests/wp_plugin/unfold_assigns.i
+ 47
− 3
View file @ 150618d5
...@@ -66,10 +66,54 @@ void ASSIGN_NO_UNFOLD_KO(struct S *s) { ...@@ -66,10 +66,54 @@ void ASSIGN_NO_UNFOLD_KO(struct S *s) {
} }
/*@ assigns *(p+(0..n)); */ /*@ assigns *(p+(0..n)); */
void f_assigns_array(int *p, unsigned n); void f_assigns_range(int *p, unsigned n);
/*@ assigns *(p+0), *(p+(1..3)), *(p+4); */
void PARTIAL_ASSIGNS_STATIC(int *p) {
f_assigns_range(p, 4);
}
/*@ requires n > 4 ; /*@ requires n > 4 ;
assigns *(p+0), *(p+(1..n-1)), *(p+n); */ assigns *(p+0), *(p+(1..n-1)), *(p+n); */
void PARTIAL_ASSIGNS(int *p, unsigned n) { void PARTIAL_ASSIGNS_VARS(int *p, unsigned n) {
f_assigns_array(p, n); f_assigns_range(p, n);
}
struct With_array {
int x ;
int t [3] ;
};
//@ assigns *s ;
void f_assigns_with_array(struct With_array* s);
//@ assigns s->x, s->t[0], s->t[1..2] ;
void NESTED_ARRAY_STATIC(struct With_array *s){
f_assigns_with_array(s);
}
/*@ requires n > 2 ;
assigns s->x, s->t[0], s->t[1..n] ; */
void NESTED_ARRAY_VARS(struct With_array *s, unsigned n){
f_assigns_with_array(s);
}
//@ assigns *(s+(0..n)) ;
void f_assigns_range_with_array(struct With_array* s, unsigned n);
/*@ assigns s[0].x, s[0].t[0], s[0].t[1..2],
s[1].x, s[1].t[0..2],
s[2];
*/
void RANGE_NESTED_ARRAY_STATIC(struct With_array* s){
f_assigns_range_with_array(s, 2);
}
/*@ requires n > 2 && m > 3 ;
assigns s[0].x, s[0].t[0], s[0].t[1..m],
s[1].x, s[1].t[0..m],
s[2 .. n];
*/
void RANGE_NESTED_ARRAY_VARS(struct With_array* s, unsigned n, unsigned m){
f_assigns_range_with_array(s, n);
} }
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