select()'s contract assigns {read,write,error}fds arguments even if they are NULL pointers (#48) · Issues · pub / frama-c

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?

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information