...
 
Commits (3)
......@@ -2,6 +2,7 @@
*.sav
*.o
*~
\#*
config.status
lia.cache
......
#include <stdlib.h>
int cgc_receive_bytes_iPcz (char *buffer, size_t count)
{
size_t total;
size_t rxbytes;
total = 0;
while(total < count) {
rxbytes = 0;
if (cgc_receive(STDIN, buffer+total, count-total, &rxbytes)==0 ) {
if (rxbytes == 0)
return(0);
else
total += rxbytes;
}
else {
return(-1);
}
}
return 0;
}
#include <stdlib.h>
#include <stdint.h>
// models the network state/data
volatile int __network;
// models some error (for non-deterministic assumes)
volatile int __error;
/*
requires \valid(buffer+(0..count-1));
assigns buffer[0..count-1] \from indirect:count, indirect:__network;
assigns \result \from indirect:count, indirect:__network;
behavior ok:
assumes !__error;
assigns buffer[0..count-1] \from indirect:count, indirect:__network;
assigns \result \from indirect:count, indirect:__network;
ensures \initialized(buffer+(0..count-1));
ensures \result == 0;
behavior error:
assumes __error;
assigns buffer[0..count-1] \from indirect:count, indirect:__network;
assigns \result \from indirect:count, indirect:__network;
ensures \result == -1;
disjoint behaviors;
complete behaviors;
*/
//int cgc_receive_bytes_iPcz(char *buffer, size_t count);
/*@
requires \valid(dst+(0..max-1));
assigns dst[0..max-1] \from indirect:delim, indirect:max;
assigns \result \from indirect:delim, indirect:max;
*/
size_t cgc_receive_until_zPccz( char *dst, char delim, size_t max );
int __fc_prng_state;
/*@
assigns __fc_prng_state \from seedValue;
*/
void cgc_seed_prng( uint32_t seedValue );
/*@
assigns \result, __fc_prng_state \from __fc_prng_state;
*/
uint32_t cgc_prng( void );
Subproject commit 5e840bb7060585b81d8fc0d76b3627ca2b8d004d
Subproject commit cf53a987f50b967ce225cab14df90eee77d82fff