]> andersk Git - splint.git/blobdiff - lib/posix.h
andersk / splint.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
Fixed help.expect
[splint.git] / lib / posix.h
diff --git a/lib/posix.h b/lib/posix.h
index 99142c01a393ba84118cd41c367def93ac481638..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@*/
@@ -270,12 +286,12 @@ struct passwd {
 } ;
 
        extern /*@observer@*/ /*@null@*/ struct passwd *
-getpwnam (const char *)
-       /*@modifies errno@*/;
+       getpwnam (const char *)
+       /*@modifies errno@*/  /*@ensures maxRead(result) == 0 /\ maxSet(result) == 0 @*/;
 
        extern /*@observer@*/ /*@null@*/ struct passwd *
 getpwuid (uid_t uid)
-       /*@modifies errno@*/;
+       /*@modifies errno@*/  /*@ensures maxRead(result) == 0 /\ maxSet(result) == 0 @*/;
 
 /*
 ** setjmp.h
@@ -327,7 +343,7 @@ kill (pid_t pid, int sig)
 
        extern int
 sigaction (int sig, const struct sigaction *act, /*@out@*/ /*@null@*/ struct sigaction *oact)
-       /*@modifies *oact, errno, internalState@*/;
+       /*@modifies *oact, errno, systemState@*/;
 
        extern int
 sigaddset (sigset_t *set, int signo)
@@ -355,11 +371,11 @@ sigpending (/*@out@*/ sigset_t *set)
 
        extern int
 sigprocmask (int how, /*@null@*/ const sigset_t *set, /*@null@*/ /*@out@*/ sigset_t *oset)
-       /*@modifies *oset, errno, internalState@*/;
+       /*@modifies *oset, errno, systemState@*/;
 
        extern int
 sigsuspend (const sigset_t *sigmask)
-       /*@modifies errno, internalState@*/;
+       /*@modifies errno, systemState@*/;
 
 /*
 ** stdio.h
@@ -369,13 +385,10 @@ sigsuspend (const sigset_t *sigmask)
 /*@constant int L_cuserid@*/
 /*@constant int STREAM_MAX@*/
 
-       extern /*@null@*/ /*@dependent@*/ FILE *
-fdopen (int fd, const char *type)
-       /*@modifies errno, fileSystem@*/;
+extern /*@null@*/ /*@dependent@*/ FILE *fdopen (int fd, const char *type)
+   /*@modifies errno, fileSystem@*/;
 
-       extern int
-fileno (FILE *fp)
-       /*@modifies errno@*/;
+extern int fileno (FILE *fp) /*@modifies errno@*/;
 
 /*
 ** sys/stat.h
@@ -397,16 +410,16 @@ fileno (FILE *fp)
 /*@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 */
 } ;
 
 /*
@@ -432,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 internalState@*/;
+int umask (mode_t cmask)
+     /*@modifies systemState@*/;
 
 /*
 ** sys/times.h
@@ -498,13 +508,11 @@ extern int WTERMSIG (int status) /*@*/ ;
 
 /*@constant int WUNTRACED@*/
 
-       extern pid_t
-wait (/*@out@*/ /*@null@*/ int *st)
-       /*@modifies *st, errno@*/;
+pid_t wait (/*@out@*/ /*@null@*/ int *st)
+   /*@modifies *st, errno, systemState@*/;
 
-       extern pid_t
-waitpid (pid_t pid, /*@out@*/ int *st, int opt)
-       /*@modifies *st, errno@*/;
+pid_t waitpid (pid_t pid, /*@out@*/ /*@null@*/ int *st, int opt)
+   /*@modifies *st, errno, systemState@*/;
 
 /*
 ** termios.h
@@ -643,7 +651,7 @@ tcsetattr (int fd, int opt, const struct termios *p)
 
        extern void
 tzset (void)
-       /*@globals environ@*/ /*@modifies internalState@*/;
+       /*@globals environ@*/ /*@modifies systemState@*/;
 
 /*
 ** unistd.h
@@ -684,34 +692,25 @@ 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 internalState@*/;
+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)
-       /*@modifies fileSystem, errno, internalState@*/;
+       /*@modifies fileSystem, errno, systemState@*/;
        /* state: record locks are unlocked */
 
        extern char *
 ctermid (/*@returned@*/ /*@out@*/ /*@null@*/ char *s)
-       /*@modifies *s, internalState@*/;
+       /*@modifies *s, systemState@*/;
 
        /* cuserid is in the 1988 version of POSIX but removed in 1990 */
        extern char *
@@ -758,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)
@@ -822,58 +823,44 @@ pause (void)
 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@*/;
+extern ssize_t read (int fd, /*@out@*/ void *buf, size_t nbyte)
+   /*@modifies errno, *buf@*/ /*@requires maxSet(buf) >= (nbyte - 1) @*/
+   /*@ensures maxRead(buf) >= nbyte @*/ ;
 
-       extern int
-rmdir (const char *path)
-       /*@modifies fileSystem, errno@*/;
+extern int rmdir (const char *path)
+   /*@modifies fileSystem, errno@*/;
 
-       extern int
-setgid (gid_t gid)
-       /*@modifies errno, internalState@*/;
+extern int setgid (gid_t gid)
+   /*@modifies errno, systemState@*/;
 
-       extern int
-setpgid (pid_t pid, pid_t pgid)
-       /*@modifies errno, internalState@*/;
+extern int setpgid (pid_t pid, pid_t pgid)
+   /*@modifies errno, systemState@*/;
 
-       extern pid_t
-setsid (void)
-       /*@*/;
+extern pid_t setsid (void) /*@modifies systemState@*/;
 
-       extern int
-setuid (uid_t uid)
-       /*@modifies errno, internalState@*/;
+extern int setuid (uid_t uid)
+   /*@modifies errno, systemState@*/;
 
-       extern unsigned int
-sleep (unsigned int sec)
-       /*@*/;
+unsigned int sleep (unsigned int sec) /*@modifies systemState@*/ ;
 
-       extern long
-sysconf (int name)
-       /*@modifies errno@*/;
+extern long sysconf (int name)
+   /*@modifies errno@*/;
 
-       extern pid_t
-tcgetpgrp (int fd)
-       /*@modifies errno@*/;
+extern pid_t tcgetpgrp (int fd)
+   /*@modifies errno@*/;
 
-       extern int
-tcsetpgrp (int fd, pid_t pgrpid)
-       /*@modifies errno, internalState@*/;
+extern int tcsetpgrp (int fd, pid_t pgrpid)
+   /*@modifies errno, systemState@*/;
 
-       /* Q: observer ok? */
-       extern /*@null@*/ /*@observer@*/ char *
-ttyname (int fd)
-       /*@modifies errno@*/;
+/* Q: observer ok? */
+extern /*@null@*/ /*@observer@*/ char *ttyname (int fd)
+   /*@modifies errno@*/;
 
-       extern int
-unlink (const char *path)
-       /*@modifies fileSystem, errno@*/;
+extern int unlink (const char *path)
+   /*@modifies fileSystem, errno@*/;
 
-       extern ssize_t
-write (int fd, const void *buf, size_t nbyte)
-       /*@modifies errno@*/;
+extern ssize_t write (int fd, const void *buf, size_t nbyte)
+   /*@modifies errno@*/;
 
 /*
 ** utime.h
@@ -953,3 +940,4 @@ void regfree (/*@only@*/ regex_t *preg) ;
 /*@constant int        REG_LARGE@*/
 /*@constant int        REG_BACKR@*/
 
+
git-cvsimport mirror of splint
This page took 0.261708 seconds and 4 git commands to generate.