lib/stdlib.h

   1 /*@constant int EXIT_FAILURE; @*/
   2 /*@constant int EXIT_SUCCESS; @*/
   3 /*@constant null anytype NULL = 0;@*/
   4 /*@constant int RAND_MAX; @*/
   5 /*@constant size_t MB_CUR_MAX; @*/
   6
   7 //     div_t Structure type returned by div() function.
   8 //   ldiv_t
   9 //       Structure type returned by ldiv() function.
  10
  11
  12      long a64l(const char *s)     ;
  13
  14 /*@exits@*/ void abort (void) /*@*/ ;
  15 extern int abs (int n) /*@*/ ;
  16 int atexit(void (*func)(void));
  17
  18 extern double atof (char *s) /*@*/ ;
  19 extern int atoi (char *s) /*@*/ ;
  20 extern long int atol (char *s) /*@*/ ;
  21
  22 void * bsearch (const void *key, const void *base, size_t nel, size_t size,
  23 int (*compar)(const void *, const void *)) /*@*/
  24      /*@requires maxSet(base) >= (nel - 1) @*/
  25      ;
  26
  27 extern /*@null@*/ /*@out@*/ /*@only@*/ void *calloc (size_t nobj, size_t size)
  28   /*@modifies errno@*/
  29   /*@ensures MaxSet(result) == (nobj - 1); @*/ ;
  30
  31   /*
  32     This is defined in ansi.h
  33     We include it here for reference
  34
  35     drl 1/4/2002
  36   */
  37
  38   /*@-redef@*/
  39 typedef /*@concrete@*/ struct
  40 {
  41   int quot;
  42   int rem;
  43 } div_t ;
  44 /*@=redef@*/
  45
  46
  47
  48 extern div_t div (int num, int denom) /*@*/ ;
  49
  50   double drand48 (void) /*@modifies internalState@*/ ;
  51
  52
  53 char *ecvt(double value, int ndigit, /*@out@*/ int *decpt, /*@out@*/ int *sign)
  54      ;
  55
  56      char *fcvt(double value, int ndigit, /*@out@*/ int *decpt,  /*@out@*/int *sign);
  57
  58      char *gcvt(double value, int ndigit, char *buf)
  59      /*@requires maxSet(buf) >= ndigit @*/
  60      ;
  61
  62      extern /*@observer@*/ /*@null@*/ char *getenv (const char *name) /*@*/ ;
  63
  64      extern  int getsubopt(char **optionp, char * const *tokens, /*@out@*/ char **valuep)
  65      /*@modifies optionp, valuep @*/ ;
  66
  67      extern  int grantpt(int fildes)
  68      /*@modifies fileSystem, errno @*/
  69      ;
  70      char *initstate(unsigned int seed, char *state, size_t size)
  71      /*@modifies internalState, state @*/ /*@requires maxSet(state) >= (size - 1) @*/ /*drl added 09-20-001*/
  72      ;
  73
  74      /*drl 1/4/2002: specifying the array sizes is meaningless but we include
  75        them to be consistent with the unix specification at opengroup.org */
  76      /*@-fixedformalarray@*/
  77      long int jrand48 (unsigned short int xsubi[3]) /*@modifies internalState@*/ /*@requires maxSet(xsubi) >= 2 @*/ ;
  78
  79      char *l64a(long value) /*@ensures maxRead(result) <= 5 /\ maxSet(result) <= 5 @*/ ;
  80      extern long int labs (long int n) /*@*/ ;
  81
  82           /*@-fixedformalarray@*/
  83 extern     void lcong48 (unsigned short int param[7]) /*@modifies internalState@*/ /*@requires maxRead(param) >= 6 @*/ ;
  84
  85     /*@=fixedformalarray@*/
  86
  87   /*
  88     This is already defined in ansi.h
  89     We include it here for reference but
  90     comment it out to avoid a warning
  91     drl 1/4/2002
  92   */
  93
  94 /*@-redef@*/
  95 typedef /*@concrete@*/ struct
  96 {
  97   long int quot;
  98   long int rem;
  99 } ldiv_t ;
 100 /*@=redef@*/
 101
 102 extern ldiv_t ldiv (long num, long denom) /*@*/ ;
 103
 104 long int lrand48 (void) /*@modifies internalState@*/ ;
 105
 106
 107 extern /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size)
 108   /*@modifies errno@*/
 109   /*@ensures MaxSet(result) == (size - 1); @*/ ;
 110
 111      extern int mblen (char *s, size_t n)
 112      /*@modifies errno@*/
 113      /*@requires maxRead(s) >= (n - 1) @*/
 114      /*drl 09-20-001 added errno*/ ;
 115
 116      size_t mbstowcs(/*@null@*/ /*@out@*/ wchar_t *pwcs, const char *s, size_t n)
 117   /*@requires maxSet(pwcs) >= (n - 1) @*/
 118      /*drl 09-20-001 added errno*/ ;
 119
 120 extern int mbtowc (/*@null@*/ /*@out@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n)
 121      /*@modifies *pwc, errno@*/   /*@requires maxRead(s) >= (n - 1) @*/ /*drl 09-20-001 added errno*/;
 122
 123
 124      extern char *mktemp(char *template) /*@modifies template @*/
 125      /*drl added 09-20-001*/ /*warn use  mkstemp */
 126      ;
 127
 128      int mkstemp(char *template)
 129      /*@modifies template, fileSystem @*/
 130
 131      /*drl added 09-20-001*/
 132      ;
 133
 134      long int mrand48 (void) /*@modifies internalState@*/ ;
 135
 136
 137           /*drl 1/4/2002: specifying the array size is meaningless but we include
 138        it to be consistent with the unix specification at opengroup.org */
 139      /*@-fixedformalarray@*/
 140  long int nrand48 (unsigned short int xsubi[3]) /*@modifies internalState, xsubi @*/
 141
 142      /*@requires maxSet(xsubi) >= 2 /\ maxRead(xsubi) >= 2 @*/
 143      ;
 144      /*@=fixedformalarray@*/
 145
 146      extern /*@dependent@*/ /*check dependent */ char *ptsname(int fildes) /*drl added 09-20-01*/ ;
 147
 148         extern int
 149         putenv (/*@kept@*/ const char *string)
 150         /*@globals environ@*/
 151         /*@modifies *environ, errno@*/
 152      /*drl 09-20-01 added kept */
 153      ;
 154
 155      extern void qsort (void *base, size_t nel, size_t size,
 156                         int (*compar)(const void *, const void *) )
 157      /*@requires maxRead(base) >= (nel - 1) @*/
 158   /*@modifies *base, errno@*/ ;
 159
 160
 161
 162 /*@constant int RAND_MAX; @*/
 163 extern int rand (void) /*@modifies internalState@*/ ;
 164
 165 extern int rand_r(unsigned int *seed) /*@modifies seed@*/   /*drl 09-20-01 added*/
 166      ;
 167
 168
 169      long random(void)  /*@modifies internalState@*/ ;
 170
 171  extern /*@null@*/ /*@only@*/ void *
 172    realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size)      /*@modifies *p, errno @*/ /*@ensures MaxSet(result) == (size - 1) @*/;
 173
 174 extern char *realpath(const char *file_name, /*@out@*/ char *resolved_name)
 175      //     *@requires maxSet(resolved_name) >=  (PATH_MAX - 1) @*/
 176      ;
 177
 178      /*drl 1/4/2002: specifying the array sizes is meaningless but we include
 179        them to be consistent with the unix specification at opengroup.org */
 180      /*@-fixedformalarray@*/
 181 unsigned short int *seed48 (unsigned short int seed16v[3]) /*@modifies internalState@*/
 182      /*@requires maxRead(seed16v) >= 2 @*/
 183      ;
 184      /*@=fixedformalarray@*/
 185
 186      void setkey(const char *key) /*@requires maxRead(key) >= 63 @*/
 187      /*@modifies internalState, errno@*/
 188      ;
 189
 190      /*@only@*/ char *setstate(/*@kept@*/ const char *state)  /*@modifies internalState, errno@*/ ;
 191
 192      extern void srand (unsigned int seed) /*@modifies internalState@*/ ;
 193
 194 extern void srand48 (long int seedval) /*@modifies internalState@*/ ;
 195
 196 extern void srandom(unsigned int seed) /*@modifies internalState@*/ /*drl added 09-20-001 */
 197      ;
 198 extern double strtod (const char *s, /*@null@*/ /*@out@*/ char **endp)
 199   /*@modifies *endp, errno@*/ ;
 200
 201 extern long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
 202   /*@modifies *endp, errno@*/ ;
 203
 204   extern unsigned long
 205   strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
 206   /*@modifies *endp, errno@*/ ;
 207
 208
 209   extern int system (/*@null@*/ const char *s) /*@modifies fileSystem, errno@*/
 210   /*drl 09-20-01 added errno */
 211      ;
 212
 213      extern int ttyslot(void) /*@*/
 214      /*drl added 09-20-001 */ /*legacy*/  ;
 215
 216
 217      extern int unlockpt(int fildes)
 218      /*@modifies fileSystem, internalState @*/
 219   /*drl added 09-20-001 */
 220      ;
 221
 222 extern void *valloc(size_t size)/*@modifies errno@*/
 223      /*drl 09-20-001 */
 224      /*@ensures MaxSet(result) == (size - 1); @*/
 225     /*legacy*/   ;
 226
 227 extern size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n)
 228      /*@modifies *s, errno@*/ /*@requires maxSet(s) >= (n - 1) @*/ ;
 229
 230 extern int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar)
 231    /*@modifies *s@*/ ;
 232