It would definitely be worth including something like this in a future

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:


global attribute checkerrno
   oneof maybeset, notset
      setserrno clause ==> maybeset
      resetserrno clause ==> notset
      errnoclear clause ==> notset
      maybeset as notset ==> error
      maybeset + notset ==> maybeset


extern double asin (double x) /*@requires errnoclear@*/ /*@ensures setserrno@*/ ;
extern /*@maynotreturn@*/ void checkError (void) /*@ensures errnoclear@*/ ;


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 --- 10 Feb 2002

testerrno.c: (in function f)
testerrno.c:4:15: Requires clause of called function asin not satisfied
                     is maybeset): requires errnoclear
  exprNode.c:3641: Source code error generation point.
  Transfer violates user-defined state rules. (Use -statetransfer to

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.

Reply via email to