Fixed help.expect

[splint.git] / lib / posix.h

diff --git a/lib/posix.h b/lib/posix.h
index 923d39353722c0508de32f43391c2c328a89671a..7fea224a4b316575ef9cc18314a9e6b9761aae26 100644 (file)
--- a/lib/posix.h
+++ b/lib/posix.h
@@ -72,7 +72,7 @@
 
 typedef /*@integraltype@*/ dev_t;
 typedef /*@integraltype@*/ gid_t;
-typedef /*@integraltype@*/ ino_t;
+typedef /*@unsignedintegraltype@*/ ino_t; /*: is this definitely unsigned? */
 typedef /*@integraltype@*/ mode_t;
 typedef /*@integraltype@*/ nlink_t;
 typedef /*@integraltype@*/ off_t;
@@ -89,21 +89,17 @@ struct dirent {
   char d_name[];
 };
 
-       extern int
-closedir (DIR *dirp)
-       /*@modifies errno@*/;
+extern int closedir (DIR *dirp)
+   /*@modifies errno@*/;
 
-       extern /*@null@*/ DIR *
-opendir (const char *dirname)
-       /*@modifies errno@*/;
+extern /*@null@*/ DIR *opendir (const char *dirname)
+   /*@modifies errno@*/;
 
-       extern /*@null@*/ struct dirent *
-readdir (DIR *dirp)
-       /*@modifies errno@*/;
+extern /*@null@*/ struct dirent *readdir (DIR *dirp)
+   /*@modifies errno@*/;
 
-       extern void
-rewinddir (DIR *dirp)
-       /*@*/;
+extern void rewinddir (DIR *dirp)
+   /*@*/;
 
 /*
 ** errno.h
@@ -197,17 +193,15 @@ struct flock {
   pid_t l_pid;
 };
 
-       extern int
-creat (const char *path, mode_t mode)
-       /*@modifies errno@*/;
+extern int creat (const char *path, mode_t mode)
+   /*@modifies errno@*/;
 
-       extern int
-fcntl (int fd, int cmd, ...)
-       /*@modifies errno@*/;
+extern int fcntl (int fd, int cmd, ...)
+   /*@modifies errno@*/;
 
-       extern int
-open (const char *path, int oflag, ...)
-       /*@modifies errno@*/;
+extern int open (const char *path, int oflag, ...)
+  /*:checkerror -1 - returns -1 on error */
+  /*@modifies errno@*/;
 
 /*
 ** grp.h
@@ -231,15 +225,37 @@ getgrnam (const char *nm)
 ** limits.h
 */
 
+/* These are always defined: */
+
+/*@constant int CHAR_BIT@*/
+/*@constant char CHAR_MIN@*/
+/*@constant char CHAR_MAX@*/
+/*@constant int INT_MIN@*/
+/*@constant int INT_MAX@*/
+/*@constant long LONG_MIN@*/
+/*@constant long LONG_MAX@*/
+/*@constant int MB_LEN_MAX@*/
+/*@constant signed char SCHAR_MIN@*/
+/*@constant signed char SCHAR_MAX@*/
+/*@constant short SHRT_MIN@*/
+/*@constant short SHRT_MAX@*/
+/*@constant unsigned char UCHAR_MAX@*/
+/*@constant unsigned int UINT_MAX@*/
+/*@constant unsigned long ULONG_MAX@*/
+/*@constant unsigned short USHRT_MAX@*/
+
+/* When _POSIX_SOURCE is defined */
+
 /*@constant long ARG_MAX@*/
 /*@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 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@*/
@@ -394,16 +410,16 @@ extern int fileno (FILE *fp) /*@modifies errno@*/;
 /*@constant int S_IXUSR@*/
 
 struct stat {
-  mode_t       st_mode;
+  mode_t st_mode;
   ino_t        st_ino;
   dev_t        st_dev;
-  nlink_t      st_nlink;
+  nlink_t st_nlink;
   uid_t        st_uid;
   gid_t        st_gid;
   off_t        st_size;
-  time_t       st_st_atime;
-  time_t       st_st_mtime;
-  time_t       st_st_ctime;
+  time_t st_atime; /* evans 2001-08-23 - these were previously st_st_atime - POSIX spec says st_atime */
+  time_t st_mtime; /* evans 2001-08-23 - these were previously st_st_mtime - POSIX spec says st_mtime */
+  time_t st_ctime; /* evans 2001-08-23 - these were previously st_st_ctime - POSIX spec says st_ctime */
 } ;
 
 /*
@@ -429,27 +445,24 @@ extern SBOOLINT S_ISFIFO (/*@sef@*/ mode_t m) /*@*/ ;
 
 extern SBOOLINT S_ISREG (/*@sef@*/ mode_t m) /*@*/ ;
 
-extern int chmod (const char *path, mode_t mode)
-   /*@modifies fileSystem, errno@*/ ;
-   
-extern int fstat (int fd, /*@out@*/ struct stat *buf)
+int chmod (const char *path, mode_t mode)
+     /*@modifies fileSystem, errno@*/ ;
+     
+int fstat (int fd, /*@out@*/ struct stat *buf)
      /*@modifies errno, *buf@*/ ;
      
-extern int
-mkdir (const char *path, mode_t mode)
-       /*@modifies fileSystem, errno@*/;
-
-       extern int
-mkfifo (const char *path, mode_t mode)
-       /*@modifies fileSystem, errno@*/;
+int mkdir (const char *path, mode_t mode)
+     /*@modifies fileSystem, errno@*/;
+     
+int mkfifo (const char *path, mode_t mode)
+     /*@modifies fileSystem, errno@*/;
 
-       extern int
-stat (const char *path, /*@out@*/ struct stat *buf)
-       /*@modifies errno, *buf@*/;
+int stat (const char *path, /*@out@*/ struct stat *buf)
+     /*:errorcode -1*/
+     /*@modifies errno, *buf@*/;
 
-       extern int
-umask (mode_t cmask)
-       /*@modifies systemState@*/;
+int umask (mode_t cmask)
+     /*@modifies systemState@*/;
 
 /*
 ** sys/times.h
@@ -679,25 +692,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)
@@ -753,9 +757,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)@*/
+     /*@requires maxRead(buf) <= (size - 1)*/
+
+     /*@modifies errno, *buf@*/ ;
 
        extern gid_t
 getegid (void)