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