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