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;
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
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@*/
char *pw_shell;
} ;
- extern /*@observer@*/ /*@null@*/ struct passwd *
-getpwnam (const char *)
- /*@modifies errno@*/;
+/*@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@*/;
+/*@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
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)
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
/*@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 */
} ;
/*
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
/*@constant int WUNTRACED@*/
- extern pid_t
-wait (/*@out@*/ /*@null@*/ int *st)
- /*@modifies *st, errno@*/;
+/* These are in Unix spec, are they in POSIX? */
+/*@constant int WCONTINUED@*/
+/*@constant int WNOHANG@*/
- extern pid_t
-waitpid (pid_t pid, /*@out@*/ int *st, int opt)
- /*@modifies *st, errno@*/;
+pid_t wait (/*@out@*/ /*@null@*/ int *st)
+ /*@modifies *st, errno, systemState@*/;
+
+pid_t waitpid (pid_t pid, /*@out@*/ /*@null@*/ int *st, int opt)
+ /*@modifies *st, errno, systemState@*/;
/*
** termios.h
extern void
tzset (void)
- /*@globals environ@*/ /*@modifies internalState@*/;
+ /*@globals environ@*/ /*@modifies systemState@*/;
/*
** unistd.h
/*@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 *
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)
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)
+ /*@requires maxRead(buf) >= nbyte@*/
+ /*@modifies errno@*/;
/*
** utime.h
utime (const char *path, /*@null@*/ const struct utimbuf *times)
/*@modifies fileSystem, errno@*/;
+/*
+** regex.h
+*/
+
+typedef /*@abstract@*/ /*@mutable@*/ void *regex_t;
+typedef /*@integraltype@*/ regoff_t;
+
+typedef struct
+{
+ regoff_t rm_so;
+ regoff_t rm_eo;
+} regmatch_t;
+
+int regcomp (/*@out@*/ regex_t *preg, /*@nullterminated@*/ const char *regex, int cflags)
+ /*:statusreturn@*/
+ /*@modifies preg@*/ ;
+
+int regexec (const regex_t *preg, /*@nullterminated@*/ const char *string, size_t nmatch, /*@out@*/ regmatch_t pmatch[], int eflags)
+ /*@requires maxSet(pmatch) >= nmatch@*/
+ /*@modifies pmatch@*/ ;
+
+size_t regerror (int errcode, const regex_t *preg, /*@out@*/ char *errbuf, size_t errbuf_size)
+ /*@requires maxSet(errbuf) >= errbuf_size@*/
+ /*@modifies errbuf@*/ ;
+
+void regfree (/*@only@*/ regex_t *preg) ;
+
+/* regcomp flags */
+/*@constant int REG_BASIC@*/
+/*@constant int REG_EXTENDED@*/
+/*@constant int REG_ICASE@*/
+/*@constant int REG_NOSUB@*/
+/*@constant int REG_NEWLINE@*/
+/*@constant int REG_NOSPEC@*/
+/*@constant int REG_PEND@*/
+/*@constant int REG_DUMP@*/
+
+/* regerror flags */
+/*@constant int REG_NOMATCH@*/
+/*@constant int REG_BADPAT@*/
+/*@constant int REG_ECOLLATE@*/
+/*@constant int REG_ECTYPE@*/
+/*@constant int REG_EESCAPE@*/
+/*@constant int REG_ESUBREG@*/
+/*@constant int REG_EBRACK@*/
+/*@constant int REG_EPAREN@*/
+/*@constant int REG_EBRACE@*/
+/*@constant int REG_BADBR@*/
+/*@constant int REG_ERANGE@*/
+/*@constant int REG_ESPACE@*/
+/*@constant int REG_BADRPT@*/
+/*@constant int REG_EMPTY@*/
+/*@constant int REG_ASSERT@*/
+/*@constant int REG_INVARG@*/
+/*@constant int REG_ATOI@*/ /* non standard */
+/*@constant int REG_ITOA@*/ /* non standard */
+
+/* regexec flags */
+/*@constant int REG_NOTBOL@*/
+/*@constant int REG_NOTEOL@*/
+/*@constant int REG_STARTEND@*/
+/*@constant int REG_TRACE@*/
+/*@constant int REG_LARGE@*/
+/*@constant int REG_BACKR@*/
+
+