/*
** stdlib.lcl
**
** based on red-cross:/usr/include/stdlib.h
** also includes misc functions from man bcopy
**                                   man memory
*/

typedef	unsigned int	size_t;	
typedef	unsigned int	wchar_t;

typedef struct {
		int	quot;	/* quotient */
		int	rem;	/* remainder */
	}	div_t;		/* result of div() */

typedef struct {
		long	quot;	/* quotient */
		long	rem;	/* remainder */
	}	ldiv_t;		/* result of ldiv() */

constant null void *NULL;  /* should be constant */

constant int EXIT_FAILURE, EXIT_SUCCESS;
constant long RAND_MAX;

constant int MB_CUR_MAX;

void abort(void)
{
  ensures true;
}

int abs(int i)
{
  ensures result = abs(i);
}

int atexit (void (*f)())
{
  ensures true;
}

double atof (char *nptr)
{
   ensures true ; /* sprintf(result) = nptr^ ? */
}

int atoi (char *nptr)
{
   ensures true ;
}

long atol (char *nptr)
{
   ensures true ;
}

void *bsearch (void *key, void *base, size_t nel, size_t size,
	       int (*compar)(void *, void *))
{
   ensures true ;
}

void *calloc (size_t nelem, size_t size)
{
   ensures true ;
}

div_t div (int numer, int denom)
{
   ensures true;
}

void exit(int status)
{
   ensures true;
}

void free(void *ptr)
{
   modifies *ptr;
   ensures true; /* trashed(ptr); */
}

char *getenv (char *name)
{
   ensures true;
}

long labs (long j)
{
   ensures true;
}

ldiv_t ldiv (long numer, long denum)
{
   ensures true;
}

void *malloc (size_t size)
{
   ensures true;
}

int mblen (char *s, size_t n)
{
   ensures true;
}

size_t mbstowcs ( wchar_t *pwcs, char *s, size_t n)
{
   modifies *pwcs;
   ensures true;
}

int mbtowc (wchar_t *pwc, char *s, size_t n)
{
   modifies *pwc;
   ensures true;
}

void qsort (void *base, size_t nel, size_t width,
	 	int (*compar)(void *, void *))
{
   modifies *base;
   ensures true;
}

int rand (void)
{
   ensures true;
}

void *realloc(void *ptr, size_t size)
{
   ensures true;
}

void srand (unsigned int seed)
{
   ensures true;
}

double strtod (char *nptr, char **eptr)
{
   modifies *eptr;
   ensures true;
}

long strtol (char *nptr, char **eptr, int base)
{
   modifies *eptr;
   ensures true;
}

unsigned long strtoul (char *nptr, char **eptr, int base)
{
   modifies *eptr;
   ensures true;
}

int system (char *string)
{
   ensures true;
}

size_t wcstombs (char *s, wchar_t *pwcs, size_t n)
{
   modifies *s;
   ensures true;
}

int wctomb (char *s, wchar_t wchar)
{
   modifies *s;
   ensures true;
}

/*
** not part of stdlib.h, but built in to c?
*/

void bcopy (char *b1, char *b2, int length)
{
   modifies *b2;
   ensures true;
}

| bool : int | bcmp (char *b1, char *b2, int length)
{
   ensures true;
}

void bzero (char *b1, int length)
{
   modifies *b1;
   ensures true;
}

int ffs (int i)
{
   ensures true;
}

void *memccpy (void *s1, void *s2, int c, size_t n)
{
   modifies *s1;
   ensures true;
}

void *memchr (void *s, int c, size_t n)
{
   ensures true;
}

| bool : int | memcmp (void *s1, void *s2, size_t n)
{
   ensures true;
}

void *memcpy (void *s1, void *s2, size_t n)
{
   modifies *s1;
   ensures true;
}

void *memset (void *s, int c, size_t n)
{
   modifies *s;
   ensures true;
}

void *memmove (void *s1, void *s2, size_t n)
{
   modifies *s1;
   ensures true;
}