X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/ccf415d04c64eb5eeabd11a28ec3028efb9fd042..f6753ca7324b8b367b49a83666614bafaf62d9df:/lib/stdlib.h

diff --git a/lib/stdlib.h b/lib/stdlib.h
index 809988a..8c7c462 100644
--- a/lib/stdlib.h
+++ b/lib/stdlib.h
@@ -26,11 +26,22 @@ int (*compar)(const void *, const void *)) /*@*/
      extern /*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/
   /*@ensures MaxSet(result) == (nobj - 1); @*/ ;
 
+  /*
+    This is defined in ansi.h
+    We include it here for reference
+
+    drl 1/4/2002
+  */
+
+  /*@-redef@*/
 typedef /*@concrete@*/ struct 
 {
   int quot;
   int rem;
 } div_t ;
+/*@=redef@*/
+
+
 
 extern div_t div (int num, int denom) /*@*/ ;
 
@@ -55,32 +66,48 @@ char *ecvt(double value, int ndigit, /*@out@*/ int *decpt, /*@out@*/ int *sign)
      /*@modifies fileSystem, errno @*/
      ;
      char *initstate(unsigned int seed, char *state, size_t size)
-     /*@modifies interalState, state @*/ /*@requires maxSet(state) >= (size - 1) @*/ /*drl added 09-20-001*/
+     /*@modifies internalState, state @*/ /*@requires maxSet(state) >= (size - 1) @*/ /*drl added 09-20-001*/
      ;
-     long int jrand48 (unsigned short int xsubi[3]) /*@modifies internalState@*/ /*@requires maxSet(xsubi) >= 2 @*/ ; 
 
+     /*drl 1/4/2002: specifying the array sizes is meaningless but we include
+       them to be consistent with the unix specification at opengroup.org */
+     /*@-fixedformalarray@*/
+     long int jrand48 (unsigned short int xsubi[3]) /*@modifies internalState@*/ /*@requires maxSet(xsubi) >= 2 @*/ ; 
+     
      char *l64a(long value) /*@ensures maxRead(result) <= 5 /\ maxSet(result) <= 5 @*/ ;
      extern long int labs (long int n) /*@*/ ; 
 
+          /*@-fixedformalarray@*/
 extern     void lcong48 (unsigned short int param[7]) /*@modifies internalState@*/ /*@requires maxRead(param) >= 6 @*/ ; 
 
+    /*@=fixedformalarray@*/
+
+  /*
+    This is already defined in ansi.h
+    We include it here for reference but
+    comment it out to avoid a warning
+    drl 1/4/2002
+  */
+
+/*@-redef@*/
 typedef /*@concrete@*/ struct 
 {
   long int quot;
   long int rem;
 } ldiv_t ;
+/*@=redef@*/
 
 extern ldiv_t ldiv (long num, long denom) /*@*/ ;
 
 long int lrand48 (void) /*@modifies internalState@*/ ; 
 
 
-extern /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@modifes errno@*/
+extern /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@modifies errno@*/
      /*drl 09-20-001 added errno*/
      /*@ensures MaxSet(result) == (size - 1); @*/ ;
 
      extern int mblen (char *s, size_t n)
-     /*@modifes errno@*/
+     /*@modifies errno@*/
      /*@requires maxRead(s) >= (n - 1) @*/
      /*drl 09-20-001 added errno*/ ;
 
@@ -104,13 +131,17 @@ extern int mbtowc (/*@null@*/ /*@out@*/ wchar_t *pwc, /*@null@*/ char *s, size_t
 
      long int mrand48 (void) /*@modifies internalState@*/ ;
 
+
+          /*drl 1/4/2002: specifying the array size is meaningless but we include
+       it to be consistent with the unix specification at opengroup.org */
+     /*@-fixedformalarray@*/
  long int nrand48 (unsigned short int xsubi[3]) /*@modifies internalState, xsubi @*/
 
      /*@requires maxSet(xsubi) >= 2 /\ maxRead(xsubi) >= 2 @*/
      ;
+     /*@=fixedformalarray@*/
      
-     extern /*@dependent@*/ /*check dependent */ char *ptsname(int fildes) /*@drl added 09-20-01@*/ ;
-     
+     extern /*@dependent@*/ /*check dependent */ char *ptsname(int fildes) /*drl added 09-20-01*/ ;
 
 	extern int
 	putenv (/*@kept@*/ const char *string)
@@ -139,13 +170,16 @@ extern int rand_r(unsigned int *seed) /*@modifies seed@*/   /*drl 09-20-01 added
    realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size)      /*@modifies *p, errno @*/ /*@ensures MaxSet(result) == (size - 1) @*/;
 
 extern char *realpath(const char *file_name, /*@out@*/ char *resolved_name)
-     //     /*@requires maxSet(resolved_name) >=  (PATH_MAX - 1) @*/
+     //     *@requires maxSet(resolved_name) >=  (PATH_MAX - 1) @*/
      ;
 
+     /*drl 1/4/2002: specifying the array sizes is meaningless but we include
+       them to be consistent with the unix specification at opengroup.org */
+     /*@-fixedformalarray@*/
 unsigned short int *seed48 (unsigned short int seed16v[3]) /*@modifies internalState@*/
      /*@requires maxRead(seed16v) >= 2 @*/
      ; 
-
+     /*@=fixedformalarray@*/
 
      void setkey(const char *key) /*@requires maxRead(key) >= 63 @*/
      /*@modifies internalState, errno@*/ 
@@ -179,11 +213,11 @@ extern long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
   
 
      extern int unlockpt(int fildes)
-     /*@modifes fileSystem, internalState @*/
+     /*@modifies fileSystem, internalState @*/
   /*drl added 09-20-001 */ 
      ;
      
-extern void *valloc(size_t size)/*@modifes errno@*/
+extern void *valloc(size_t size)/*@modifies errno@*/
      /*drl 09-20-001 */
      /*@ensures MaxSet(result) == (size - 1); @*/ 
     /*legacy*/   ;