X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/86d93ed383c14be2a4548bd8ab98e4c1a79cb1f0..768a340a15bd3bf200883e277f0a33de81d9a8e8:/lib/posix.h

diff --git a/lib/posix.h b/lib/posix.h
index da1d1db..924efa8 100644
--- a/lib/posix.h
+++ b/lib/posix.h
@@ -95,10 +95,10 @@ extern int closedir (DIR *dirp)
    /*drl 1/4/2001 added the dependent annotation as suggested by
      Ralf Wildenhues */
    
-   extern /*@null@*/ /*@dependent@*/ DIR *opendir (const char *dirname)
+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)
@@ -173,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;
@@ -204,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
@@ -216,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
@@ -288,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
@@ -302,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
@@ -397,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;
@@ -511,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@*/;
 
@@ -827,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)
@@ -863,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