X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/1d239d69c6db918ef0691cc89740335df558c7c6..210066f9dd04de7d7d2f04d320b39a52f28b290b:/lib/unix.h diff --git a/lib/unix.h b/lib/unix.h index e92db76..0cba8d8 100644 --- a/lib/unix.h +++ b/lib/unix.h @@ -4,18 +4,63 @@ /*@-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! */ -extern int /*@alt lltX_bool@*/ bcmp (char *b1, char *b2, int length) /*@*/ ; +extern int /*@alt _Bool@*/ bcmp (char *b1, char *b2, int length) /*@*/ ; /* Return value is NOT like strcmp! */ extern void bzero (/*@out@*/ char *b1, int length) /*@modifies *b1@*/ ; @@ -45,9 +90,6 @@ extern size_t 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) @@ -57,22 +99,19 @@ extern int strcasecmp (char *s1, char *s2) /*@*/ ; extern int strncasecmp (char *s1, char *s2, int n) /*@*/ ; extern /*@null@*/ /*@only@*/ char *strdup (char *s) /*@*/ ; -extern /*@null@*/ char *tempnam (char *dir, /*@null@*/ char *pfx) - /*@modifies internalState@*/ ; - 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@*/ ; +# if 0 +These are in ISO C99. Moved to standard.h: + extern double cbrt (double x) /*@modifies errno@*/ ; + extern double rint (double x) /*@*/ ; + extern double trunc (double x) /*@*/ ; +# endif -extern double cbrt (double x) /*@modifies errno@*/ ; -extern double rint (double x) /*@*/ ; -extern double trunc (double x) /*@*/ ; /*@constant int ENOTBLK@*/ /*@constant int ETXTBSY@*/ @@ -139,17 +178,22 @@ extern double trunc (double x) /*@*/ ; /*@constant int USI_MAX@*/ /*@constant int WORD_BIT@*/ /*@constant int LONG_BIT@*/ + +/*@-incondefs@*/ /* some constant are also declared in posix.h*/ + /*@constant long NAME_MAX@*/ + /*@constant long NGROUPS_MAX@*/ -/*@constant long MAX_INPUT@*/ + /*@constant long MAX_CANON@*/ /*@constant int MAX_CHAR@*/ /*@constant long OPEN_MAX@*/ /*@constant int PASS_MAX@*/ -/*@constant int PATH_MAX@*/ + /*@constant int PID_MAX@*/ /*@constant int SYSPID_MAX@*/ /*@constant long PIPE_BUF@*/ +/*@=incondefs@*/ /*@constant int PIPE_MAX@*/ /*@constant int PROC_MAX@*/ /*@constant int STD_BLK@*/ @@ -198,6 +242,11 @@ extern /*@unchecked@*/ char *tzname[]; 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; @@ -215,15 +264,12 @@ typedef char *addr_t; typedef long physadr_t; typedef short cnt_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; @@ -241,28 +287,29 @@ typedef u_long fixpt_t; typedef long segsz_t; typedef /*@abstract@*/ fd_set; -int ttyname_r (int fg, /*@out@*/ char *buffer, int len) /*@modifies buffer@*/ ; int ioctl (int d, int /*@alt long@*/ request, /*@out@*/ void *arg) /*@modifies *arg, errno@*/ ; /* depends on request! */ pid_t vfork (void) /*@modifies fileSystem@*/ ; +/* +** sys/uio.h +*/ struct iovec { - void *iov_base; - size_t iov_len; + /*@dependent@*/ void *iov_base; + size_t iov_len; /*: maxSet(iov_base) = iov_len */ }; +/* from limits.h */ /*@constant int UIO_MAXIOV@*/ /* BSD */ /*@constant int IOV_MAX@*/ /* supposedly SVR4 */ - extern ssize_t -readv (int fd, const struct iovec iov[], int iovcnt) - /*@modifies iov[].iov_base, fileSystem, errno@*/; +ssize_t readv (int fd, const struct iovec *iov, int iovcnt) + /*@modifies iov->iov_base, fileSystem, errno@*/; - extern ssize_t -writev (int fd, const struct iovec iov[], int iovcnt) - /*@modifies errno@*/; +ssize_t writev (int fd, const struct iovec *iov, int iovcnt) + /*@modifies errno@*/; /*________________________________________________________________________ * poll.h @@ -300,34 +347,34 @@ extern void free (/*@notnull@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies *p@*/ * sys/socket.h */ -/*@constant int SOCK_STREAM@*/ -/*@constant int SOCK_DGRAM@*/ -/*@constant int SOCK_RAW@*/ + + + /*@constant int SOCK_RDM@*/ -/*@constant int SOCK_SEQPACKET@*/ -/*@constant int SO_DEBUG@*/ -/*@constant int SO_ACCEPTCONN@*/ -/*@constant int SO_REUSEADDR@*/ -/*@constant int SO_KEEPALIVE@*/ -/*@constant int SO_DONTROUTE@*/ -/*@constant int SO_BROADCAST@*/ + + + + + + + /*@constant int SO_USELOOPBACK@*/ -/*@constant int SO_LINGER@*/ -/*@constant int SO_OOBINLINE@*/ + + /*@constant int SO_REUSEPORT@*/ -/*@constant int SO_SNDBUF@*/ -/*@constant int SO_RCVBUF@*/ -/*@constant int SO_SNDLOWAT@*/ -/*@constant int SO_RCVLOWAT@*/ -/*@constant int SO_SNDTIMEO@*/ -/*@constant int SO_RCVTIMEO@*/ -/*@constant int SO_ERROR@*/ -/*@constant int SO_TYPE@*/ -/*@constant int SOL_SOCKET@*/ -/*@constant int AF_UNSPEC@*/ + + + + + + + + + + /*@constant int AF_LOCAL@*/ -/*@constant int AF_UNIX@*/ -/*@constant int AF_INET@*/ + + /*@constant int AF_IMPLINK@*/ /*@constant int AF_PUP@*/ /*@constant int AF_CHAOS@*/ @@ -355,13 +402,12 @@ extern void free (/*@notnull@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies *p@*/ /*@constant int AF_ISDN@*/ /*@constant int AF_E164@*/ /*@constant int AF_MAX@*/ -/*@constant int MSG_OOB@*/ -/*@constant int MSG_PEEK@*/ -/*@constant int MSG_DONTROUTE@*/ -/*@constant int MSG_EOR@*/ -/*@constant int MSG_TRUNC@*/ -/*@constant int MSG_CTRUNC@*/ -/*@constant int MSG_WAITALL@*/ + + + + + + /*@constant int MSG_DONTWAIT@*/ /*@constant int MSG_EOF@*/ /*@constant int MSG_COMPAT@*/ @@ -400,60 +446,135 @@ extern void free (/*@notnull@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies *p@*/ /*@constant int NET_RT_FLAGS@*/ /*@constant int NET_RT_IFLIST@*/ /*@constant int NET_RT_MAXID@*/ -/*@constant int SOMAXCONN@*/ -/*@constant int SCM_RIGHTS@*/ - struct sockaddr { - u_char sa_len; /* total length */ - u_char sa_family; /* address family */ - char sa_data[14]; /* actually longer; address value */ -}; +/*moved this to before socket.h to get splint to parse the header*/ +typedef /*@unsignedintegraltype@*/ sa_family_t; - struct linger { - int l_onoff; /* option on/off */ - int l_linger; /* linger time */ -}; +/* +** sys/socket.h +** (updated 26 May 2002) +*/ + +typedef /*@unsignedintegraltype@*/ __socklen_t; /* not in USB, but needed by linux */ +typedef /*@unsignedintegraltype@*/ socklen_t; - struct sockproto { - u_short sp_family; /* address family */ - u_short sp_protocol; /* protocol */ +struct sockaddr { + sa_family_t sa_family; /* address family */ + char sa_data[]; /* variable length */ }; - struct msghdr { - caddr_t msg_name; /* optional address */ - u_int msg_namelen; /* size of address */ - struct iovec *msg_iov; /* scatter/gather array */ - u_int msg_iovlen; /* # elements in msg_iov */ - caddr_t msg_control; /* ancillary data, see below */ - u_int msg_controllen; /* ancillary data buffer len */ - int msg_flags; /* flags on received message */ + +struct sockaddr_storage { + sa_family_t ss_family; +} ; + +struct msghdr { + /*@dependent@*/ void *msg_name; + socklen_t msg_namelen; /*: maxSet (msg_name) >= msg_namelen */ + /*@dependent@*/ struct iovec *msg_iov; /* scatter/gather array */ + int msg_iovlen; /* # elements in msg_iov */ /*: maxSet (msg_iov) >= msg_iovlen */ + /*@dependent@*/ void *msg_control; /* ancillary data, see below */ + socklen_t msg_controllen; /*: maxSet (msg_control) >= msg_controllen */ + int msg_flags; /* flags on received message */ +} ; + +struct cmsghdr { + socklen_t cmsg_len; /* data byte count, including hdr */ + int cmsg_level; /* originating protocol */ + int cmsg_type; /* protocol-specific type */ +} ; + +/*@constant int SCM_RIGHTS@*/ + +/*@exposed@*/ unsigned char *CMSG_DATA (/*@sef@*/ struct cmsghdr *) /*@*/ ; +/*@null@*/ /*@exposed@*/ struct cmsghdr *CMSG_NXTHDR (struct msghdr *, struct cmsghdr *) /*@*/ ; +/*@null@*/ /*@exposed@*/ struct cmsghdr *CMSG_FIRSTHDR (struct msghdr *) /*@*/ ; + +struct linger { + int l_onoff; + int l_linger; }; - struct cmsghdr { - u_int cmsg_len; /* data byte count, including hdr */ - int cmsg_level; /* originating protocol */ - int cmsg_type; /* protocol-specific type */ -/* followed by u_char cmsg_data[]; */ +/*@constant int SOCK_DGRAM@*/ +/*@constant int SOCK_RAW@*/ +/*@constant int SOCK_SEQPACKET@*/ +/*@constant int SOCK_STREAM@*/ + +/*@constant int SOL_SOCKET@*/ + +/*@constant int SO_ACCEPTCONN@*/ +/*@constant int SO_BROADCAST@*/ +/*@constant int SO_DEBUG@*/ +/*@constant int SO_DONTROUTE@*/ +/*@constant int SO_ERROR@*/ +/*@constant int SO_KEEPALIVE@*/ +/*@constant int SO_LINGER@*/ +/*@constant int SO_OOBINLINE@*/ +/*@constant int SO_RCVBUF@*/ +/*@constant int SO_RCVLOWAT@*/ +/*@constant int SO_RCVTIMEO@*/ +/*@constant int SO_REUSEADDR@*/ +/*@constant int SO_SNDBUF@*/ +/*@constant int SO_SNDLOWAT@*/ +/*@constant int SO_SNDTIMEO@*/ +/*@constant int SO_TYPE@*/ + +/*@constant int SOMAXCONN@*/ + +/*@constant int MSG_CTRUNC@*/ +/*@constant int MSG_DONTROUTE@*/ +/*@constant int MSG_EOR@*/ +/*@constant int MSG_OOB@*/ +/*@constant int MSG_PEEK@*/ +/*@constant int MSG_TRUNC@*/ +/*@constant int MSG_WAITALL@*/ + +/*@constant int AF_INET@*/ +/*@constant int AF_INET6@*/ +/*@constant int AF_UNIX@*/ +/*@constant int AF_UNSPEC@*/ + +/*@constant int SHUT_RD@*/ +/*@constant int SHUT_RDWR@*/ +/*@constant int SHUT_WR@*/ + +# if 0 +/* +** These were in the old unix.h spec, but are not in SUS6 +*/ + +struct sockproto { + u_short sp_family; /* address family */ + u_short sp_protocol; /* protocol */ }; - extern int -accept (int s, struct sockaddr *addr, int *addrlen) - /*@modifies *addrlen, errno@*/; +# endif - extern int -bind (int s, struct sockaddr *name, int namelen) - /*@modifies errno, fileSystem@*/; +int accept (int s, struct sockaddr *addr, int *addrlen) + /*@modifies *addrlen, errno@*/; - extern int -connect (int s, struct sockaddr *name, int namelen) - /*@modifies errno, internalState@*/; +int bind (int s, const struct sockaddr *name, int namelen) + /*@modifies errno, fileSystem@*/; -int getpeername (int s, /*@out@*/ struct sockaddr *name, size_t *namelen) - /*@modifies *name, *namelen, errno@*/; +int connect (int s, const struct sockaddr *name, int namelen) + /*@modifies errno, internalState@*/; -int getsockname (int s, struct sockaddr *address, size_t *address_len) - /*?requires maxSet(address) > *address_len@*/ +int getpeername (int s, /*@out@*/ struct sockaddr */*restrict*/ name, socklen_t */*restrict*/ namelen) + /*drl splint doesn't handle restrict yet*/ + /*@modifies *name, *namelen, errno@*/; + +#ifdef STRICT + +int getsockname (int s, /*@out@*/ struct sockaddr *address, socklen_t *address_len) + /*@i556@*/ /*: can't do this? requires maxSet(address) >= (*address_len) @*/ /*@modifies *address, *address_len, errno@*/; +#else +int getsockname (int s, /*@out@*/ struct sockaddr *address, socklen_t /*@alt size_t@*/ *address_len) + /*@i556@*/ /*: can't do this? requires maxSet(address) >= (*address_len) @*/ + /*@modifies *address, *address_len, errno@*/; + +#endif + int getsockopt (int s, int level, int optname, /*@out@*/ void *optval, size_t *optlen) /*@modifies *optval, *optlen, errno@*/; @@ -524,27 +645,11 @@ socketpair (int d, int type, int protocol, /*@out@*/ int *sv) 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@*/ @@ -680,9 +785,9 @@ mprotect (caddr_t addr, int len, int prot) /*@*/; 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) /*@*/; @@ -775,41 +880,17 @@ munlock (caddr_t addr, size_t len) /*@constant int MAXHOSTNAMELEN@*/ - extern void -FD_CLR (int n, fd_set *p) - /*@modifies *p@*/; - - extern void -FD_COPY (fd_set *f, /*@out@*/ fd_set *t) - /*@modifies *t@*/; +extern void FD_CLR (/*@sef@*/ int n, /*@sef@*/ fd_set *p) /*@modifies *p@*/ ; +extern void FD_COPY (/*@sef@*/ fd_set *f, /*@out@*/ fd_set *t) /*@modifies *t@*/ ; +extern int /*@alt _Bool@*/ FD_ISSET (/*@sef@*/ int n, /*@sef@*/ fd_set *p) /*@*/ ; +extern void FD_SET (/*@sef@*/ int n, /*@sef@*/ fd_set *p) /*@modifies *p@*/ ; +extern void FD_ZERO (/*@sef@*/ fd_set /*@out@*/ *p) /*@modifies *p@*/; - extern int /*@alt lltX_bool@*/ -FD_ISSET (int n, fd_set *p) - /*@*/; +extern int fchdir (int fd) /*@modifies internalState, errno@*/; +extern int fchown (int fd, uid_t owner, gid_t group) /*@modifies errno, fileSystem@*/; +extern int fsync (int fd) /*@modifies errno, fileSystem@*/; - extern void -FD_SET (int n, fd_set *p) - /*@modifies *p@*/; - - extern void -FD_ZERO (fd_set /*@out@*/ *p) - /*@modifies *p@*/; - - extern int -fchdir (int fd) - /*@modifies internalState, errno@*/; - - extern int -fchown (int fd, uid_t owner, gid_t group) - /*@modifies errno, fileSystem@*/; - - extern int -fsync (int fd) - /*@modifies errno, fileSystem@*/; - - extern int -ftruncate (int fd, off_t length) - /*@modifies errno, fileSystem@*/; +extern int ftruncate (int fd, off_t length) /*@modifies errno, fileSystem@*/; int gethostname (/*@out@*/ char *address, size_t address_len) /*:errorstatus@*/ @@ -818,50 +899,38 @@ int gethostname (/*@out@*/ char *address, size_t address_len) int initgroups (const char *name, int basegid) /*@modifies internalState@*/; - extern int -lchown (const char *path, uid_t owner, gid_t group) - /*@modifies errno, fileSystem@*/; - - extern int -readlink (const char *path, /*@out@*/ char *buf, int size) - /*@modifies *buf, errno@*/ /*@ensures result <= size @*/; - - extern int -select (int mfd, fd_set /*@null@*/ *r, fd_set /*@null@*/ *w, fd_set /*@null@*/ *e, struct timeval *t) - /*@modifies *r, *w, *e, *t, errno@*/; - - extern int -setegid (gid_t egid) - /*@modifies errno, internalState@*/; - - extern int -seteuid (uid_t euid) - /*@modifies errno, internalState@*/; - - extern int -setgroups (int ngroups, const gid_t *gidset) - /*@modifies errno, internalState@*/; - - extern int -setregid (gid_t rgid, gid_t egid) - /*@modifies errno, internalState@*/; - - extern int -setreuid (gid_t ruid, gid_t euid) - /*@modifies errno, internalState@*/; - - extern void -sync (void) - /*@modifies fileSystem@*/; - - extern int -symlink (const char *path, const char *path2) - /*@modifies fileSystem@*/; - - extern int -truncate (const char *name, off_t length) - /*@modifies errno, fileSystem@*/; - +int lchown (const char *path, uid_t owner, gid_t group) + /*@modifies errno, fileSystem@*/; + +int select (int mfd, fd_set /*@null@*/ *r, fd_set /*@null@*/ *w, + fd_set /*@null@*/ *e, /*@null@*/ struct timeval *t) + /*@modifies *r, *w, *e, *t, errno@*/; + /* evans - 2002-05-26: added null for t, bug reported by Enrico Scholz */ + +int setegid (gid_t egid) + /*@modifies errno, internalState@*/; + +int seteuid (uid_t euid) + /*@modifies errno, internalState@*/; + +int setgroups (int ngroups, const gid_t *gidset) + /*@modifies errno, internalState@*/; + +int setregid (gid_t rgid, gid_t egid) + /*@modifies errno, internalState@*/; + +int setreuid (gid_t ruid, gid_t euid) + /*@modifies errno, internalState@*/; + +void sync (void) + /*@modifies fileSystem@*/; + +int symlink (const char *path, const char *path2) + /*@modifies fileSystem@*/; + +int truncate (const char *name, off_t length) + /*@modifies errno, fileSystem@*/; + /*@constant int EBADRPC@*/ /*@constant int ERPCMISMATCH@*/ /*@constant int EPROGUNAVAIL@*/ @@ -872,9 +941,9 @@ truncate (const char *name, off_t length) /*@constant int ENEEDAUTH@*/ /*@constant int ELAST@*/ -/*________________________________________________________________________ - * tar.h - */ +/* +** tar.h +*/ /*@unchecked@*/ extern char *TMAGIC; /*@constant int TMAGLEN@*/ @@ -926,9 +995,9 @@ struct ipc_perm { /*@constant int IPC_SET@*/ /*@constant int IPC_STAT@*/ -/*________________________________________________________________________ - * sys/msg.h - */ +/* +** sys/msg.h +*/ struct msqid_ds { struct ipc_perm msg_perm; /* msg queue permission bits */ @@ -971,9 +1040,9 @@ msgrcv (int id, /*@out@*/ void *ptr, size_t nbytes, long type, int flags) msgsnd (int id, const void *ptr, size_t nbytes, int flag) /*@modifies errno@*/; -/*________________________________________________________________________ - * sys/sem.h - */ +/* +** sys/sem.h +*/ struct semid_ds { struct ipc_perm sem_perm; @@ -1035,9 +1104,9 @@ semget (key_t key, int nsems, int flag) semop (int id, struct sembuf *semoparray, size_t nops) /*@modifies errno@*/; -/*________________________________________________________________________ - * sys/shm.h - */ +/* +** sys/shm.h +*/ struct shmid_ds { struct ipc_perm shm_perm; @@ -1064,25 +1133,26 @@ semop (int id, struct sembuf *semoparray, size_t nops) /*@constant int SHM_W@*/ /*@constant int SHM_UNLOCK@*/ - void * -shmat (int id, /*@null@*/ void *addr, int flag) - /*@modifies errno@*/; +void * shmat (int id, /*@null@*/ void *addr, int flag) + /*@modifies errno@*/ ; + +extern int shmctl (int id, int cmd, /*@out@*/ struct shmid_ds *buf) + /*@modifies errno, *buf@*/ ; - extern int -shmctl (int id, int cmd, /*@out@*/ struct shmid_ds *buf) - /*@modifies errno, *buf@*/; +extern int shmdt (void *addr) + /*@modifies errno@*/ ; - extern int -shmdt (void *addr) - /*@modifies errno@*/; +extern int shmget (key_t key, int size, int flag) + /*@modifies errno@*/ ; - extern int -shmget (key_t key, int size, int flag) - /*@modifies errno@*/; -/*________________________________________________________________________ - * syslog.h - */ +/* +** stdio.h - in separte file stdio.h +*/ + +/* +** syslog.h +*/ /*@constant int LOG_EMERG@*/ /*@constant int LOG_ALERT@*/ @@ -1121,33 +1191,26 @@ shmget (key_t key, int size, int flag) /*@constant int LOG_NOWAIT@*/ /*@constant int LOG_PERROR@*/ - extern int -LOG_MASK (int pri) - /*@*/; - - extern int -LOG_UPTO (int pri) - /*@*/; - - extern void -closelog (void) - /*@modifies fileSystem@*/; - - extern void -openlog (const char *ident, int logopt, int facility) - /*@modifies fileSystem@*/; - - extern int -setlogmask (int maskpri) - /*@modifies internalState@*/; - - extern void /*@printflike@*/ -syslog (int priority, const char *message, ...) - /*@modifies fileSystem@*/; - - extern void -vsyslog (int priority, const char *message, va_list args) - /*@modifies fileSystem@*/; +int LOG_MASK (int pri) + /*@*/; + +int LOG_UPTO (int pri) + /*@*/; + +void closelog (void) + /*@modifies fileSystem@*/; + +void openlog (const char *ident, int logopt, int facility) + /*@modifies fileSystem@*/; + +int setlogmask (int maskpri) + /*@modifies internalState@*/; + +void /*@printflike@*/ syslog (int priority, const char *message, ...) + /*@modifies fileSystem@*/; + +void vsyslog (int priority, const char *message, va_list args) + /*@modifies fileSystem@*/; /*________________________________________________________________________ * pwd.h @@ -1169,29 +1232,20 @@ setpassent (int stayopen) setpwent (void) /*@modifies internalState@*/; -/*________________________________________________________________________ - * grp.h - */ +/* +** grp.h +*/ - extern void -endgrent (void) - /*@modifies internalState@*/; +void endgrent (void) /*@modifies internalState@*/; - extern /*@null@*/ struct group * -getgrent (void) - /*@modifies internalState@*/; +/*@null@*/ /*@observer@*/ struct group *getgrent (void) + /*@modifies internalState@*/; - extern int -setgrent (void) - /*@modifies internalState@*/; +int setgrent (void) /*@modifies internalState@*/; - extern void -setgrfile (const char *name) - /*@modifies internalState@*/; +void setgrfile (const char *name) /*@modifies internalState@*/; - extern int -setgroupent (int stayopen) - /*@modifies internalState@*/; +int setgroupent (int stayopen) /*@modifies internalState@*/; /* ** sys/stat.h @@ -1203,6 +1257,7 @@ setgroupent (int stayopen) ** 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 */ @@ -1219,18 +1274,9 @@ struct stat { this object. In some filesystem types, this may vary from file to file */ blkcnt_t st_blocks; /* number of blocks allocated for this object */ -} - -/*@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@*/ +} ; +/*@=redef@*/ /*@=matchfields@*/ -/*@constant mode_t S_IRWXU@*/ -/*@constant mode_t S_IRUSR@*/ /*@constant mode_t S_IWUSR@*/ /*@constant mode_t S_IXUSR@*/ /*@constant mode_t S_IRWXG@*/ @@ -1246,7 +1292,8 @@ struct stat { /*@constant mode_t S_ISVTX@*/ # if 0 -These are the old definitions - they don't appear to be in the Single UNIX Specification +/*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 S_IWRITE@*/ @@ -1274,23 +1321,23 @@ These are the old definitions - they don't appear to be in the Single UNIX Speci /*@constant int UF_APPEND@*/ # endif -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) /*@*/; +int /*@alt _Bool@*/ S_ISBLK (/*@sef@*/ __mode_t m) /*@*/; +int /*@alt _Bool@*/ S_ISCHR (/*@sef@*/ __mode_t m) /*@*/; +int /*@alt _Bool@*/ S_ISDIR (/*@sef@*/ __mode_t m) /*@*/; +int /*@alt _Bool@*/ S_ISFIFO (/*@sef@*/ __mode_t m) /*@*/; +int /*@alt _Bool@*/ S_ISREG (/*@sef@*/ __mode_t m) /*@*/; +int /*@alt _Bool@*/ S_ISLNK (/*@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) /*@*/ ; +int /*@alt _Bool@*/ S_TYPEISMQ (/*@sef@*/ struct stat *buf) /*@*/ ; +int /*@alt _Bool@*/ S_TYPEISSEM (/*@sef@*/ struct stat *buf) /*@*/ ; +int /*@alt _Bool@*/ S_TYPEISSHM (/*@sef@*/ struct stat *buf) /*@*/ ; /* in POSIX: chmod, fstat, mkdir, mkfifo, stat, umask */ int lstat(const char *, /*@out@*/ struct stat *) - /*:errorcode -1:*/ - /*@modifies errno@*/ ; - + /*:errorcode -1:*/ + /*@modifies 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:*/ @@ -1304,6 +1351,39 @@ int fchflags (int fd, u_long flags) /*@warn unixstandard "Not in Single UNIX Specification Version 2"@*/ /*@modifies fileSystem, errno@*/; +/* evans 2002-03-17: this was missing, reported by Ralf Wildenhues */ +int fchmod(int fildes, mode_t mode) + /*@modifies fileSystem, errno@*/ ; + +/* +** sys/statvfs.h +** from http://www.opengroup.org/onlinepubs/007908799/xsh/sysstatvfs.h.html +*/ + +struct statvfs { + unsigned long f_bsize; + unsigned long f_frsize; + fsblkcnt_t f_blocks; + fsblkcnt_t f_bfree; + fsblkcnt_t f_bavail; + fsfilcnt_t f_files; + fsfilcnt_t f_ffree; + fsfilcnt_t f_favail; + unsigned long f_fsid; + unsigned long f_flag; + unsigned long f_namemax; +} ; + +/*@constant unsigned long ST_RDONLY; @*/ +/*@constant unsigned long ST_NOSUID; @*/ + +int fstatvfs (int fildes, /*@out@*/ struct statvfs *buf) + /*@modifies buf@*/ ; + +int statvfs (const char *path, /*@out@*/ struct statvfs *buf) + /*@modifies buf@*/ ; + + /*________________________________________________________________________ * stropts.h */ @@ -1351,82 +1431,62 @@ getpmsg (int fd, /*@out@*/ struct strbuf *c, /*@out@*/ struct strbuf *d, int *b, 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 - */ +/* +** sys/resource.h +** +** Update 2002-07-09 from +** http://www.opengroup.org/onlinepubs/007904975/basedefs/sys/resource.h.html +*/ -/*@constant int RLIMIT_CPU@*/ -/*@constant int RLIMIT_FSIZE@*/ -/*@constant int RLIMIT_DATA@*/ -/*@constant int RLIMIT_STACK@*/ -/*@constant int RLIMIT_CORE@*/ -/*@constant int RLIMIT_RSS@*/ -/*@constant int RLIMIT_MEMLOCK@*/ -/*@constant int RLIMIT_NPROC@*/ -/*@constant int RLIMIT_NOFILE@*/ -/*@constant int RLIM_NLIMITS@*/ -/*@constant int RLIM_INFINITY@*/ -/*@constant int PRIO_MIN@*/ -/*@constant int PRIO_MAX@*/ /*@constant int PRIO_PROCESS@*/ /*@constant int PRIO_PGRP@*/ /*@constant int PRIO_USER@*/ + +typedef /*@unsignedintegraltype@*/ rlim_t; + +/*@constant rlim_t RLIM_INFINITY@*/ +/*@constant rlim_t RLIM_SAVED_MAX@*/ +/*@constant rlim_t RLIM_SAVED_CUR@*/ + /*@constant int RUSAGE_SELF@*/ /*@constant int RUSAGE_CHILDREN@*/ - struct rusage { - struct timeval ru_utime; /* user time used */ - struct timeval ru_stime; /* system time used */ - long ru_maxrss; /* max resident set size */ - long ru_ixrss; /* integral shared memory size */ - long ru_idrss; /* integral unshared data " */ - long ru_isrss; /* integral unshared stack " */ - long ru_minflt; /* page reclaims */ - long ru_majflt; /* page faults */ - long ru_nswap; /* swaps */ - long ru_inblock; /* block input operations */ - long ru_oublock; /* block output operations */ - long ru_msgsnd; /* messages sent */ - long ru_msgrcv; /* messages received */ - long ru_nsignals; /* signals received */ - long ru_nvcsw; /* voluntary context switches */ - long ru_nivcsw; /* involuntary " */ +struct rlimit { + rlim_t rlim_cur; + rlim_t rlim_max; }; - struct rlimit { - long rlim_cur; - long rlim_max; +struct rusage { + struct timeval ru_utime; /* user time used */ + struct timeval ru_stime; /* system time used */ + /* other members optional */ }; - struct loadavg { - unsigned long ldavg[3]; - long fscale; -}; - - extern int -getpriority (int which, int who) - /*@modifies errno@*/; +/*@constant int RLIMIT_CORE@*/ +/*@constant int RLIMIT_CPU@*/ +/*@constant int RLIMIT_DATA@*/ +/*@constant int RLIMIT_FSIZE@*/ +/*@constant int RLIMIT_NOFILE@*/ +/*@constant int RLIMIT_STACK@*/ +/*@constant int RLIMIT_AS@*/ - extern int -getrlimit (int res, /*@out@*/ struct rlimit *rlp) - /*@modifies *rlp, errno@*/; +int getpriority (int which, id_t who) + /*@modifies errno@*/; - extern int -getrusage (int who, /*@out@*/ struct rusage *rusage) - /*@modifies *rusage, errno@*/; +int getrlimit (int res, /*@out@*/ struct rlimit *rlp) + /*@modifies *rlp, errno@*/; - extern int -setpriority (int which, int who, int prio) - /*@modifies errno, internalState@*/; +int getrusage (int who, /*@out@*/ struct rusage *rusage) + /*@modifies *rusage, errno@*/; - extern int -setrlimit (int resource, const struct rlimit *rlp) - /*@modifies errno, internalState@*/; +int setpriority (int which, id_t who, int prio) + /*@modifies errno, internalState@*/; +int setrlimit (int resource, const struct rlimit *rlp) + /*@modifies errno, internalState@*/; /* ** in @@ -1458,10 +1518,8 @@ struct servent *getservbyport_r (int port, /*@null@*/ const char *proto, /*@out@ /*@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) @@ -1472,15 +1530,15 @@ struct hostent *gethostbyname_r (/*@nullterminated@*/ const char *name, /*@notnu /*@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"@*/ ; @@ -1488,17 +1546,13 @@ struct hostent *gethostbyaddr_r (/*@notnull@*/ const void *addr, size_t addrlen, 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 { @@ -1511,36 +1565,450 @@ struct hostent { } ; /* -** arpa/inet.h +** unistd.h +** from http://www.opengroup.org/onlinepubs/007908799/xsh/unistd.h.html */ -typedef uint32_t in_addr_t; +/*@constant int _POSIX_VERSION@*/ +/*@constant int _POSIX2_VERSION@*/ +/*@constant int _POSIX2_C_VERSION@*/ +/*@constant int _XOPEN_VERSION@*/ +/*@constant int _XOPEN_XCU_VERSION@*/ + +/* for access: */ + +/*@constant int R_OK@*/ +/*@constant int W_OK@*/ +/*@constant int X_OK@*/ +/*@constant int F_OK@*/ + +/* for confstr: */ +/*@constant int _CS_PATH@*/ +/*@constant int _CS_XBS5_ILP32_OFF32_CFLAGS@*/ +/*@constant int _CS_XBS5_ILP32_OFF32_LDFLAGS@*/ +/*@constant int _CS_XBS5_ILP32_OFF32_LIBS@*/ +/*@constant int _CS_XBS5_ILP32_OFF32_LINTFLAGS@*/ +/*@constant int _CS_XBS5_ILP32_OFFBIG_CFLAGS@*/ +/*@constant int _CS_XBS5_ILP32_OFFBIG_LDFLAGS@*/ +/*@constant int _CS_XBS5_ILP32_OFFBIG_LIBS@*/ +/*@constant int _CS_XBS5_ILP32_OFFBIG_LINTFLAGS@*/ +/*@constant int _CS_XBS5_LP64_OFF64_CFLAGS@*/ +/*@constant int _CS_XBS5_LP64_OFF64_LDFLAGS@*/ +/*@constant int _CS_XBS5_LP64_OFF64_LIBS@*/ +/*@constant int _CS_XBS5_LP64_OFF64_LINTFLAGS@*/ +/*@constant int _CS_XBS5_LPBIG_OFFBIG_CFLAGS@*/ +/*@constant int _CS_XBS5_LPBIG_OFFBIG_LDFLAGS@*/ +/*@constant int _CS_XBS5_LPBIG_OFFBIG_LIBS@*/ +/*@constant int _CS_XBS5_LPBIG_OFFBIG_LINTFLAGS@*/ + +/* name parameters to sysconf: */ + +/*@constant int _SC_2_C_BIND@*/ +/*@constant int _SC_2_C_DEV@*/ +/*@constant int _SC_2_C_VERSION@*/ +/*@constant int _SC_2_FORT_DEV@*/ +/*@constant int _SC_2_FORT_RUN@*/ +/*@constant int _SC_2_LOCALEDEF@*/ +/*@constant int _SC_2_SW_DEV@*/ +/*@constant int _SC_2_UPE@*/ +/*@constant int _SC_2_VERSION@*/ +/*@constant int _SC_ARG_MAX@*/ +/*@constant int _SC_AIO_LISTIO_MAX@*/ +/*@constant int _SC_AIO_MAX@*/ +/*@constant int _SC_AIO_PRIO_DELTA_MAX@*/ +/*@constant int _SC_ASYNCHRONOUS_IO@*/ +/*@constant int _SC_ATEXIT_MAX@*/ +/*@constant int _SC_BC_BASE_MAX@*/ +/*@constant int _SC_BC_DIM_MAX@*/ +/*@constant int _SC_BC_SCALE_MAX@*/ +/*@constant int _SC_BC_STRING_MAX@*/ +/*@constant int _SC_CHILD_MAX@*/ +/*@constant int _SC_CLK_TCK@*/ +/*@constant int _SC_COLL_WEIGHTS_MAX@*/ +/*@constant int _SC_DELAYTIMER_MAX@*/ +/*@constant int _SC_EXPR_NEST_MAX@*/ +/*@constant int _SC_FSYNC@*/ +/*@constant int _SC_GETGR_R_SIZE_MAX@*/ +/*@constant int _SC_GETPW_R_SIZE_MAX@*/ +/*@constant int _SC_IOV_MAX@*/ +/*@constant int _SC_JOB_CONTROL@*/ +/*@constant int _SC_LINE_MAX@*/ +/*@constant int _SC_LOGIN_NAME_MAX@*/ +/*@constant int _SC_MAPPED_FILES@*/ +/*@constant int _SC_MEMLOCK@*/ +/*@constant int _SC_MEMLOCK_RANGE@*/ +/*@constant int _SC_MEMORY_PROTECTION@*/ +/*@constant int _SC_MESSAGE_PASSING@*/ +/*@constant int _SC_MQ_OPEN_MAX@*/ +/*@constant int _SC_MQ_PRIO_MAX@*/ +/*@constant int _SC_NGROUPS_MAX@*/ +/*@constant int _SC_OPEN_MAX@*/ +/*@constant int _SC_PAGESIZE@*/ +/*@constant int _SC_PAGE_SIZE@*/ +/*@constant int _SC_PASS_MAX@*/ +/*@constant int _SC_PRIORITIZED_IO@*/ +/*@constant int _SC_PRIORITY_SCHEDULING@*/ +/*@constant int _SC_RE_DUP_MAX@*/ +/*@constant int _SC_REALTIME_SIGNALS@*/ +/*@constant int _SC_RTSIG_MAX@*/ +/*@constant int _SC_SAVED_IDS@*/ +/*@constant int _SC_SEMAPHORES@*/ +/*@constant int _SC_SEM_NSEMS_MAX@*/ +/*@constant int _SC_SEM_VALUE_MAX@*/ +/*@constant int _SC_SHARED_MEMORY_OBJECTS@*/ +/*@constant int _SC_SIGQUEUE_MAX@*/ +/*@constant int _SC_STREAM_MAX@*/ +/*@constant int _SC_SYNCHRONIZED_IO@*/ +/*@constant int _SC_THREADS@*/ +/*@constant int _SC_THREAD_ATTR_STACKADDR@*/ +/*@constant int _SC_THREAD_ATTR_STACKSIZE@*/ +/*@constant int _SC_THREAD_DESTRUCTOR_ITERATIONS@*/ +/*@constant int _SC_THREAD_KEYS_MAX@*/ +/*@constant int _SC_THREAD_PRIORITY_SCHEDULING@*/ +/*@constant int _SC_THREAD_PRIO_INHERIT@*/ +/*@constant int _SC_THREAD_PRIO_PROTECT@*/ +/*@constant int _SC_THREAD_PROCESS_SHARED@*/ +/*@constant int _SC_THREAD_SAFE_FUNCTIONS@*/ +/*@constant int _SC_THREAD_STACK_MIN@*/ +/*@constant int _SC_THREAD_THREADS_MAX@*/ +/*@constant int _SC_TIMERS@*/ +/*@constant int _SC_TIMER_MAX@*/ +/*@constant int _SC_TTY_NAME_MAX@*/ +/*@constant int _SC_TZNAME_MAX@*/ +/*@constant int _SC_VERSION@*/ +/*@constant int _SC_XOPEN_VERSION@*/ +/*@constant int _SC_XOPEN_CRYPT@*/ +/*@constant int _SC_XOPEN_ENH_I18N@*/ +/*@constant int _SC_XOPEN_SHM@*/ +/*@constant int _SC_XOPEN_UNIX@*/ +/*@constant int _SC_XOPEN_XCU_VERSION@*/ +/*@constant int _SC_XOPEN_LEGACY@*/ +/*@constant int _SC_XOPEN_REALTIME@*/ +/*@constant int _SC_XOPEN_REALTIME_THREADS@*/ +/*@constant int _SC_XBS5_ILP32_OFF32@*/ +/*@constant int _SC_XBS5_ILP32_OFFBIG@*/ +/*@constant int _SC_XBS5_LP64_OFF64@*/ +/*@constant int _SC_XBS5_LPBIG_OFFBIG@*/ + + +int access(const char *, int) /*@modifies errno@*/ /*:errorcode -1:*/ ; +unsigned int alarm (unsigned int) /*@modifies internalState@*/ ; + +int brk(void *) + /*@modifies errno@*/ + /*:errorcode -1:*/ + /*@warn legacy "brk is obsolete"@*/ ; + +int chdir (const char *) + /*@modifies internalState, errno@*/ + /*:errorcode -1:*/ ; + +int chown (const char *, uid_t, gid_t) + /*@modifies internalState, errno@*/ + /*:errorcode -1:*/ ; + +int close (int) + /*@modifies internalState, errno@*/ + /*:errorcode -1:*/ ; + +size_t confstr(int, /*@null@*/ char *, size_t) + /*@globals internalState@*/ + /*@modifies errno@*/ + /*:errorcode 0:*/ ; + +/*@dependent@*/ /*@null@*/ char *crypt(const char *, const char *) + /*@modifies errno, internalState@*/ ; + +/*@dependent@*/ /*@null@*/ char *ctermid(/*@returned@*/ /*@null@*/ /*@out@*/ char *s) + /*@modifies s@*/ ; + +/*@null@*/ /*@dependent@*/ char *cuserid (/*@null@*/ /*@returned@*/ char *s) + /*@warn legacy "cuserid is obsolete"@*/ + /*@modifies s@*/ ; + +int dup(int) + /*@modifies errno, internalState@*/ + /*:errorcode -1:*/ ; + +int dup2(int, int) + /*@modifies errno, internalState@*/ + /*:errorcode -1:*/ ; + +void encrypt(char p_block[], int) + /*@requires maxSet(p_block) == 63@*/ + /*@modifies p_block, errno@*/ ; + +extern char **environ; + +int execl (const char *, const char *, ...) + /*@modifies errno, internalState@*/ + /*:errorcode -1:*/ ; + +int execle(const char *, const char *, ...) + /*@modifies errno, internalState@*/ + /*:errorcode -1:*/ ; + +int execlp(const char *, const char *, ...) + /*@modifies errno, internalState@*/ + /*:errorcode -1:*/ ; + +int execv(const char *, char *const []) + /*@modifies errno, internalState@*/ + /*:errorcode -1:*/ ; + +int execve(const char *, char *const [], char *const []) + /*@modifies errno, internalState@*/ + /*:errorcode -1:*/ ; + +int execvp(const char *, char *const []) + /*@modifies errno, internalState@*/ + /*:errorcode -1:*/ ; + +/*@exits@*/ void _exit (int); + +int fchown (int, uid_t, gid_t) + /*@modifies errno, fileSystem@*/ + /*:errorcode -1:*/ ; + +int fchdir (int) + /*@modifies errno, fileSystem@*/ + /*:errorcode -1:*/ ; -struct in_addr -{ - in_addr_t s_addr; -}; +int fdatasync (int) + /*@modifies errno, fileSystem@*/ + /*:errorcode -1:*/ ; -typedef uint16_t in_port_t; +pid_t fork (void) + /*@modifies errno, internalState@*/ + /*:errorcode -1:*/ ; -in_addr_t htonl (in_addr_t hostlong) /*@*/ ; -in_port_t htons (in_port_t hostshort) /*@*/ ; -in_addr_t ntohl (in_addr_t netlong) /*@*/ ; -in_port_t ntohs (in_port_t netshort) /*@*/ ; +long int fpathconf(int, int) + /*@modifies errno, internalState@*/ + /*:errorcode -1:*/ ; + +int fsync(int) + /*@modifies errno, fileSystem@*/ + /*:errorcode -1:*/ ; + +int ftruncate(int, off_t) + /*@modifies errno, fileSystem@*/ + /*:errorcode -1:*/ ; + +/*@null@*/ char *getcwd (/*@returned@*/ char *buf, size_t size) + /*@requires maxSet(buf) >= size;@*/ + /*@modifies errno@*/ ; + +int getdtablesize (void) + /*@warn legacy "getdtablesize is obsolete"@*/ ; + +gid_t getegid (void) /*@globals internalState*/ ; +uid_t geteuid (void) /*@globals internalState*/ ; +gid_t getgid (void) /*@globals internalState*/ ; + +int getgroups (int gidsetsize, gid_t grouplist[]) + /*@requires maxSet(grouplist) >= gidsetsize@*/ + /*@modifies errno@*/ + /*:errorcode -1:*/ ; + +long gethostid (void) /*@globals internalState@*/ ; + +/*@null@*/ /*@dependent@*/ char *getlogin (void) + /*@modifies errno@*/ ; + +int getlogin_r (char *name, size_t namesize) + /*@requires maxSet(name) >= namesize@*/ + /*:errorcode !0:*/ ; + +extern char *optarg; +extern int optind; +extern int opterr; +extern int optopt; + +int getopt(int, char * const [], const char *) + /*@modifies optind, opterr, optopt, errno@*/ + /*:errorcode -1:*/ ; + +int getpagesize(void) + /*@warn legacy "getpagesize is obsolete"@*/ ; + +/*@dependent@*/ /*@null@*/ char *getpass(/*@nullterminated@*/ const char *) + /*@warn legacy "getpass is obsolete"@*/ ; + +pid_t getpgid(pid_t) + /*@modifies errno@*/ + /*@globals internalState@*/ + /*:errorcode (pid_t)-1:*/ ; + +pid_t getpgrp(void) /*@globals internalState*/ ; + +pid_t getpid(void) /*@globals internalState*/ ; +pid_t getppid(void) /*@globals internalState*/ ; + +pid_t getsid(pid_t) + /*@modifies errno@*/ + /*@globals internalState@*/ + /*:errorcode (pid_t)-1:*/ ; + +uid_t getuid(void) /*@globals internalState@*/ ; + +/*@null@*/ char *getwd (/*@returned@*/ char *path_name) + /*@modifies path_name@*/ ; + +int isatty(int) + /*@globals internalState@*/ + /*@modifies errno@*/ + /*:errorcode 0:*/ ; + +int lchown(const char *, uid_t, gid_t) + /*@modifies errno, fileSystem@*/ + /*:errorcode -1:*/ ; + +int link(const char *, const char *) + /*@modifies errno, fileSystem@*/ + /*:errorcode -1:*/ ; + +int lockf(int, int, off_t) + /*@modifies errno, fileSystem@*/ + /*:errorcode -1:*/ ; + +off_t lseek(int, off_t, int) + /*@modifies errno, fileSystem@*/ + /*:errorcode (off_t)-1:*/ ; + +int nice(int) + /*@modifies errno, fileSystem@*/ + /*:errorcode -1:*/ ; + +long int pathconf(const char *, int) + /*@modifies errno, internalState@*/ + /*:errorcode -1:*/ ; + +int pause(void) + /*@modifies errno, internalState@*/ + /*:errorcode -1:*/ ; + +int pipe(int p[]) + /*@requires maxRead(p) == 1@*/ + /*@modifies errno, fileSystem@*/ + /*:errorcode -1:*/ ; + +ssize_t pread(int, /*@out@*/ void *buf, size_t nbyte, off_t offset) + /*@modifies errno, fileSystem@*/ + /*@requires maxSet(buf) >= (nbyte - 1) @*/ + /*@ensures maxRead(buf) >= nbyte @*/ + /*:errorcode -1:*/ ; + +int pthread_atfork(void (*)(void), void (*)(void), void(*)(void)) + /*@modifies errno, fileSystem@*/ + /*:errorcode !0:*/ ; + +ssize_t pwrite(int, const void *buf, size_t nbyte, off_t) + /*@requires maxRead(buf) >= nbyte@*/ + /*@modifies errno, fileSystem@*/ + /*:errorcode -1:*/ ; + +/* ssize_t read(int, void *, size_t); in posix.h */ + +int readlink(const char *, char *buf, size_t bufsize) + /*@requires maxSet(buf) >= (bufsize - 1)@*/ + /*@modifies errno, fileSystem, *buf@*/ + /*:errorcode -1:*/ ; + +/* int rmdir(const char *); in posix.h */ + +void *sbrk(intptr_t) + /*@modifies errno@*/ + /*:errorcode (void *)-1:*/ + /*@warn legacy "sbrk is obsolete"@*/ ; + + /* int setgid(gid_t); + int setpgid(pid_t, pid_t); + */ + +pid_t setpgrp(void) /*@modifies internalState@*/ ; + +int setregid(gid_t, gid_t) + /*@modifies errno, internalState@*/ + /*:errorcode -1:*/ ; + +int setreuid(uid_t, uid_t) + /*@modifies errno, internalState@*/ + /*:errorcode -1:*/ ; + +pid_t setsid(void) + /*@modifies errno, internalState@*/ + /*:errorcode (pid_t) -1:*/ ; + +int setuid(uid_t) + /*@modifies errno, internalState@*/ + /*:errorcode -1:*/ ; + +unsigned int sleep(unsigned int) + /*@modifies systemState@*/ ; + +void swab(/*@unique@*/ const void *src, /*@unique@*/ void *dest, ssize_t nbytes) + /*@requires maxSet(dest) >= (nbytes - 1)@*/ ; + +int symlink(const char *, const char *) + /*@modifies errno, fileSystem@*/ + /*:errorcode -1:*/ ; + +void sync(void) /*@modifies systemState@*/ ; + +long int sysconf(int) + /*@modifies errno, systemState@*/ + /*:errorcode -1:*/ ; + +pid_t tcgetpgrp(int) + /*@globals systemState@*/ + /*@modifies errno@*/ + /*:errorcode -1:*/ ; + +int tcsetpgrp(int, pid_t) + /*@modifies errno, systemState@*/ + /*:errorcode -1:*/ ; + +int truncate(const char *, off_t) + /*@modifies errno, fileSystem@*/ + /*:errorcode -1:*/ ; + +/*@dependent@*/ /*@null@*/ char *ttyname(int) + /*@globals systemState@*/ + /*@modifies errno@*/ + /*:errorcode -1:*/ ; + +int ttyname_r(int, char *name, size_t namesize) + /*@requires maxSet(name) >= (namesize - 1)@*/ ; + /*:errorcode !0:*/ ; + +useconds_t ualarm(useconds_t, useconds_t) + /*@modifies systemState@*/ ; + +int unlink(const char *) + /*@modifies fileSystem, errno@*/ + /*:errorcode -1:*/ ; + +int usleep(useconds_t) + /*@modifies fileSystem, errno@*/ + /*:errorcode -1:*/ ; + +pid_t vfork(void) + /*@modifies fileSystem, errno@*/ + /*:errorcode -1:*/ ; + + /* in posix.h ssize_t write(int, const void *, size_t); */ -/* -** unistd.h -*/ int chroot (/*@notnull@*/ /*@nullterminated@*/ const char *path) - /*:statusreturn@*/ - /*@warn superuser "Only super-user processes may call chroot."@*/ - /*: other wanings? */ ; + /*@modifies internalState, errno@*/ + /*:errorcode -1:*/ + /*@warn superuser "Only super-user processes may call chroot."@*/ ; int fchroot (int fildes) /*:statusreturn@*/ /*@warn superuser "Only super-user processes may call fchroot."@*/ ; + /* ** ctype.h ** @@ -1548,15 +2016,184 @@ int fchroot (int fildes) */ # ifdef STRICT -lltX_bool isascii(int) /*@*/ ; -lltX_bool toascii(int) /*@*/ ; +_Bool isascii(int) /*@*/ ; +_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@*/); +_Bool /*@alt int@*/ isascii(int /*@alt unsigned char@*/) /*@*/ ; +_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 +*/ + +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. */ + +/* sa_family_t moved earlier */ + +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 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 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_addr_t ntohl (in_addr_t netlong) /*@*/ ; +in_port_t ntohs (in_port_t netshort) /*@*/ ; + +/* +** dirent.h +** +** evans 2001-08-27 - added from http://www.opengroup.org/onlinepubs/007908799/xsh/dirent.h.html +*/ + +/*@-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@*/ /*@dependent@*/ DIR *opendir(const char *) /*@modifies errno, fileSystem@*/ ; + +/* in posix.h: struct dirent *readdir(DIR *); */ + +int readdir_r (DIR *, struct dirent *, /*@out@*/ struct dirent **result) + /*@modifies *result@*/ + /*:errorcode !0:*/ ; + +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 */ + /*not sure what the exact size of this is + also can IPv6 use this function? + */ + /*I'm going to assume that the address had the format: + "###.###.###.###" which is 16 bytes*/ + + /*@kept@*/ 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 */; + + + + + +