On the prototype of recv()

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

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 <= \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?