It would definitely be worth including something like this in a future release.
We can approximate it reasonably well with the metastate annotations. The global attribute checkerrno is either maybeset (meaning we have called a function that sets errno, but haven't checked it yet) or notset (meaning we know errno is okay). Then we use /*@requires errnoclear@*/ for functions that might set errno to indicate it must be unset before the call. Here's how: errno.mts: global attribute checkerrno oneof maybeset, notset annotations setserrno clause ==> maybeset resetserrno clause ==> notset errnoclear clause ==> notset preconditions maybeset as notset ==> error merge maybeset + notset ==> maybeset default notset end errno.xh: extern double asin (double x) /*@requires errnoclear@*/ /*@ensures setserrno@*/ ; extern /*@maynotreturn@*/ void checkError (void) /*@ensures errnoclear@*/ ; testerrno.c: double f (double x, double y) { double r1 = asin (x); double r2 = asin (y); /* error: didn't check errno after asin(x) */ return r1 + r2; } splint -mts errno testerrno.c Splint 3.0.1.6 --- 10 Feb 2002 testerrno.c: (in function f) testerrno.c:4:15: Requires clause of called function asin not satisfied (state is maybeset): requires errnoclear exprNode.c:3641: Source code error generation point. Transfer violates user-defined state rules. (Use -statetransfer to inhibit warning) Finished checking --- 1 code warning --- Dave On Mon, 18 Feb 2002, Richard A. O'Keefe wrote: > > With the wonderful new things that Splint can do, I've been thinking > about signal handlers. There are at least three issues: > > (1) A signal handler should not be allowed to call a function unless that > function is known to be safe for such use. The POSIX standard has a > list of functions that are safe for signal handlers. Functions that > have no side effects should also be safe for signal handlers. It > would often be safe for a signal handler to call another signal handler. > > (2) Strictly speaking, a signal handler should not affect any non-local > variables except volatile sigatomic_t ones. A programmer might want > to take responsibility for advising that other types or variables are > OK, but even then such variables should probably be declared volatile. > > (3) The errno variable is not of type sigatomic_t, but a signal handler > that issues a system call may well change it. Other things being > equal, if a signal handler does anything that may modify errno, it > should have > int old_errno = errno; > somewhere before errno is changed, and should set > errno = old_errno; > before any return or longjmp(). > > At a minimum, two annotations 'signal_safe' and 'signal_handler' seem to > be needed. Example: > > extern int /*@signal_safe @modifies errno*/ close(int); > volatile /*@signal_safe@*/ int logfd; > > void /*@signal_handler @modifies logfd@*/ > handle_usr1(int signo) { > int old_errno = errno; > > if (logfd >= 0) close(logfd); > logfd = -1; > errno = old_errno; > } > > Apparently, Splint lets one add new properties like this, but I don't know > how one could integrate the other tests. > >