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

[wp] Update tests oracles

parent cfe2a65d
No related branches found
No related tags found
No related merge requests found
......@@ -36,6 +36,6 @@ Prove: true.
/*@
behavior typed:
requires \separated(message + (..), &size);
requires \separated(message + (0 .. \at(size,Post)), &size);
ensures \separated(message + (0 .. \at(size,Post)), &size);
*/
void receive(int n, char *message);
......@@ -59,3 +59,7 @@ Assume {
Prove: !valid_rw(Malloc_0[L_y_25 <- 0], a, 1).
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'h':
/*@ behavior typed:
ensures \separated(\result, &x); */
int *h(int x);
......@@ -59,3 +59,7 @@ Assume {
Prove: !valid_rw(Malloc_0[L_y_25 <- 0], a, 1).
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'h':
/*@ behavior typed_ref:
ensures \separated(\result, &x); */
int *h(int x);
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment