X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/8fe44445b039605d306d64e3919e562081a10881..f6753ca7324b8b367b49a83666614bafaf62d9df:/lib/posix.h diff --git a/lib/posix.h b/lib/posix.h index acb7c1c..2706e2d 100644 --- a/lib/posix.h +++ b/lib/posix.h @@ -92,10 +92,13 @@ struct dirent { extern int closedir (DIR *dirp) /*@modifies errno@*/; -extern /*@null@*/ DIR *opendir (const char *dirname) - /*@modifies errno@*/; + /*drl 1/4/2001 added the dependent annotation as suggested by + Ralf Wildenhues */ + +extern /*@null@*/ /*@dependent@*/ DIR *opendir (const char *dirname) + /*@modifies errno, fileSystem@*/; -extern /*@null@*/ struct dirent *readdir (DIR *dirp) +extern /*@dependent@*/ /*@null@*/ struct dirent *readdir (DIR *dirp) /*@modifies errno@*/; extern void rewinddir (DIR *dirp) @@ -170,20 +173,32 @@ extern void rewinddir (DIR *dirp) /*@constant int SEEK_CUR@*/ /*@constant int SEEK_END@*/ /*@constant int SEEK_SET@*/ -/*@constant int S_IRGRP@*/ -/*@constant int S_IROTH@*/ -/*@constant int S_IUSR@*/ -/*@constant int S_IWXG@*/ -/*@constant int S_IWXO@*/ -/*@constant int S_IWXU@*/ -/*@constant int S_ISGID@*/ -/*@constant int S_ISUID@*/ -/*@constant int S_IWGRP@*/ -/*@constant int S_IWOTH@*/ -/*@constant int S_IWUSR@*/ -/*@constant int S_IXGRP@*/ -/*@constant int S_IXOTH@*/ -/*@constant int S_IXUSR@*/ + +/*@constant mode_t S_IFMT@*/ +/*@constant mode_t S_IFBLK@*/ +/*@constant mode_t S_IFCHR@*/ +/*@constant mode_t S_IFIFO@*/ +/*@constant mode_t S_IFREG@*/ +/*@constant mode_t S_IFDIR@*/ +/*@constant mode_t S_IFLNK@*/ + +/*@constant mode_t S_IRWXU@*/ +/*@constant mode_t S_IRUSR@*/ + +/*@constant mode_t S_IRGRP@*/ +/*@constant mode_t S_IROTH@*/ +/*@constant mode_t S_IUSR@*/ +/*@constant mode_t S_IWXG@*/ +/*@constant mode_t S_IWXO@*/ +/*@constant mode_t S_IWXU@*/ +/*@constant mode_t S_ISGID@*/ +/*@constant mode_t S_ISUID@*/ +/*@constant mode_t S_IWGRP@*/ +/*@constant mode_t S_IWOTH@*/ +/*@constant mode_t S_IWUSR@*/ +/*@constant mode_t S_IXGRP@*/ +/*@constant mode_t S_IXOTH@*/ +/*@constant mode_t S_IXUSR@*/ struct flock { short l_type; @@ -201,7 +216,8 @@ extern int fcntl (int fd, int cmd, ...) extern int open (const char *path, int oflag, ...) /*:checkerror -1 - returns -1 on error */ - /*@modifies errno@*/; + /* the ... is one mode_t param */ + /*@modifies errno@*/ ; /* ** grp.h @@ -213,13 +229,13 @@ struct group { char **gr_mem; }; - extern /*@null@*/ struct group * -getgrgid (gid_t gid) - /*@modifies errno@*/; +/* evans 2002-07-09: added observer annotation (reported by Enrico Scholz). */ - extern /*@null@*/ struct group * -getgrnam (const char *nm) - /*@modifies errno@*/; +/*@observer@*/ /*@null@*/ struct group * getgrgid (gid_t gid) + /*@modifies errno@*/; + +/*@observer@*/ /*@null@*/ struct group *getgrnam (const char *nm) + /*@modifies errno@*/; /* ** limits.h @@ -250,12 +266,12 @@ getgrnam (const char *nm) /*@constant long CHILD_MAX@*/ /*@constant long LINK_MAX@*/ /*@constant long MAX_CANON@*/ -/*@constant long MAX_INPUT@*/ -/*@constant long NAME_MAX@*/ +/*@constant size_t MAX_INPUT@*/ /* evans 2001-10-15 changed type to size_t from long */ +/*@constant size_t NAME_MAX@*/ /* evans 2001-10-15 changed type to size_t from long */ /*@constant long NGROUPS_MAX@*/ /*@constant long OPEN_MAX@*/ -/*@constant long PATH_MAX@*/ -/*@constant long PIPE_BUF@*/ +/*@constant size_t PATH_MAX@*/ /* evans 2001-10-15 changed type to size_t from long */ +/*@constant size_t PIPE_BUF@*/ /* evans 2001-10-15 changed type to size_t from long */ /*@constant long SSIZE_MAX@*/ /*@constant long STREAM_MAX@*/ /*@constant long TZNAME_MAX@*/ @@ -285,13 +301,11 @@ struct passwd { char *pw_shell; } ; - extern /*@observer@*/ /*@null@*/ struct passwd * - getpwnam (const char *) - /*@modifies errno@*/ /*@ensures maxRead(result) == 0 /\ maxSet(result) == 0 @*/; +/*@observer@*/ /*@null@*/ struct passwd *getpwnam (const char *) + /*@modifies errno@*/ /*@ensures maxRead(result) == 0 /\ maxSet(result) == 0 @*/; - extern /*@observer@*/ /*@null@*/ struct passwd * -getpwuid (uid_t uid) - /*@modifies errno@*/ /*@ensures maxRead(result) == 0 /\ maxSet(result) == 0 @*/; +/*@observer@*/ /*@null@*/ struct passwd *getpwuid (uid_t uid) + /*@modifies errno@*/ /*@ensures maxRead(result) == 0 /\ maxSet(result) == 0 @*/; /* ** setjmp.h @@ -299,13 +313,9 @@ getpwuid (uid_t uid) typedef /*@abstract@*/ /*@mutable@*/ void *sigjmp_buf; - extern /*@mayexit@*/ void -siglongjmp (sigjmp_buf env, int val) - /*@*/; +/*@mayexit@*/ void siglongjmp (sigjmp_buf env, int val) /*@*/; - extern int -sigsetjmp (/*@out@*/ sigjmp_buf env, int savemask) - /*@modifies env@*/; +int sigsetjmp (/*@out@*/ sigjmp_buf env, int savemask) /*@modifies env@*/; /* ** signal.h @@ -394,21 +404,6 @@ extern int fileno (FILE *fp) /*@modifies errno@*/; ** sys/stat.h */ -/*@constant int S_IRGRP@*/ -/*@constant int S_IROTH@*/ -/*@constant int S_IUSR@*/ -/*@constant int S_IWXG@*/ -/*@constant int S_IWXO@*/ -/*@constant int S_IWXU@*/ -/*@constant int S_ISGID@*/ -/*@constant int S_ISUID@*/ -/*@constant int S_IWGRP@*/ -/*@constant int S_IWOTH@*/ -/*@constant int S_IWUSR@*/ -/*@constant int S_IXGRP@*/ -/*@constant int S_IXOTH@*/ -/*@constant int S_IXUSR@*/ - struct stat { mode_t st_mode; ino_t st_ino; @@ -429,10 +424,10 @@ struct stat { # ifdef STRICT /*@notfunction@*/ -# define SBOOLINT lltX_bool /*@alt int@*/ +# define SBOOLINT _Bool /*@alt int@*/ # else /*@notfunction@*/ -# define SBOOLINT lltX_bool +# define SBOOLINT _Bool # endif extern SBOOLINT S_ISBLK (/*@sef@*/ mode_t m) /*@*/ ; @@ -508,6 +503,10 @@ extern int WTERMSIG (int status) /*@*/ ; /*@constant int WUNTRACED@*/ +/* These are in Unix spec, are they in POSIX? */ +/*@constant int WCONTINUED@*/ +/*@constant int WNOHANG@*/ + pid_t wait (/*@out@*/ /*@null@*/ int *st) /*@modifies *st, errno, systemState@*/; @@ -692,25 +691,16 @@ tzset (void) /*@constant int _SC_TZNAME_MAX@*/ /*@constant int _SC_VERSION@*/ - extern /*@exits@*/ void -_exit (int status) - /*@*/; +extern /*@exits@*/ void _exit (int status) /*@*/; - extern int -access (const char *path, int mode) - /*@modifies errno@*/; +extern int access (const char *path, int mode) /*@modifies errno@*/; - extern unsigned int -alarm (unsigned int) - /*@modifies systemState@*/; +extern unsigned int alarm (unsigned int) /*@modifies systemState@*/; - extern int -chdir (const char *path) - /*@modifies errno@*/; +extern int chdir (const char *path) /*@modifies errno@*/; - extern int -chown (const char *path, uid_t owner, gid_t group) - /*@modifies fileSystem, errno@*/; +extern int chown (const char *path, uid_t owner, gid_t group) + /*@modifies fileSystem, errno@*/; extern int close (int fd) @@ -766,9 +756,11 @@ fork (void) fpathconf (int fd, int name) /*@modifies errno@*/; - extern char * -getcwd (/*@returned@*/ /*@out@*/ char *buf, size_t size) - /*@modifies errno, *buf@*/; +extern /*@null@*/ char *getcwd (/*@returned@*/ /*@out@*/ /*@notnull@*/ char *buf, size_t size) + /*@requires maxSet(buf) >= (size - 1)@*/ + /*@ensures maxRead(buf) <= (size - 1)@*/ + + /*@modifies errno, *buf@*/ ; extern gid_t getegid (void) @@ -831,7 +823,8 @@ pipe (/*@out@*/ int fd[]) /* Out parameter noticed by Marc Espie. */ /*@modifies errno@*/; extern ssize_t read (int fd, /*@out@*/ void *buf, size_t nbyte) - /*@modifies errno, *buf@*/ /*@requires maxSet(buf) >= (nbyte - 1) @*/ + /*@modifies errno, *buf@*/ + /*@requires maxSet(buf) >= (nbyte - 1) @*/ /*@ensures maxRead(buf) >= nbyte @*/ ; extern int rmdir (const char *path) @@ -867,7 +860,8 @@ extern int unlink (const char *path) /*@modifies fileSystem, errno@*/; extern ssize_t write (int fd, const void *buf, size_t nbyte) - /*@modifies errno@*/; + /*@requires maxRead(buf) >= nbyte@*/ + /*@modifies errno@*/; /* ** utime.h