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