*** empty log message ***

[splint.git] / lib / stdlib.h

diff --git a/lib/stdlib.h b/lib/stdlib.h
index 3a180f3d8af7e59dd6a91751dd3bf2892b52d4fb..372e93a494a60e88555cdb8b14329f5fb815fbae 100644 (file)
--- a/lib/stdlib.h
+++ b/lib/stdlib.h
@@ -4,9 +4,9 @@
 /*@constant int RAND_MAX; @*/
 /*@constant size_t MB_CUR_MAX; @*/
 
-     div_t Structure type returned by div() function. 
-     ldiv_t
-         Structure type returned by ldiv() function.
+//     div_t Structure type returned by div() function. 
+//   ldiv_t
+//       Structure type returned by ldiv() function.
 
      
      long a64l(const char *s)     ;
@@ -75,12 +75,12 @@ 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*/ ;
 
@@ -139,7 +139,7 @@ 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) @*/
      ;
 
 unsigned short int *seed48 (unsigned short int seed16v[3]) /*@modifies internalState@*/
@@ -157,7 +157,7 @@ unsigned short int *seed48 (unsigned short int seed16v[3]) /*@modifies internalS
      
 extern void srand48 (long int seedval) /*@modifies internalState@*/ ;
 
-ertern void srandom(unsigned int seed) /*@modifies internalState@*/ /*drl added 09-20-001 */
+extern void srandom(unsigned int seed) /*@modifies internalState@*/ /*drl added 09-20-001 */
      ;
 extern double strtod (const char *s, /*@null@*/ /*@out@*/ char **endp)
   /*@modifies *endp, errno@*/ ;
@@ -179,13 +179,13 @@ 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); @*/ ;
+     /*@ensures MaxSet(result) == (size - 1); @*/ 
     /*legacy*/   ;
 
 extern size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n)