X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/7bf960677344d11a101697c76672a0be4b3759f2..HEAD:/lib/posix.h

diff --git a/lib/posix.h b/lib/posix.h
index 01fbf40..aa35f6d 100644
--- 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,20 @@ 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@*/;
+   /*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)
-	/*@modifies errno@*/;
+extern /*@dependent@*/ /*@null@*/ struct dirent *readdir (DIR *dirp)
+   /*@modifies errno@*/;
 
-	extern void
-rewinddir (DIR *dirp)
-	/*@*/;
+extern void rewinddir (DIR *dirp)
+   /*@*/;
 
 /*
 ** errno.h
@@ -174,20 +173,32 @@ 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;
@@ -197,17 +208,16 @@ 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 */
+     /* the ... is one mode_t param */
+  /*@modifies errno@*/ ;
 
 /*
 ** grp.h
@@ -219,27 +229,49 @@ 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
 */
 
+/* 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@*/
@@ -269,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
@@ -283,20 +313,44 @@ 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
+** moved up from signal.h
 */
 
 typedef /*@abstract@*/ sigset_t;
 
+typedef struct {
+  void *ss_sp;
+  size_t ss_size;
+  int ss_flags;
+} stack_t;
+
+/*
+** ucontext.h
+*/
+
+typedef /*@abstract@*/ mcontext_t;
+
+typedef struct s_ucontext_t {
+  /*@null@*/ struct s_ucontext_t *uc_link;
+  sigset_t uc_sigmask;
+  stack_t uc_stack;
+  mcontext_t uc_mcontext;
+} ucontext_t;
+
+int  getcontext(ucontext_t *);
+int  setcontext(const ucontext_t *);
+void makecontext(ucontext_t *, void (*)(void), int, ...);
+int  swapcontext(ucontext_t *restrict, const ucontext_t *restrict);
+
+/*
+** signal.h
+*/
+
 /*@constant int SA_NOCLDSTOP@*/
 /*@constant int SIG_BLOCK@*/
 /*@constant int SIG_SETMASK@*/
@@ -315,10 +369,33 @@ typedef /*@abstract@*/ sigset_t;
 /*@constant int SIGUSR1@*/
 /*@constant int SIGUSR2@*/
 
+struct sigstack {
+  int ss_onstack;
+  void *ss_sp;
+} ;
+
+typedef struct {
+  int si_signo;
+  int si_errno;
+  int si_code;
+  pid_t si_pid;
+  uid_t si_uid;
+  void *si_addr;
+  int si_status;
+  long si_band;
+  union sigval si_value;
+} siginfo_t;
+
+typedef union {
+  int    sival_int;
+  void  *sival_ptr;    
+} sigval;
+
 struct sigaction {
   void (*sa_handler)();
   sigset_t sa_mask;
   int sa_flags;
+  void (*sa_sigaction)(int, siginfo_t *, void *); /* Added 2003-06-13: Noticed by Jerry James */
 } ;
  
 	extern /*@mayexit@*/ int
@@ -369,45 +446,31 @@ 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
 */
 
-/*@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;
+  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 */
 } ;
+/*
+** evans 2004-05-19: dependent annotations atted for time_t fields.  Could not find
+** any clear documetation on this, but it seems to be correct. 
+*/
 
 /*
 ** POSIX does not require that the S_I* be functions. They're
@@ -416,10 +479,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) /*@*/ ;
@@ -432,27 +495,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@*/;
+int mkdir (const char *path, mode_t mode)
+     /*@modifies fileSystem, errno@*/;
+     
+int mkfifo (const char *path, mode_t mode)
+     /*@modifies fileSystem, errno@*/;
 
-	extern int
-mkfifo (const char *path, mode_t mode)
-	/*@modifies fileSystem, errno@*/;
+int stat (const char *path, /*@out@*/ struct stat *buf)
+     /*:errorcode -1*/
+     /*@modifies errno, *buf@*/;
 
-	extern int
-stat (const char *path, /*@out@*/ struct stat *buf)
-	/*@modifies errno, *buf@*/;
-
-	extern int
-umask (mode_t cmask)
-	/*@modifies systemState@*/;
+int umask (mode_t cmask)
+     /*@modifies systemState@*/;
 
 /*
 ** sys/times.h
@@ -498,6 +558,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@*/;
 
@@ -682,25 +746,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)
@@ -756,9 +811,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)
@@ -820,58 +877,46 @@ 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@*/ /*@requires maxSet(buf) >= (nbyte - 1) @*/
-     /*@ensures maxRead(buf) >= nbyte @*/;
-     /*@i33*/
-     
-	extern int
-rmdir (const char *path)
-	/*@modifies fileSystem, errno@*/;
+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
-setgid (gid_t gid)
-	/*@modifies errno, systemState@*/;
+extern int rmdir (const char *path)
+   /*@modifies fileSystem, errno@*/;
 
-	extern int
-setpgid (pid_t pid, pid_t pgid)
-	/*@modifies errno, systemState@*/;
+extern int setgid (gid_t gid)
+   /*@modifies errno, systemState@*/;
 
-	extern pid_t
-setsid (void)
-	/*@*/;
+extern int setpgid (pid_t pid, pid_t pgid)
+   /*@modifies errno, systemState@*/;
 
-	extern int
-setuid (uid_t uid)
-	/*@modifies errno, systemState@*/;
+extern pid_t setsid (void) /*@modifies systemState@*/;
+
+extern int setuid (uid_t uid)
+   /*@modifies errno, systemState@*/;
 
 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, systemState@*/;
+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)
+     /*@requires maxRead(buf) >= nbyte@*/
+     /*@modifies errno@*/;
 
 /*
 ** utime.h