Frama-C news and ideas

To content | To menu | To search | Frama-C Home

On the prototype of recv()

Typing man recv on my system, I get:

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.”

The type ssize_t is defined as a signed variant of size_t. “Is that not what ptrdiff_t is 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_t is generally 32-bit wide, although it should be wider by the same reasoning applied in the accepted answer and in some of its comments.

That function 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 recv()'s prototype:

   /*@ … ensures -1 <= \result <= 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?


1. On Friday, June 21 2013, 10:26 by David Mentré

Candidate answer: "length" is of type size_t so unsigned, so the returned value could be of greater size than allowed by \result of type ssize_t (signed). Of course this assumes that size_t and ssize_t are based on the same integer size, e.g. 32 bits. If ssize_t is 64 bits and size_t 32 bits, there is no issue.

2. On Friday, June 21 2013, 11:21 by Ryan Fox

Does your post-condition generate C code that gets added to the program at compile-time? If so, comparing length to -1 is probably not going to work correctly, since length is a size_t and therefore not signed.

3. On Friday, June 21 2013, 14:53 by tobi

A comparison between signed and unsigned? Is that a relevant issue in the context of that precondition?

4. On Friday, June 21 2013, 19:26 by Mansour

The result has an upper bound of SSIZE_MAX, whereas the parameter 'length' has an upper bound of about twice that: SIZE_MAX. If a length of SSIZE_MAX + 1 is successfully written to the buffer, -1 might be returned (on systems where signed overflow results in the modulo).

So your post-condition needs a corresponding pre-condition: 0 <= length <= SSIZE_MAX.

That is why I think ssize_t should not exist. A function should return an error code, and "return" a size by setting a pointer argument, not try to do both at the same time.

5. On Friday, June 21 2013, 19:54 by pascal

David, Ryan, tobi, Mansour:

Hi! This post generated more interest than is usual for this blog. I am going to have the write the sequel then…

In a nutshell, yes, there seems to be an issue if recv() actually takes advantage of the permission it is given to write, say, SSIZE_MAX + 1 bytes. For an actual implementation that never takes advantage of this permission, there is no problem. Mansour's suggested pre-condition guarantees that recv() is never used in conditions where the programmer has to worry about the above. I am tempted to write this pre-condition in Frama-C's libc ACSL specifications.

Finally, I also agree with Mansour on the distastefulness of ssize_t. On the other hand, it is inconvenient to have a function return several results in C (actually recv() is also specified to set errno in case of error, and the -1 return value is redundant with that). For this reason, if it was me, I might specify that recv() returns a size_t, that (size_t)(-1) is the return value corresponding to errors, and that recv() and other functions that accept a size_t argument only accept values in the range 0..SIZE_MAX-1. But I admit this is not a perfect solution either.