/*@-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;
int ioctl (int d, int /*@alt long@*/ request, /*@out@*/ void *arg)
/*@modifies *arg, errno@*/ ; /* depends on request! */
-int gethostname (/*@out@*/ char *address, int address_len)
- /*@modifies address@*/ ;
-
pid_t vfork (void) /*@modifies fileSystem@*/ ;
- struct iovec {
- void *iov_base;
- size_t iov_len;
+struct iovec {
+ void *iov_base;
+ size_t iov_len;
};
/*@constant int UIO_MAXIOV@*/ /* BSD */
connect (int s, struct sockaddr *name, int namelen)
/*@modifies errno, internalState@*/;
- extern int
-getpeername (int s, /*@out@*/ struct sockaddr *name, int *namelen)
+int getpeername (int s, /*@out@*/ struct sockaddr *name, size_t *namelen)
/*@modifies *name, *namelen, errno@*/;
- extern int
-getsockname (int s, struct sockaddr *name, int *namelen)
- /*@modifies *name, *namelen, errno@*/;
+int getsockname (int s, struct sockaddr *address, size_t *address_len)
+ /*: can't do this? requires maxSet(address) >= (*address_len) @*/
+ /*@modifies *address, *address_len, errno@*/;
- extern int
-getsockopt (int s, int level, int optname, /*@out@*/ void *optval, int *optlen)
+int getsockopt (int s, int level, int optname, /*@out@*/ void *optval, size_t *optlen)
/*@modifies *optval, *optlen, errno@*/;
extern int
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)
/*@*/;
ftruncate (int fd, off_t length)
/*@modifies errno, fileSystem@*/;
- extern int
-gethostname (/*@out@*/ char *name, int namlen)
- /*@modifies *name@*/;
+int gethostname (/*@out@*/ char *address, size_t address_len)
+ /*:errorstatus@*/
+ /*@modifies address@*/ ;
- extern int
-initgroups (const char *name, int basegid)
- /*@modifies internalState@*/;
+int initgroups (const char *name, int basegid)
+ /*@modifies internalState@*/;
extern int
lchown (const char *path, uid_t owner, gid_t group)
extern int
readlink (const char *path, /*@out@*/ char *buf, int size)
- /*@modifies *buf, errno@*/;
+ /*@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)
shmget (key_t key, int size, int flag)
/*@modifies errno@*/;
-
-/*________________________________________________________________________
- * regex.h -- intended to be POSIX 1003.2 compliant
- */
-
- typedef off_t regoff_t;
-
- typedef struct {
- int re_magic;
- size_t re_nsub; /* number of parenthesized subexpressions */
- char *re_endp; /* end pointer for REG_PEND */
- struct re_guts *re_g; /* none of your business :-) */
-} regex_t;
-
- typedef struct {
- regoff_t rm_so; /* start of match */
- regoff_t rm_eo; /* end of match */
-} regmatch_t;
-
-/* 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@*/
-
- extern int
-regcomp (/*@out@*/ regex_t *preg, const char *pattern, int flags)
- /*@modifies *preg@*/;
-
- extern size_t
-regerror (int code, const regex_t *re, /*@out@*/ char *errbuf, size_t bufsize)
- /*@modifies *errbuf@*/;
-
- extern int
-regexec (const regex_t *preg, const char *s, size_t n, /*@out@*/ regmatch_t *m, int f)
- /*@modifies *m@*/;
-
- extern void
-regfree (regex_t *p)
- /*@modifies *p@*/;
-
/*________________________________________________________________________
* syslog.h
*/
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
setrlimit (int resource, const struct rlimit *rlp)
/*@modifies errno, internalState@*/;
+
+/*
+** in <netdb.h>
+*/
+
+struct servent
+{
+ /*@observer@*/ char *s_name; /* Official service name. */
+ /*@observer@*/ char **s_aliases; /* Alias list. */
+ int s_port; /* Port number. */
+ /*@observer@*/ char *s_proto; /* Protocol to use. */
+} ;
+
+/*@observer@*/ /*@dependent@*/ /*@null@*/ struct servent *getservbyname (const char *name, /*@null@*/ const char *proto)
+ /*@warn multithreaded "Unsafe in multithreaded applications, use getsrvbyname_r instead"@*/ ;
+
+struct servent *getservbyname_r (const char *name, /*@null@*/ const char *proto, /*@out@*/ /*@returned@*/ struct servent *result, /*@out@*/ char *buffer, int buflen)
+ /*@requires maxSet (buffer) >= buflen@*/ ;
+
+
+/*@observer@*/ /*@dependent@*/ struct servent *getservbyport (int port, /*@null@*/ const char *proto)
+ /*@warn multithreaded "Unsafe in multithreaded applications, use getservbyport_r instead"@*/ ;
+
+struct servent *getservbyport_r (int port, /*@null@*/ const char *proto, /*@out@*/ /*@returned@*/ struct servent *result, /*@out@*/ char *buffer, int buflen)
+ /*@requires maxSet (buffer) >= buflen@*/ ;
+
+/*@null@*/ struct servent *getservent (void);
+
+/*@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)
+ /*@warn multithreaded "Unsafe in multithreaded applications, use gethostbyname_r instead"@*/
+ /*@modifies h_errno@*/ ;
+
+struct hostent *gethostbyname_r (/*@nullterminated@*/ const char *name, /*@notnull@*/ /*@returned@*/ struct hostent *hent, /*@out@*/ /*@exposed@*/ char *buffer, int bufsize, /*@out@*/ int *h_errnop)
+ /*@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? */
+ /*@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? */ ;
+
+/*@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);
+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 {
+ /*@observer@*/ /*@nullterminated@*/ char *h_name; /* official name of host */
+ /*@observer@*/ /*@nullterminated@*/ char * /*:observer@*/ /*:nullterminated@*/ *h_aliases; /* alias list */
+ int h_addrtype; /* host address type*/
+ int h_length; /* length ofaddress*/
+ /*@observer@*/ /*@nullterminated@*/ char * /*:observer@*/ /*:nullterminated@*/ *h_addr_list; /* list of addressesfrom name server */
+ /*@observer@*/ /*@nullterminated@*/ char *h_addr; /* first address in list (backward compatibility) */
+} ;
+
+/*
+** unistd.h
+*/
+
+int chroot (/*@notnull@*/ /*@nullterminated@*/ const char *path)
+ /*:statusreturn@*/
+ /*@warn superuser "Only super-user processes may call chroot."@*/
+ /*: other wanings? */ ;
+
+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
+*/
+
+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_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@*/ 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 */;
+
+
+
+
+
+
andersk / splint.git / blobdiff