+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 */;
+
+
+
+
+