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

[wp] reverted post-validity

parent 474f91e0
No related branches found
No related tags found
No related merge requests found
......@@ -34,5 +34,9 @@ Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'receive':
/*@ behavior typed: requires \separated(&size,message+(..)); */
/*@
behavior typed:
requires \separated(message + (..), &size);
requires \separated(message + (0 .. \at(size,Post)), &size);
*/
void receive(int n, char *message);
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