typedef /*@integraltype@*/ blkcnt_t;
typedef /*@integraltype@*/ blksize_t;
+
+/*@-redef@*/ /* These are also defined by ansi.h: */
typedef /*@integraltype@*/ clock_t;
-typedef /*@integraltype@*/ clockid_t;
typedef /*@integraltype@*/ dev_t;
-typedef /*@unsignedintegraltype@*/ fsblkcnt_t;
-typedef /*@unsignedintegraltype@*/ fsfilcnt_t;
typedef /*@integraltype@*/ gid_t;
-typedef /*@integraltype@*/ id_t;
typedef /*@unsignedintegraltype@*/ ino_t;
-typedef /*@integraltype@*/ key_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_rwlockattr_t;
typedef /*@integraltype@*/ pthread_t;
typedef /*@signedintegraltype@*/ suseconds_t;
-typedef /*@integraltype@*/ time_t;
typedef /*@integraltype@*/ timer_t;
-typedef /*@integraltype@*/ uid_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 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 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)
** 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 */
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_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_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 */
/*@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 {
/*@observer@*/ /*@nullterminated@*/ char *h_addr; /* first address in list (backward compatibility) */
} ;
-/*
-** arpa/inet.h
-*/
-
-typedef uint32_t in_addr_t;
-
-struct in_addr
-{
- in_addr_t s_addr;
-};
-
-typedef uint16_t in_port_t;
-
-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) /*@*/ ;
-
/*
** unistd.h
*/
*/
double drand48 (void) /*@modifies internalState@*/ ;
-double erand48 (unsigned short int xsubi[3]) /*@modifies internalState@*/ ;
+double erand48 (unsigned short int /*@-fixedformalarray@*/ xsubi[3] /*@=fixedformalarray@*/ )
+ /*@modifies internalState@*/ ;
+
void srand48 (long int seedval) /*@modifies internalState@*/ ;
/*
/*@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 */
+/*:i32 need to check annotations on these */
+
int closedir (DIR *) /*:errorcode -1*/ ;
/*@null@*/ DIR *opendir(const char *) ;
struct dirent *readdir(DIR *);
/*@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