imports/stdlib.lcl

   1 /*
   2 ** stdlib.lcl
   3 **
   4 ** based on red-cross:/usr/include/stdlib.h
   5 ** also includes misc functions from man bcopy
   6 **                                   man memory
   7 */
   8
   9 typedef unsigned int    size_t;
  10 typedef unsigned int    wchar_t;
  11
  12 typedef struct {
  13                 int     quot;   /* quotient */
  14                 int     rem;    /* remainder */
  15         }       div_t;          /* result of div() */
  16
  17 typedef struct {
  18                 long    quot;   /* quotient */
  19                 long    rem;    /* remainder */
  20         }       ldiv_t;         /* result of ldiv() */
  21
  22 constant null void *NULL;  /* should be constant */
  23
  24 constant int EXIT_FAILURE, EXIT_SUCCESS;
  25 constant long RAND_MAX;
  26
  27 constant int MB_CUR_MAX;
  28
  29 void abort(void)
  30 {
  31   ensures true;
  32 }
  33
  34 int abs(int i)
  35 {
  36   ensures result = abs(i);
  37 }
  38
  39 int atexit (void (*f)())
  40 {
  41   ensures true;
  42 }
  43
  44 double atof (char *nptr)
  45 {
  46    ensures true ; /* sprintf(result) = nptr^ ? */
  47 }
  48
  49 int atoi (char *nptr)
  50 {
  51    ensures true ;
  52 }
  53
  54 long atol (char *nptr)
  55 {
  56    ensures true ;
  57 }
  58
  59 void *bsearch (void *key, void *base, size_t nel, size_t size,
  60                int (*compar)(void *, void *))
  61 {
  62    ensures true ;
  63 }
  64
  65 void *calloc (size_t nelem, size_t size)
  66 {
  67    ensures true ;
  68 }
  69
  70 div_t div (int numer, int denom)
  71 {
  72    ensures true;
  73 }
  74
  75 void exit(int status)
  76 {
  77    ensures true;
  78 }
  79
  80 void free(void *ptr)
  81 {
  82    modifies *ptr;
  83    ensures true; /* trashed(ptr); */
  84 }
  85
  86 char *getenv (char *name)
  87 {
  88    ensures true;
  89 }
  90
  91 long labs (long j)
  92 {
  93    ensures true;
  94 }
  95
  96 ldiv_t ldiv (long numer, long denum)
  97 {
  98    ensures true;
  99 }
 100
 101 void *malloc (size_t size)
 102 {
 103    ensures true;
 104 }
 105
 106 int mblen (char *s, size_t n)
 107 {
 108    ensures true;
 109 }
 110
 111 size_t mbstowcs ( wchar_t *pwcs, char *s, size_t n)
 112 {
 113    modifies *pwcs;
 114    ensures true;
 115 }
 116
 117 int mbtowc (wchar_t *pwc, char *s, size_t n)
 118 {
 119    modifies *pwc;
 120    ensures true;
 121 }
 122
 123 void qsort (void *base, size_t nel, size_t width,
 124                 int (*compar)(void *, void *))
 125 {
 126    modifies *base;
 127    ensures true;
 128 }
 129
 130 int rand (void)
 131 {
 132    ensures true;
 133 }
 134
 135 void *realloc(void *ptr, size_t size)
 136 {
 137    ensures true;
 138 }
 139
 140 void srand (unsigned int seed)
 141 {
 142    ensures true;
 143 }
 144
 145 double strtod (char *nptr, char **eptr)
 146 {
 147    modifies *eptr;
 148    ensures true;
 149 }
 150
 151 long strtol (char *nptr, char **eptr, int base)
 152 {
 153    modifies *eptr;
 154    ensures true;
 155 }
 156
 157 unsigned long strtoul (char *nptr, char **eptr, int base)
 158 {
 159    modifies *eptr;
 160    ensures true;
 161 }
 162
 163 int system (char *string)
 164 {
 165    ensures true;
 166 }
 167
 168 size_t wcstombs (char *s, wchar_t *pwcs, size_t n)
 169 {
 170    modifies *s;
 171    ensures true;
 172 }
 173
 174 int wctomb (char *s, wchar_t wchar)
 175 {
 176    modifies *s;
 177    ensures true;
 178 }
 179
 180 /*
 181 ** not part of stdlib.h, but built in to c?
 182 */
 183
 184 void bcopy (char *b1, char *b2, int length)
 185 {
 186    modifies *b2;
 187    ensures true;
 188 }
 189
 190 | bool : int | bcmp (char *b1, char *b2, int length)
 191 {
 192    ensures true;
 193 }
 194
 195 void bzero (char *b1, int length)
 196 {
 197    modifies *b1;
 198    ensures true;
 199 }
 200
 201 int ffs (int i)
 202 {
 203    ensures true;
 204 }
 205
 206 void *memccpy (void *s1, void *s2, int c, size_t n)
 207 {
 208    modifies *s1;
 209    ensures true;
 210 }
 211
 212 void *memchr (void *s, int c, size_t n)
 213 {
 214    ensures true;
 215 }
 216
 217 | bool : int | memcmp (void *s1, void *s2, size_t n)
 218 {
 219    ensures true;
 220 }
 221
 222 void *memcpy (void *s1, void *s2, size_t n)
 223 {
 224    modifies *s1;
 225    ensures true;
 226 }
 227
 228 void *memset (void *s, int c, size_t n)
 229 {
 230    modifies *s;
 231    ensures true;
 232 }
 233
 234 void *memmove (void *s1, void *s2, size_t n)
 235 {
 236    modifies *s1;
 237    ensures true;
 238 }
 239
 240
 241
 242
 243
 244
 245
 246