Skip to content
Snippets Groups Projects
Commit 76b5af6d authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] naming pre-conditions

parent 16c7e68e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 173 additions and 100 deletions
src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
+ 18
− 6
View file @ 76b5af6d
......@@ -17,7 +17,9 @@ Assume {
(* Goal *)
When: (0 <= i_1) /\ (i_1 < n).
(* Pre-condition *)
Have: (0 <= n) /\ separated(a_1, n, shift_sint32(b, 0), n).
Have: 0 <= n.
(* Pre-condition *)
Have: separated(a_1, n, shift_sint32(b, 0), n).
(* Invariant 'Copy' *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_2[shift_sint32(b, i_2)] = a_2[shift_sint32(a, i_2)]))).
......@@ -41,7 +43,9 @@ Assume {
(* Goal *)
When: (0 <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: (0 <= n) /\ separated(a_1, n, shift_sint32(b, 0), n).
Have: 0 <= n.
(* Pre-condition *)
Have: separated(a_1, n, shift_sint32(b, 0), n).
(* Invariant 'Copy' *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_2[shift_sint32(b, i_2)] = a_2[shift_sint32(a, i_2)]))).
......@@ -74,7 +78,9 @@ Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
(* Pre-condition *)
Have: (0 <= n) /\ separated(a_1, n, shift_sint32(b, 0), n).
Have: 0 <= n.
(* Pre-condition *)
Have: separated(a_1, n, shift_sint32(b, 0), n).
(* Invariant 'Copy' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
(a_2[shift_sint32(b, i_1)] = a_2[shift_sint32(a, i_1)]))).
......@@ -109,7 +115,9 @@ Assume {
(* Goal *)
When: (0 <= i_1) /\ (i_1 < i).
(* Pre-condition *)
Have: (0 <= n) /\ separated(a_1, n, shift_sint32(b, 0), n).
Have: 0 <= n.
(* Pre-condition *)
Have: separated(a_1, n, shift_sint32(b, 0), n).
(* Invariant 'Copy' *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_2[shift_sint32(b, i_2)] = a_2[shift_sint32(a, i_2)]))).
......@@ -134,7 +142,9 @@ Assume {
(* Goal *)
When: (0 <= i_1) /\ (i_1 < i).
(* Pre-condition *)
Have: (0 <= n) /\ separated(a_1, n, shift_sint32(b, 0), n).
Have: 0 <= n.
(* Pre-condition *)
Have: separated(a_1, n, shift_sint32(b, 0), n).
(* Invariant 'Copy' *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_2[shift_sint32(b, i_2)] = a_2[shift_sint32(a, i_2)]))).
......@@ -174,7 +184,9 @@ Assume {
(* Goal *)
When: !invalid(Malloc_0, a_3, 1).
(* Pre-condition *)
Have: (0 <= n) /\ separated(a_1, n, shift_sint32(b, 0), n).
Have: 0 <= n.
(* Pre-condition *)
Have: separated(a_1, n, shift_sint32(b, 0), n).
(* Invariant 'Copy' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
(a_2[shift_sint32(b, i_1)] = a_2[shift_sint32(a, i_1)]))).
......
src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
+ 18
− 6
View file @ 76b5af6d
......@@ -17,7 +17,9 @@ Assume {
(* Goal *)
When: (i_1 <= b) /\ (a <= i_1) /\ is_sint32(i_1).
(* Pre-condition *)
Have: (a <= b) /\ valid_rw(Malloc_0, a_1, 1 + b - a).
Have: valid_rw(Malloc_0, a_1, 1 + b - a).
(* Pre-condition *)
Have: a <= b.
(* Invariant 'qed_ok' *)
Have: forall i_2 : Z. ((a <= i_2) -> ((i_2 < i) ->
(a_2[shift_sint32(t, i_2)] = e))).
......@@ -39,7 +41,9 @@ Assume {
(* Heap *)
Type: (region(t.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
Have: (a <= b) /\ valid_rw(Malloc_0, a_1, 1 + b - a).
Have: valid_rw(Malloc_0, a_1, 1 + b - a).
(* Pre-condition *)
Have: a <= b.
(* Invariant 'qed_ok' *)
Have: forall i_1 : Z. ((a <= i_1) -> ((i_1 < i) ->
(havoc(Mint_undef_0, Mint_0, a_1, i - a)[shift_sint32(t, i_1)] = e))).
......@@ -58,7 +62,9 @@ Assume {
(* Heap *)
Type: (region(t.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
Have: (a <= b) /\ valid_rw(Malloc_0, shift_sint32(t, a), 1 + b - a).
Have: valid_rw(Malloc_0, shift_sint32(t, a), 1 + b - a).
(* Pre-condition *)
Have: a <= b.
}
Prove: a <= (1 + b).
......@@ -75,7 +81,9 @@ Assume {
(* Goal *)
When: (a <= i_1) /\ (i_1 <= i) /\ is_sint32(i_1).
(* Pre-condition *)
Have: (a <= b) /\ valid_rw(Malloc_0, a_1, 1 + b - a).
Have: valid_rw(Malloc_0, a_1, 1 + b - a).
(* Pre-condition *)
Have: a <= b.
(* Invariant 'qed_ok' *)
Have: forall i_2 : Z. ((a <= i_2) -> ((i_2 < i) ->
(a_2[shift_sint32(t, i_2)] = e))).
......@@ -116,7 +124,9 @@ Assume {
(* Goal *)
When: !invalid(Malloc_0, a_2, 1).
(* Pre-condition *)
Have: (a <= b) /\ valid_rw(Malloc_0, a_1, 1 + b - a).
Have: valid_rw(Malloc_0, a_1, 1 + b - a).
(* Pre-condition *)
Have: a <= b.
(* Invariant 'qed_ok' *)
Have: forall i_1 : Z. ((a <= i_1) -> ((i_1 < i) ->
(havoc(Mint_undef_0, Mint_0, a_1, i - a)[shift_sint32(t, i_1)] = e))).
......@@ -140,7 +150,9 @@ Assume {
(* Heap *)
Type: (region(t.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
Have: (a <= b) /\ valid_rw(Malloc_0, a_1, 1 + b - a).
Have: valid_rw(Malloc_0, a_1, 1 + b - a).
(* Pre-condition *)
Have: a <= b.
}
Prove: i <= (1 + b).
......
src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle
+ 15
− 5
View file @ 76b5af6d
......@@ -20,7 +20,9 @@ Assume {
(* Heap *)
Type: is_sint32(calls_0).
(* Pre-condition *)
Have: (L_sequence(calls_0) = nil) /\ (0 <= n).
Have: 0 <= n.
(* Pre-condition *)
Have: L_sequence(calls_0) = nil.
(* Invariant *)
Have: ([ 1, 2 ] *^ i) = a.
(* Invariant *)
......@@ -51,7 +53,9 @@ Assume {
(* Heap *)
Type: is_sint32(calls_1).
(* Pre-condition *)
Have: (L_sequence(calls_1) = nil) /\ (0 <= n).
Have: 0 <= n.
(* Pre-condition *)
Have: L_sequence(calls_1) = nil.
(* Invariant *)
Have: (a_2 *^ i) = a.
(* Invariant *)
......@@ -124,7 +128,9 @@ Assume {
(* Heap *)
Type: is_sint32(calls_0).
(* Pre-condition *)
Have: (L_sequence(calls_0) = nil) /\ (0 <= n).
Have: 0 <= n.
(* Pre-condition *)
Have: L_sequence(calls_0) = nil.
(* Call 'f' *)
Have: L_sequence(calls_1) = [ 1 ].
(* Invariant *)
......@@ -147,7 +153,9 @@ Assume {
(* Heap *)
Type: is_sint32(calls_0).
(* Pre-condition *)
Have: (L_sequence(calls_0) = nil) /\ (0 <= n).
Have: 0 <= n.
(* Pre-condition *)
Have: L_sequence(calls_0) = nil.
(* Call 'f' *)
Have: L_sequence(calls_1) = [ 1 ].
(* Invariant *)
......@@ -180,7 +188,9 @@ Assume {
(* Heap *)
Type: is_sint32(calls_0).
(* Pre-condition *)
Have: (L_sequence(calls_0) = nil) /\ (0 <= n).
Have: 0 <= n.
(* Pre-condition *)
Have: L_sequence(calls_0) = nil.
(* Call 'f' *)
Have: L_sequence(calls_1) = [ 1 ].
(* Invariant *)
......
src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
+ 5
− 5
View file @ 76b5af6d
......@@ -278,7 +278,7 @@ Goal Post-condition 'ok,m2' in 'no_calls':
Assume {
(* Heap *)
Type: is_sint32(call_seq_0).
(* Pre-condition *)
(* Pre-condition 'init' *)
Have: L_call_obs(call_seq_0) = nil.
}
Prove: length(L_call_nil) = 0.
......@@ -294,7 +294,7 @@ Goal Post-condition 'ok,n2' in 'no_calls':
Assume {
(* Heap *)
Type: is_sint32(call_seq_0).
(* Pre-condition *)
(* Pre-condition 'init' *)
Have: L_call_obs(call_seq_0) = nil.
}
Prove: L_call_nil = nil.
......@@ -305,7 +305,7 @@ Goal Post-condition 'ok,n3' in 'no_calls':
Assume {
(* Heap *)
Type: is_sint32(call_seq_0).
(* Pre-condition *)
(* Pre-condition 'init' *)
Have: L_call_obs(call_seq_0) = nil.
}
Prove: L_call_nil = nil.
......@@ -319,7 +319,7 @@ Assume {
Type: is_sint32(call_seq_0).
(* Goal *)
When: 0 <= a.
(* Pre-condition *)
(* Pre-condition 'init' *)
Have: L_call_obs(call_seq_0) = nil.
}
Prove: (L_call_nil = nil) \/ (a <= 0).
......@@ -336,7 +336,7 @@ Assume {
Type: is_sint32(a).
(* Heap *)
Type: is_sint32(call_seq_0).
(* Pre-condition *)
(* Pre-condition 'init' *)
Have: L_call_obs(call_seq_0) = nil.
}
Prove: (L_call_nil = nil) \/ (a <= 0).
......
src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
+ 96
− 69
View file @ 76b5af6d
......@@ -11,10 +11,12 @@ Assume {
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n) /\
separated(a, n, shift_sint8(src_0, 0), n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, dest_0, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, src_0, n).
(* Pre-condition 'separation' *)
Have: separated(a, n, shift_sint8(src_0, 0), n).
(* Invariant 'no_eva' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
(a_1[shift_sint8(src_0, i_1)] = a_1[shift_sint8(dest_0, i_1)]))).
......@@ -41,10 +43,12 @@ Assume {
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n) /\
separated(a, n, shift_sint8(src_0, 0), n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, dest_0, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, src_0, n).
(* Pre-condition 'separation' *)
Have: separated(a, n, shift_sint8(src_0, 0), n).
(* Invariant 'no_eva' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
(a_1[shift_sint8(src_0, i_1)] = a_1[shift_sint8(dest_0, i_1)]))).
......@@ -63,10 +67,12 @@ Assume {
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n) /\
separated(shift_sint8(dest_0, 0), n, shift_sint8(src_0, 0), n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, dest_0, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, src_0, n).
(* Pre-condition 'separation' *)
Have: separated(shift_sint8(dest_0, 0), n, shift_sint8(src_0, 0), n).
}
Prove: 0 <= n.
......@@ -83,10 +89,12 @@ Assume {
linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
When: (0 <= i_1) /\ (i_1 < to_uint64(1 + i)).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n) /\
separated(a, n, shift_sint8(src_0, 0), n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, dest_0, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, src_0, n).
(* Pre-condition 'separation' *)
Have: separated(a, n, shift_sint8(src_0, 0), n).
(* Invariant 'no_eva' *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_1[shift_sint8(src_0, i_2)] = a_1[shift_sint8(dest_0, i_2)]))).
......@@ -127,10 +135,12 @@ Assume {
linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
When: !invalid(Malloc_0, a_2, 1).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n) /\
separated(a, n, shift_sint8(src_0, 0), n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, dest_0, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, src_0, n).
(* Pre-condition 'separation' *)
Have: separated(a, n, shift_sint8(src_0, 0), n).
(* Invariant 'no_eva' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
(a_1[shift_sint8(src_0, i_1)] = a_1[shift_sint8(dest_0, i_1)]))).
......@@ -157,10 +167,12 @@ Assume {
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n) /\
separated(a, n, shift_sint8(src_0, 0), n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, dest_0, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, src_0, n).
(* Pre-condition 'separation' *)
Have: separated(a, n, shift_sint8(src_0, 0), n).
(* Invariant 'no_eva' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
(a_1[shift_sint8(src_0, i_1)] = a_1[shift_sint8(dest_0, i_1)]))).
......@@ -185,9 +197,10 @@ Assume {
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, dest_0, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, src_0, n).
If n = 0
Then { Have: Mchar_1 = Mchar_0. }
Else {
......@@ -256,9 +269,10 @@ Assume {
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, dest_0, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, src_0, n).
(* Else *)
Have: n != 0.
(* Call 'memoverlap' *)
......@@ -291,9 +305,10 @@ Assume {
Type: is_sint32(memoverlap_0) /\ is_uint64(n).
(* Heap *)
Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, d, n) /\
P_valid_read_or_empty(Malloc_0, s, n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, d, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, s, n).
(* Else *)
Have: n != 0.
(* Call 'memoverlap' *)
......@@ -320,9 +335,10 @@ Assume {
sconst(Mchar_0).
(* Goal *)
When: (0 <= i_1) /\ (i_1 < to_uint64(1 + i)).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, d, n) /\
P_valid_read_or_empty(Malloc_0, s, n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, d, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, s, n).
(* Else *)
Have: n != 0.
(* Call 'memoverlap' *)
......@@ -366,9 +382,10 @@ Assume {
sconst(Mchar_0).
(* Goal *)
When: (i_1 < n) /\ (to_uint64(1 + i) <= i_1).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, d, n) /\
P_valid_read_or_empty(Malloc_0, s, n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, d, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, s, n).
(* Else *)
Have: n != 0.
(* Call 'memoverlap' *)
......@@ -408,9 +425,10 @@ Assume {
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, dest_0, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, src_0, n).
(* Else *)
Have: n != 0.
(* Call 'memoverlap' *)
......@@ -443,9 +461,10 @@ Assume {
Type: is_sint32(memoverlap_0) /\ is_uint64(n).
(* Heap *)
Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, d, n) /\
P_valid_read_or_empty(Malloc_0, s, n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, d, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, s, n).
(* Else *)
Have: n != 0.
(* Call 'memoverlap' *)
......@@ -472,9 +491,10 @@ Assume {
sconst(Mchar_0).
(* Goal *)
When: (i_1 < n) /\ (to_uint64(i - 1) < i_1).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, d, n) /\
P_valid_read_or_empty(Malloc_0, s, n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, d, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, s, n).
(* Else *)
Have: n != 0.
(* Call 'memoverlap' *)
......@@ -511,9 +531,10 @@ Assume {
linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
When: (i < n) /\ (to_uint64(n - 1) < i).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, dest_0, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, src_0, n).
(* Else *)
Have: n != 0.
(* Call 'memoverlap' *)
......@@ -541,9 +562,10 @@ Assume {
sconst(Mchar_0).
(* Goal *)
When: (0 <= i_1) /\ (i_1 <= to_uint64(i - 1)).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, d, n) /\
P_valid_read_or_empty(Malloc_0, s, n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, d, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, s, n).
(* Else *)
Have: n != 0.
(* Call 'memoverlap' *)
......@@ -598,9 +620,10 @@ Assume {
linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
When: !invalid(Malloc_0, a_3, 1).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, d, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, d, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, src_0, n).
(* Else *)
Have: n != 0.
(* Call 'memoverlap' *)
......@@ -650,9 +673,10 @@ Assume {
linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
When: !invalid(Malloc_0, a_3, 1).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, d, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, d, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, src_0, n).
(* Else *)
Have: n != 0.
(* Call 'memoverlap' *)
......@@ -724,9 +748,10 @@ Assume {
linked(Malloc_0) /\ sconst(Mchar_0).
(* Goal *)
When: !invalid(Malloc_0, a, 1).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, d, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, d, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, src_0, n).
(* Else *)
Have: n != 0.
(* Call 'memoverlap' *)
......@@ -767,9 +792,10 @@ Assume {
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, dest_0, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, src_0, n).
(* Else *)
Have: n != 0.
(* Call 'memoverlap' *)
......@@ -809,9 +835,10 @@ Assume {
(* Heap *)
Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
linked(Malloc_0) /\ sconst(Mchar_0).
(* Pre-condition *)
Have: P_valid_or_empty(Malloc_0, dest_0, n) /\
P_valid_read_or_empty(Malloc_0, src_0, n).
(* Pre-condition 'valid_dest' *)
Have: P_valid_or_empty(Malloc_0, dest_0, n).
(* Pre-condition 'valid_src' *)
Have: P_valid_read_or_empty(Malloc_0, src_0, n).
(* Else *)
Have: n != 0.
(* Call 'memoverlap' *)
......
src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle
+ 1
− 1
View file @ 76b5af6d
......@@ -13,7 +13,7 @@ Let a = shift_uint32(t, 0).
Assume {
(* Heap *)
Type: (region(t.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
(* Pre-condition 'access' *)
Have: valid_rw(Malloc_0, a, 16).
}
Prove: P_zeroed(Mint_0[a <- 0][shift_uint32(t, 1) <- 0][shift_uint32(t, 2)
......
src/plugins/wp/tests/wp_store/oracle/nonaliasing.res.oracle
+ 20
− 8
View file @ 76b5af6d
......@@ -22,8 +22,11 @@ Assume {
(* Goal *)
When: q != p.
(* Pre-condition *)
Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 199) /\ (x_1 <= 199) /\
valid_rw(Malloc_0, p, 1) /\ valid_rw(Malloc_0, q, 1).
Have: valid_rw(Malloc_0, p, 1).
(* Pre-condition *)
Have: valid_rw(Malloc_0, q, 1).
(* Pre-condition *)
Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 199) /\ (x_1 <= 199).
}
Prove: x_5 = x_2.
......@@ -43,8 +46,11 @@ Assume {
(* Goal *)
When: q != p.
(* Pre-condition *)
Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 199) /\ (x_1 <= 199) /\
valid_rw(Malloc_0, p, 1) /\ valid_rw(Malloc_0, q, 1).
Have: valid_rw(Malloc_0, p, 1).
(* Pre-condition *)
Have: valid_rw(Malloc_0, q, 1).
(* Pre-condition *)
Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 199) /\ (x_1 <= 199).
}
Prove: x_2 = x_1.
......@@ -64,8 +70,11 @@ Assume {
(* Heap *)
Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 199) /\ (x_1 <= 199) /\
valid_rw(Malloc_0, p, 1) /\ valid_rw(Malloc_0, q, 1).
Have: valid_rw(Malloc_0, p, 1).
(* Pre-condition *)
Have: valid_rw(Malloc_0, q, 1).
(* Pre-condition *)
Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 199) /\ (x_1 <= 199).
}
Prove: x_5 = x_2.
......@@ -83,8 +92,11 @@ Assume {
(* Heap *)
Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 199) /\ (x_1 <= 199) /\
valid_rw(Malloc_0, p, 1) /\ valid_rw(Malloc_0, q, 1).
Have: valid_rw(Malloc_0, p, 1).
(* Pre-condition *)
Have: valid_rw(Malloc_0, q, 1).
(* Pre-condition *)
Have: (0 <= x) /\ (0 <= x_1) /\ (x <= 199) /\ (x_1 <= 199).
}
Prove: x_2 = x_1.
......
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