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;
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
/*@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;
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
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
/*@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@*/
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
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@*/
/*@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
** 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;
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
# 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) /*@*/ ;
/*@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@*/;
/*@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)
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)
/*@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)
/*@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
andersk / splint.git / blobdiff