On the prototype of recv()Pascal Cuoq - 20th Jun 2013
man recv on my system, I get:
ssize_t recv(int socket, void *buffer, size_t length, int flags);
The man page contains this additional bit of specification: “These calls return the number of bytes received, or -1 if an error occurred.”
ssize_tis defined as a signed variant of
size_t. “Is that not what
ptrdiff_tis for?”, you may ask. Jonathan Leffler was wondering about this very question during the last days of 2011. I am unsure of the answers conclusiveness: on 32-bit platforms that let
malloc()create objects of more than 2GiB
ptrdiff_tis generally 32-bit wide although it should be wider by the same reasoning applied in the accepted answer and in some of its comments.
recv() may return
-1 in case of error is probably the reason for the result of
recv() being of the signed type
ssize_t. Fair enough. Now let us write a bit of formal specification to go with
/*@ … ensures -1 <= \esult <= length ; */
The unimpeachable logic here is that since function
recv() is well-written not to overflow the buffer passed to it the number of bytes received can only be lower than the number of bytes it was allowed to write. Or naturally it can be
-1 in case of error.
Question: what is strange about the above post-condition?