select()'s contract assigns {read,write,error}fds arguments even if they are NULL pointers
My understanding is that select()
accepts NULL
pointers for any of the fd_set*
argument.
POSIX 2008 states "If the name
argument is not a null pointer," for name in {readfds
, writefds
, errorfds
}. The manual page for select on my system also states this is allowed: "Each of the fd_set
arguments may be specified as NULL
if no file descriptors are to be watched for the corresponding class of events."
The select()
contract in Frama-C's libc has an unconditional assigns
clause for these arguments:
assigns *readfds, *writefds, *errorfds, *timeout, \result
This means that a function calling select()
with a NULL
pointer for any of the fd_set*
argument, is unable to prove an assigns
clause, unless it contains *(fd_set*)0
.
Could the select()
contract be updated to reflect this case?