/*@-nextlinemacros@*/
+/*
+** sys/types.h
+**
+** evans - 2001-08-27: from http://www.opengroup.org/onlinepubs/007908799/xsh/systypes.h.html
+*/
+
+typedef /*@integraltype@*/ blkcnt_t;
+typedef /*@integraltype@*/ blksize_t;
+
+/*@-redef@*/ /* These are also defined by ansi.h: */
+typedef /*@integraltype@*/ clock_t;
+typedef /*@integraltype@*/ dev_t;
+typedef /*@integraltype@*/ gid_t;
+typedef /*@unsignedintegraltype@*/ ino_t;
+typedef /*@integraltype@*/ mode_t;
+typedef /*@integraltype@*/ nlink_t;
+typedef /*@integraltype@*/ off_t;
+typedef /*@integraltype@*/ pid_t;
+typedef /*@integraltype@*/ time_t;
+typedef /*@integraltype@*/ uid_t;
+
+/*@=redef@*/
+
+typedef /*@integraltype@*/ clockid_t;
+typedef /*@unsignedintegraltype@*/ fsblkcnt_t;
+typedef /*@unsignedintegraltype@*/ fsfilcnt_t;
+typedef /*@integraltype@*/ id_t;
+
+typedef /*@integraltype@*/ key_t;
+typedef /*@integraltype@*/ pthread_attr_t;
+typedef /*@integraltype@*/ pthread_cond_t;
+typedef /*@integraltype@*/ pthread_condattr_t;
+typedef /*@integraltype@*/ pthread_key_t;
+typedef /*@integraltype@*/ pthread_mutex_t;
+typedef /*@integraltype@*/ pthread_mutexattr_t;
+typedef /*@integraltype@*/ pthread_once_t;
+typedef /*@integraltype@*/ pthread_rwlock_t;
+typedef /*@integraltype@*/ pthread_rwlockattr_t;
+typedef /*@integraltype@*/ pthread_t;
+typedef /*@signedintegraltype@*/ suseconds_t;
+typedef /*@integraltype@*/ timer_t;
+typedef /*@unsignedintegraltype@*/ useconds_t;
+
+ /*-------------------------------------------------------------
+ -------------------------------------------------------------
+ */
+
+
/*
** Extra stuff in some unixen, not in posix.
*/
-/*@unchecked@*/ int signgam;
+extern /*@unchecked@*/ int signgam;
+/*@-redef@*/ /* Defined by ansi: */
typedef /*@integraltype@*/ clockid_t;
+/*@=redef@*/
extern void bcopy (char *b1, /*@out@*/ char *b2, int length)
/*@modifies *b2@*/ ; /* Yes, the second parameter is the out param! */
fwrite_unlocked (void *pointer, size_t size, size_t num_items, FILE *stream)
/*@modifies *stream;@*/ ;
-extern void funlockfile (FILE *file) /*@modifies *file;@*/ ;
-extern void flockfile (FILE *file) /*@modifies *file@*/ ;
-
extern void /*@alt void * @*/
memccpy (/*@returned@*/ /*@out@*/ void *s1,
/*@unique@*/ void *s2, int c, size_t n)
extern int strcasecmp (char *s1, char *s2) /*@*/ ;
extern int strncasecmp (char *s1, char *s2, int n) /*@*/ ;
-extern char *strdup (char *s) /*@*/ ;
-
-extern /*@null@*/ char *tempnam (char *dir, /*@null@*/ char *pfx)
- /*@modifies internalState@*/ ;
+extern /*@null@*/ /*@only@*/ char *strdup (char *s) /*@*/ ;
extern /*@null@*/ /*@dependent@*/ char *
index (/*@returned@*/ char *s, char c) /*@*/ ;
extern /*@null@*/ /*@dependent@*/ char *
rindex (/*@returned@*/ char *s, char c) /*@*/ ;
-extern /*@dependent@*/ /*@null@*/ FILE *popen (char *command, char *ttype)
- /*@modifies fileSystem, errno@*/ ;
-extern int pclose (FILE *stream) /*@modifies fileSystem, *stream, errno@*/ ;
extern double cbrt (double x) /*@modifies errno@*/ ;
extern double rint (double x) /*@*/ ;
extern void tzset(void) /*@modifies daylight, timezone, tzname@*/ ;
/*@=incondefs@*/
+/*@-redef@*/ /* Defined by ansi: */
+typedef /*@integraltype@*/ key_t;
+/*@-incondefs@*/ typedef long timer_t; /*@=incondefs@*/
+/*@=redef@*/
+
typedef unsigned char uchar_t;
typedef unsigned short ushort_t;
typedef unsigned int uint_t;
typedef int chan_t;
typedef unsigned long rlim_t;
typedef int paddr_t;
-typedef /*@integraltype@*/ key_t;
typedef void *mid_t;
typedef char slab_t[12];
typedef ulong_t shmatt_t;
typedef ulong_t msgqnum_t;
typedef ulong_t msglen_t;
-typedef long timer_t;
typedef uchar_t uchar;
typedef ushort_t ushort;
typedef uint_t uint;
/*@modifies *name, *namelen, errno@*/;
int getsockname (int s, struct sockaddr *address, size_t *address_len)
- /*?requires maxSet(address) > *address_len@*/
+ /*: can't do this? requires maxSet(address) >= (*address_len) @*/
/*@modifies *address, *address_len, errno@*/;
int getsockopt (int s, int level, int optname, /*@out@*/ void *optval, size_t *optlen)
extern void psignal (int sig, const char *msg)
/*@modifies fileSystem@*/;
-/*@unchecked@*/ extern char *optarg;
-/*@unchecked@*/ extern int optind;
-/*@unchecked@*/ extern int optopt;
-/*@unchecked@*/ extern int opterr;
-/*@unchecked@*/ extern int optreset;
-
- extern int
-getopt (int argc, char * const *argv, const char *optstring)
- /*@globals optarg, optind, optopt, opterr, optreset@*/
- /*@modifies optarg, optind, optopt@*/;
-
extern int
setenv (const char *name, const char *value, int overwrite)
/*@globals environ@*/
/*@modifies *environ, errno@*/;
- extern int
-putenv (const char *string)
- /*@globals environ@*/
- /*@modifies *environ, errno@*/;
-
extern void
unsetenv (const char *name)
/*@globals environ@*/
/*@*/;
extern int
-munmap (caddr_t addr, size_t len)
- /*@*/;
-
+ int munmap (/*@only@*/ caddr_t addr, size_t len)
+ /*@modifies fileSystem, *addr, errno @*/;
+
extern int
msync (caddr_t addr, int len, int flags)
/*@*/;
extern int
readlink (const char *path, /*@out@*/ char *buf, int size)
- /*@modifies *buf, errno@*/ /*@ensures result <= size @*/;
+ /*@modifies *buf, errno@*/
+ /*drl 10/27/001*/
+ /*@requires maxSet(buf) >= (size - 1) @*/
+ /*@ensures result <= size @*/;
extern int
select (int mfd, fd_set /*@null@*/ *r, fd_set /*@null@*/ *w, fd_set /*@null@*/ *e, struct timeval *t)
setgroupent (int stayopen)
/*@modifies internalState@*/;
-/*________________________________________________________________________
- * sys/stat.h
- */
+/*
+** sys/stat.h
+**
+** evans 2001-08-26 - updated from http://www.opengroup.org/onlinepubs/007908799/xsh/sysstat.h.html
+*/
+
+/*
+** struct stat replaces POSIX version - more required fields in Unix
+*/
+
+/*@-redef@*/ /*@-matchfields@*/
+struct stat {
+ dev_t st_dev; /* ID of device containing file */
+ ino_t st_ino; /* file serial number */
+ mode_t st_mode; /* mode of file (see below) */
+ nlink_t st_nlink; /* number of links to the file */
+ uid_t st_uid; /* user ID of file */
+ gid_t st_gid; /* group ID of file */
+ dev_t st_rdev; /* device ID (if file is character or block special) */
+ off_t st_size; /* file size in bytes (if file is a regular file) */
+ time_t st_atime; /* time of last access */
+ time_t st_mtime; /* time of last data modification */
+ time_t st_ctime; /* time of last status change */
+ blksize_t st_blksize; /* a filesystem-specific preferred I/O block size for
+ this object. In some filesystem types, this may
+ vary from file to file */
+ blkcnt_t st_blocks; /* number of blocks allocated for this object */
+} ;
+/*@=redef@*/ /*@=matchfields@*/
+
+/*@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@*/
+
+/*@-incondefs@*/ /*: probably wrong in posix.h? */
+/*@constant mode_t S_IWUSR@*/
+/*@constant mode_t S_IXUSR@*/
+/*@constant mode_t S_IRWXG@*/
+/*@constant mode_t S_IRGRP@*/
+/*@constant mode_t S_IWGRP@*/
+/*@constant mode_t S_IXGRP@*/
+/*@constant mode_t S_IRWXO@*/
+/*@constant mode_t S_IROTH@*/
+/*@constant mode_t S_IWOTH@*/
+/*@constant mode_t S_IXOTH@*/
+/*@constant mode_t S_ISUID@*/
+/*@constant mode_t S_ISGID@*/
+/*@constant mode_t S_ISVTX@*/
+
+/*@=incondefs@*/
+
+# if 0
+/*These are the old definitions - they don't appear to be in the Single UNIX Specification */
/*@constant int S_ISTXT@*/
/*@constant int S_IREAD@*/
/*@constant int UF_NODUMP@*/
/*@constant int UF_IMMUTABLE@*/
/*@constant int UF_APPEND@*/
+# endif
- extern int /*@alt lltX_bool@*/
-S_ISLNK (/*@sef@*/ mode_t m)
- /*@*/;
+int /*@alt lltX_bool@*/ S_ISBLK (/*@sef@*/ mode_t m) /*@*/;
+int /*@alt lltX_bool@*/ S_ISCHR (/*@sef@*/ mode_t m) /*@*/;
+int /*@alt lltX_bool@*/ S_ISDIR (/*@sef@*/ mode_t m) /*@*/;
+int /*@alt lltX_bool@*/ S_ISFIFO (/*@sef@*/ mode_t m) /*@*/;
+int /*@alt lltX_bool@*/ S_ISREG (/*@sef@*/ mode_t m) /*@*/;
+int /*@alt lltX_bool@*/ S_ISLNK (/*@sef@*/ mode_t m) /*@*/;
- extern int /*@alt lltX_bool@*/
-S_ISSOCK (/*@sef@*/ mode_t m)
- /*@*/;
+int /*@alt lltX_bool@*/ S_TYPEISMQ (/*@sef@*/ struct stat *buf) /*@*/ ;
+int /*@alt lltX_bool@*/ S_TYPEISSEM (/*@sef@*/ struct stat *buf) /*@*/ ;
+int /*@alt lltX_bool@*/ S_TYPEISSHM (/*@sef@*/ struct stat *buf) /*@*/ ;
- extern int
-chflags (const char *path, u_long flags)
- /*@modifies fileSystem, errno@*/;
+/* in POSIX: chmod, fstat, mkdir, mkfifo, stat, umask */
- extern int
-fchflags (int fd, u_long flags)
- /*@modifies fileSystem, errno@*/;
+int lstat(const char *, /*@out@*/ struct stat *)
+ /*:errorcode -1:*/
+ /*@modifies errno@*/ ;
- extern int
-fchmod (int fd, mode_t mode)
- /*@modifies fileSystem, errno@*/;
+int mknod (const char *, mode_t, dev_t)
+ /*@warn portability "The only portable use of mknod is to create FIFO-special file. If mode is not S_IFIFO or dev is not 0, the behaviour of mknod() is unspecified."@*/
+ /*:errorcode -1:*/
+ /*@modifies errno@*/ ;
- extern int
-lstat (const char *path, /*@out@*/ struct stat *buf)
- /*@modifies errno, *buf@*/;
+int chflags (const char *path, u_long flags)
+ /*@warn unixstandard "Not in Single UNIX Specification Version 2"@*/
+ /*@modifies fileSystem, errno@*/;
+
+int fchflags (int fd, u_long flags)
+ /*@warn unixstandard "Not in Single UNIX Specification Version 2"@*/
+ /*@modifies fileSystem, errno@*/;
/*________________________________________________________________________
* stropts.h
putmsg (int fd, const struct strbuf *c, const struct strbuf *d, int *f)
/*@modifies internalState, errno@*/;
- extern int
-putpmsg (int fd, const struct strbuf *c, const struct strbuf *d, int b, int *f)
- /*@modifies internalState, errno@*/;
+extern int putpmsg (int fd, const struct strbuf *c, const struct strbuf *d, int b, int *f)
+ /*@modifies internalState, errno@*/;
/*________________________________________________________________________
* sys/resource.h
/*@null@*/ struct servent *getservent_r (struct servent *result, char *buffer, int buflen);
int setservent (int stayopen);
-
int endservent (void);
-
extern int h_errno;
/*@null@*/ /*@observer@*/ struct hostent *gethostbyname (/*@nullterminated@*/ /*@notnull@*/ const char *name)
/*@requires maxSet(buffer) >= bufsize@*/ ;
/*@null@*/ /*@observer@*/ struct hostent *gethostbyaddr (/*@notnull@*/ const void *addr, size_t addrlen, int type)
- /*@requires maxRead(addr) == addrlen@*/ /*@i534 ??? is this right? */
+ /*@requires maxRead(addr) == addrlen@*/ /*:i534 ??? is this right? */
/*@warn multithreaded "Unsafe in multithreaded applications, use gethostbyaddr_r instead"@*/
/*@modifies h_errno@*/ ;
struct hostent *gethostbyaddr_r (/*@notnull@*/ const void *addr, size_t addrlen, int type,
/*@returned@*/ /*@out@*/ struct hostent *hent,
/*@exposed@*/ /*@out@*/ char *buffer, int bufsize, /*@out@*/ int *h_errnop)
- /*@requires maxRead(addr) == addrlen
- /\ maxSet(buffer) >= bufsize@*/ /*@i534 ??? is this right? */ ;
+ /*@requires maxRead(addr) == addrlen /\ maxSet(buffer) >= bufsize@*/
+ /*:i534 ??? is this right? */ ;
/*@observer@*/ /*@null@*/ struct hostent *gethostent (void)
/*@warn multithreaded "Unsafe in multithreaded applications, use gethostent_r instead"@*/ ;
struct hostent *gethostent_r (/*@out@*/ /*@returned@*/ struct hostent *hent, /*@exposed@*/ /*@out@*/ char *buffer, int bufsize)
/*@requires maxSet(buffer) >= bufsize@*/ ;
- /*@i534 need to annotate these: */
-struct hostent *fgethostent(FILE *f);
+/*:i534 need to annotate these: */
+struct hostent *fgethostent(FILE *f);
struct hostent *fgethostent_r(FILE*f, struct hostent *hent, char buffer, int bufsize);
-
void sethostent(int stayopen);
-
void endhostent(void);
-
void herror(const char *string);
-
char *hstrerror(int err);
struct hostent {
} ;
/*
-** arpa/inet.h
+** unistd.h
*/
-typedef uint32_t in_addr_t;
+int chroot (/*@notnull@*/ /*@nullterminated@*/ const char *path)
+ /*:statusreturn@*/
+ /*@warn superuser "Only super-user processes may call chroot."@*/
+ /*: other wanings? */ ;
-struct in_addr
-{
- in_addr_t s_addr;
-};
+int fchroot (int fildes)
+ /*:statusreturn@*/
+ /*@warn superuser "Only super-user processes may call fchroot."@*/ ;
+
+/*
+** ctype.h
+**
+** evans 2001-08-26 - added from http://www.opengroup.org/onlinepubs/007908799/xsh/ctype.h.html
+*/
+
+# ifdef STRICT
+lltX_bool isascii(int) /*@*/ ;
+lltX_bool toascii(int) /*@*/ ;
+char _toupper(/*@sef@*/ int) /*@*/ ;
+char _tolower(/*@sef@*/ int) /*@*/ ;
+# else
+lltX_bool /*@alt int@*/ isascii(int /*@alt unsigned char@*/) /*@*/ ;
+lltX_bool /*@alt int@*/ toascii(int /*@alt unsigned char@*/);
+char /*@alt int@*/ _toupper(/*@sef@*/ int /*@alt unsigned char@*/);
+char /*@alt int@*/ _tolower(/*@sef@*/ int /*@alt unsigned char@*/);
+# endif
+
+/* other ctype.h functions in ansi.h */
+
+/*
+** stdlib.h
+**
+** evans 2001-08-27 - added from http://www.opengroup.org/onlinepubs/007908799/xsh/drand48.html
+*/
-typedef uint16_t in_port_t;
+double drand48 (void) /*@modifies internalState@*/ ;
+double erand48 (unsigned short int /*@-fixedformalarray@*/ xsubi[3] /*@=fixedformalarray@*/ )
+ /*@modifies internalState@*/ ;
+
+void srand48 (long int seedval) /*@modifies internalState@*/ ;
+
+/*
+** netinet/in.h
+**
+** evans 2001-08-27 - added from http://www.opengroup.org/onlinepubs/007908799/xns/netinetin.h.html
+*/
+
+typedef /*@unsignedintegraltype@*/ in_port_t; /* An unsigned integral type of exactly 16 bits. */
+typedef /*@unsignedintegraltype@*/ in_addr_t; /* An unsigned integral type of exactly 32 bits. */
+
+typedef /*@unsignedintegraltype@*/ sa_family_t;
+
+struct in_addr {
+ in_addr_t s_addr;
+} ;
+
+struct sockaddr_in {
+ sa_family_t sin_family;
+ in_port_t sin_port;
+ struct in_addr sin_addr;
+ unsigned char sin_zero[8];
+} ;
+
+
+/* The <netinet/in.h> header defines the following macros for use as values of the level argument of
+ getsockopt() and setsockopt():
+ */
+
+/*@constant int IPPROTO_IP@*/
+/*@constant int IPPROTO_ICMP@*/
+/*@constant int IPPROTO_TCP@*/
+/*@constant int IPPROTO_UDP@*/
+
+/* The <netinet/in.h> header defines the following macros for use as destination addresses for connect(), sendmsg() and sendto():
+ */
+
+/*@constant in_addr_t INADDR_ANY@*/
+/*@constant in_addr_t INADDR_BROADCAST@*/
+
+/*
+** arpa/inet.h
+*/
in_addr_t htonl (in_addr_t hostlong) /*@*/ ;
in_port_t htons (in_port_t hostshort) /*@*/ ;
in_port_t ntohs (in_port_t netshort) /*@*/ ;
/*
-** unistd.h
+** dirent.h
+**
+** evans 2001-08-27 - added from http://www.opengroup.org/onlinepubs/007908799/xsh/dirent.h.html
*/
-int chroot (/*@notnull@*/ /*@nullterminated@*/ const char *path)
- /*:statusreturn@*/
- /*@warn superuser "Only super-user processes may call chroot."@*/
- /*: other wanings? */ ;
+/*@-redef@*/ /*@-matchfields@*/ /* Has d_ino field, not in posix (?) */
+
+struct dirent
+{
+ ino_t d_ino;
+ char d_name[];
+} ;
+
+/*@=redef@*/ /*@=matchfields@*/
+
+typedef /*@abstract@*/ DIR;
+
+/*:i32 need to check annotations on these */
+
+int closedir (DIR *) /*:errorcode -1*/ ;
+/*@null@*/ DIR *opendir(const char *) ;
+struct dirent *readdir(DIR *);
+int readdir_r(DIR *, struct dirent *, struct dirent **);
+void rewinddir(DIR *);
+void seekdir(DIR *, long int);
+long int telldir(DIR *);
+
+/*drl added these functions
+ stpcpy and stpncpy are found on linux but
+ don't seem to be present on other unixes
+
+ thanks to Jeff Johnson for pointing out that
+ these functions were in the unix library
+*/
+
+/* this function is like strcpy but it reutrns a pointer to the null terminated character in dest instead of the beginning of dest */
+
+extern char * stpcpy(/*@out@*/ /*@returned@*/ char * dest, const char * src)
+ /*@modifies *dest @*/
+ /*@requires maxSet(dest) >= maxRead(src) @*/
+ /*@ensures MaxRead(dest) == MaxRead (src) /\ MaxRead(result) == 0 /\ MaxSet(result) == ( maxSet(dest) - MaxRead(src) ); @*/;
+
+
+extern char * stpncpy(/*@out@*/ /*@returned@*/ char * dest,
+ const char * src, size_t n)
+ /*@modifies *dest @*/
+ /*@requires MaxSet(dest) >= ( n - 1 ); @*/ /*@ensures MaxRead (src) >= MaxRead(dest) /\ MaxRead (dest) <= n; @*/
+ ;
+
+ /* drl added 09-25-001
+ Alexander Ma pointed out these were missing
+ */
+
+int usleep (useconds_t useconds) /*@modifies systemState, errno@*/
+ /*error -1 sucess 0 */
+ /* warn opengroup unix specification recommends using setitimer(), timer_create(), timer_delete(), timer_getoverrun(), timer_gettime() or
+ timer_settime() instead of this interface.
+ */
+ ;
+
+
+ /* drl added 10-27-001 */
+ /*@i23*/
+
+ /*not sure what the exact size of this is
+ also can IPv6 use this function?
+ */
+
+ char *inet_ntoa(struct in_addr in)
+ /*@ensures maxSet(result) <= 15 /\ maxRead(result) <= 15 @*/
+ ;
+
+
+ extern double hypot(double x, double y) /*@modifies errno@*/ /*error errno only*/;
+
+
+ extern double j0(double x) /*@modifies errno @*/ /*error 0 or NaN */;
+ extern double j1(double x) /*@modifies errno @*/ /*error 0 or NaN */;
+ extern double jn(int n, double x) /*@modifies errno @*/ /*error 0 or NaN */;
+
+ extern double y0(double x) /*@modifies errno @*/ /*error NaN -HUGE_VAL 0.0 */ ;
+ extern double y1 (double x) /*@modifies errno @*/ /*error NaN -HUGE_VAL 0.0 */;
+ extern double yn (int n, double x) /*@modifies errno @*/ /*error NaN -HUGE_VAL 0.0 */;
+
+ extern double acosh(double x) /*@modifies errno @*/ /*error errno and implementation-dependent(NaN if present) */ /*error NaN and may errno*/;
+ extern double asinh(double x) /*@modifies errno @*/ /*error NaN and may errno */;
+
+ extern double atanh(double x) /*@modifies errno @*/ /*error errno and implementation-dependent(NaN if present) */ /*error NaN and may errno */ ;
+
+ extern double lgamma(double x) /*@modifies errno @*/ /*error NaN or HUGE_VAL may set errno */;
+
+ extern int signgam ;
+
+ extern double erf(double x) /*@modifies errno @*/ /*error NaN or 0 may set errno */;
+
+ extern double erfc (double x) /*@modifies errno @*/ /*error NaN or 0
+ may set errno */;
+
+
+
+
+
-int fchroot (int fildes)
- /*:statusreturn@*/
- /*@warn superuser "Only super-user processes may call fchroot."@*/ ;
andersk / splint.git / blobdiff