Committing my cosmetic code changes and fix of the token problem in

[splint.git] / lib / ansi.h

/*
** satndard.h --- ISO C99 Standard Library for Splint.
**
** Process with -DSTRICT to get strict library.
*/

/*@-nextlinemacros@*/
/*@+allimponly@*/
/*@+globsimpmodifiesnothing@*/

/*
** errno.h
*/

/*@constant int EDOM;@*/
/*@constant int ERANGE;@*/
/*@constant int EILSEQ;@*/

# ifdef STRICT
/*@checkedstrict@*/ int errno;
# else 
/*@unchecked@*/ int errno;
# endif

/*
** types 
*/

typedef /*@integraltype@*/ ptrdiff_t;    
typedef /*@unsignedintegraltype@*/ size_t;
typedef /*@signedintegraltype@*/ ssize_t;
typedef /*@integraltype@*/ wchar_t;

/*
** Added by Amendment 1 to ISO.
*/

typedef /*@integraltype@*/ wint_t;
typedef /*@abstract@*/ mbstate_t;

/*@constant null anytype NULL = 0;@*/

/*
** assert.h
*/

/*@constant lltX_bool NDEBUG;@*/

# ifdef STRICT
/*@falseexit@*/ void assert (/*@sef@*/ lltX_bool e) 
  /*@*/ ;
# else
/*@falseexit@*/ void assert (/*@sef@*/ lltX_bool /*@alt int@*/ e) 
  /*@*/ ;
# endif


/*
** ctype.h
*/

# ifdef STRICT
lltX_bool isalnum (int c) /*@*/ ;
lltX_bool isalpha (int c) /*@*/ ;
lltX_bool iscntrl (int c) /*@*/ ;
lltX_bool isdigit (int c) /*@*/ ;
lltX_bool isgraph (int c) /*@*/ ;
lltX_bool islower (int c) /*@*/ ;
lltX_bool isprint (int c) /*@*/ ;
lltX_bool ispunct (int c) /*@*/ ;
lltX_bool isspace (int c) /*@*/ ;
lltX_bool isupper (int c) /*@*/ ;
lltX_bool isxdigit (int c) /*@*/ ;
char tolower (int c) /*@*/ ;
char toupper (int c) /*@*/ ;
# else
/*
** evans 2002-01-03: added alt char (was alt unsigned char)
*/

lltX_bool /*@alt int@*/ isalnum (int /*@alt char, unsigned char@*/ c) /*@*/ ;
lltX_bool /*@alt int@*/ isalpha (int /*@alt char, unsigned char@*/ c) /*@*/ ;
lltX_bool /*@alt int@*/ iscntrl (int /*@alt char, unsigned char@*/ c) /*@*/ ;
lltX_bool /*@alt int@*/ isdigit (int /*@alt char, unsigned char@*/ c) /*@*/ ;
lltX_bool /*@alt int@*/ isgraph (int /*@alt char, unsigned char@*/ c) /*@*/ ;
lltX_bool /*@alt int@*/ islower (int /*@alt char, unsigned char@*/ c) /*@*/ ;
lltX_bool /*@alt int@*/ isprint (int /*@alt char, unsigned char@*/ c) /*@*/ ;
lltX_bool /*@alt int@*/ ispunct (int /*@alt char, unsigned char@*/ c) /*@*/ ;
lltX_bool /*@alt int@*/ isspace (int /*@alt char, unsigned char@*/ c) /*@*/ ;
lltX_bool /*@alt int@*/ isupper (int /*@alt char, unsigned char@*/ c) /*@*/ ;
lltX_bool /*@alt int@*/ isxdigit (int /*@alt char, unsigned char@*/ c) /*@*/ ;
char /*@alt int@*/ tolower (int /*@alt char, unsigned char@*/ c) /*@*/ ;
char /*@alt int@*/ toupper (int /*@alt char, unsigned char@*/ c) /*@*/ ;
# endif

/*
** locale.h
*/

struct lconv
{
  char *decimal_point;
  char *thousands_sep;
  char *grouping;
  char *int_curr_symbol;
  char *currency_symbol;
  char *mon_decimal_point;
  char *mon_thousands_sep;
  char *mon_grouping;
  char *positive_sign;
  char *negative_sign;
  char int_frac_digits;
  char frac_digits;
  char p_cs_precedes;
  char p_sep_by_space;
  char n_cs_precedes;
  char n_sep_by_space;
  char p_sign_posn;
  char n_sign_posn;
} ;

/*@constant int LC_ALL;@*/
/*@constant int LC_COLLATE;@*/
/*@constant int LC_CTYPE;@*/
/*@constant int LC_MONETARY;@*/
/*@constant int LC_NUMERIC;@*/
/*@constant int LC_TIME;@*/

/*@observer@*/ /*@null@*/ char *setlocale (int category, /*@null@*/ char *locale) 
   /*@modifies internalState, errno@*/ ;

struct lconv *localeconv (void) /*@*/ ;

/*
** float.h
*/

/*
** Note, these are defined by macros, but NOT necessarily
** constants.  They may be used as lvalues.
*/

/*@unchecked@*/ int    DBL_DIG;
/*@unchecked@*/ double DBL_EPSILON;
/*@unchecked@*/ int    DBL_MANT_DIG;
/*@unchecked@*/ double DBL_MAX;
/*@unchecked@*/ int    DBL_MAX_10_EXP;
/*@unchecked@*/ int    DBL_MAX_EXP;
/*@unchecked@*/ double DBL_MIN;
/*@unchecked@*/ int    DBL_MIN_10_EXP;
/*@unchecked@*/ int    DBL_MIN_EXP;

/*@unchecked@*/ int   FLT_DIG;
/*@unchecked@*/ float FLT_EPSILON;
/*@unchecked@*/ int   FLT_MANT_DIG;
/*@unchecked@*/ float FLT_MAX;
/*@unchecked@*/ int   FLT_MAX_10_EXP;
/*@unchecked@*/ int   FLT_MAX_EXP;
/*@unchecked@*/ float FLT_MIN;
/*@unchecked@*/ int   FLT_MIN_10_EXP;
/*@unchecked@*/ int   FLT_MIN_EXP;
/*@constant            int   FLT_RADIX@*/
/*@unchecked@*/ int   FLT_ROUNDS;

/*@unchecked@*/ int         LDBL_DIG;
/*@unchecked@*/ long double LDBL_EPSILON;
/*@unchecked@*/ int         LDBL_MANT_DIG;
/*@unchecked@*/ long double LDBL_MAX;
/*@unchecked@*/ int         LDBL_MAX_10_EXP;
/*@unchecked@*/ int         LDBL_MAX_EXP;
/*@unchecked@*/ long double LDBL_MIN;
/*@unchecked@*/ int         LDBL_MIN_10_EXP;
/*@unchecked@*/ int         LDBL_MIN_EXP;

/*
** limits.h
*/

/*@constant int CHAR_BIT; @*/
/*@constant char CHAR_MAX; @*/
/*@constant char CHAR_MIN; @*/
/*@constant int INT_MAX; @*/
/*@constant int INT_MIN; @*/
/*@constant long int LONG_MAX; @*/
/*@constant long int LONG_MIN; @*/
/*@constant long int MB_LEN_MAX@*/
/*@constant signed char SCHAR_MAX; @*/
/*@constant signed char SCHAR_MIN; @*/
/*@constant short SHRT_MAX; @*/
/*@constant short SHRT_MIN; @*/
/*@constant unsigned char UCHAR_MAX; @*/
/*@constant unsigned char UCHAR_MIN; @*/
/*@constant unsigned int UINT_MAX; @*/
/*@constant unsigned long ULONG_MAX; @*/
/*@constant unsigned short USHRT_MAX; @*/

/*
** math.h
*/

/*@constant double HUGE_VAL; @*/

/*
** math functions that may have a range error modify errno 
*/

double sin (double x) /*@*/ ;
double cos (double x) /*@*/ ;
double tan (double x) /*@*/ ;
double asin (double x) /*@modifies errno@*/ ;
double acos (double x) /*@modifies errno@*/ ;
double atan (double x) /*@*/ ;
double atan2 (double y, double x) /*@*/ ;
double sinh (double x) /*@*/ ;
double cosh (double x) /*@modifies errno@*/ ;
double tanh (double x) /*@*/ ;

double exp (double x) /*@modifies errno@*/ ;
double ldexp (double x, int n) /*@modifies errno@*/ ;
double frexp (double x, /*@out@*/ int *xp) /*@modifies *xp;@*/ ;

double log (double x) /*@modifies errno@*/ ;
double log10 (double x) /*@modifies errno@*/ ;

double pow (double x, double y) /*@modifies errno@*/ ;
double sqrt (double x) /*@modifies errno@*/ ;

double ceil (double x) /*@*/ ;
double floor (double x) /*@*/ ;
double fabs (double x) /*@*/ ;

double modf (double x, /*@out@*/ double *ip) /*@modifies *ip;@*/ ;
double fmod (double x, double y) /*@*/ ;

/*
** These functions are optional in iso C.  An implementation does not
** have to provide them.  They are included in comments here, but
** are not required to be part of the standard library.
*/

# ifdef OPTIONAL_MATH

float acosf (float x) /*@modifies errno@*/ ;
long double acosl (long double x) /*@modifies errno@*/ ;
float asinf (float x)	/*@modifies errno@*/ ;
long double asinl (long double x) /*@modifies errno@*/ ;
float atanf (float x)	/*@*/ ;
long double atanl (long double x) /*@*/ ;
float atan2f (float y, float x) /*@*/ ;
long double atan2l (long double y, long double x) /*@*/ ;
float ceilf (float x)	/*@*/ ;
long double ceill (long double x) /*@*/ ;
float cosf (float x) /*@*/ ;
long double cosl (long double x) /*@*/ ;
float coshf (float x)	/*@modifies errno@*/ ;
long double coshl (long double x) /*@modifies errno@*/ ;
float expf (float x) /*@modifies errno@*/ ;
long double expl (long double x) /*@modifies errno@*/;
float fabsf (float x)	/*@*/ ;
long double fabsl (long double x) /*@*/ ;
float floorf (float x) /*@*/ ;
long double floorl (long double x) /*@*/ ;
float fmodf (float x, float y) /*@*/ ;
long double fmodl (long double x, long double y)	/*@*/ ;
float frexpf (float x, /*@out@*/ int *xp) /*@modifies *xp@*/;
long double frexpl (long double x, /*@out@*/ int *xp) /*@modifies *xp@*/;
float ldexpf (float x, int n) /*@modifies errno@*/ ;
long double ldexpl (long double x, int n) /*@modifies errno@*/ ;
float logf (float x) /*@modifies errno@*/ ;
long double logl (long double x) /*@modifies errno@*/ ;
float log10f (float x) /*@modifies errno@*/;
long double log10l (long double x) /*@modifies errno@*/;
float modff (float x, /*@out@*/ float *xp) /*@modifies *xp@*/ ;
long double modfl (long double x, /*@out@*/ long double *xp) /*@modifies *xp@*/ ;
float powf (float x, float y) /*@modifies errno@*/ ;
long double powl (long double x, long double y) /*@modifies errno@*/ ;
float sinf (float x) /*@*/ ;
long double sinl (long double x)	/*@*/ ;
float sinhf (float x) /*@*/ ;
long double sinhl (long double x) /*@*/ ;
float sqrtf (float x) /*@modifies errno@*/ ;
long double sqrtl (long double x) /*@modifies errno@*/ ;
float tanf (float x) /*@*/ ;
long double tanl (long double x)	/*@*/ ;
float tanhf (float x) /*@*/ ;
long double tanhl (long double x) /*@*/ ;

# endif

/*
** setjmp.h
*/

typedef /*@abstract@*/ /*@mutable@*/ void *jmp_buf;

int setjmp (/*@out@*/ jmp_buf env) /*@modifies env;@*/ ;
/*@mayexit@*/ void longjmp (jmp_buf env, int val) /*@*/ ;

/*
** signal.h
*/

/*@constant int SIGABRT; @*/
/*@constant int SIGFPE; @*/
/*@constant int SIGILL; @*/
/*@constant int SIGINT; @*/
/*@constant int SIGSEGV; @*/
/*@constant int SIGTERM; @*/

typedef /*@integraltype@*/ sig_atomic_t;

/*@constant void (*SIG_DFL)(int); @*/
/*@constant void (*SIG_ERR)(int); @*/
/*@constant void (*SIG_IGN)(int); @*/

/*
** signal takes an int, and a function takes int returns void, and
** returns the function (or NULL if unsuccessful).
*/

/*@null@*/ void (*signal (int sig, /*@null@*/ void (*func)(int))) (int) 
   /*@modifies internalState, errno;@*/ ;

/*@mayexit@*/ int raise (int sig) ;

/*
** stdarg.h
*/

typedef /*@abstract@*/ /*@mutable@*/ void *va_list;

void va_start (/*@out@*/ va_list ap, ...) /*@modifies ap;@*/ ;
void va_end (va_list va) /*@modifies va;@*/ ;

/*
** va_arg is builtin
*/

/*
** stdio.h
*/

typedef /*@abstract@*/ /*@mutable@*/ void *FILE;
typedef /*@abstract@*/ /*@mutable@*/ void *fpos_t;

/*@constant int _IOFBF; @*/
/*@constant int _IOLBF; @*/
/*@constant int _IONBF; @*/

/*@constant int BUFSIZ; @*/
/*@constant int EOF; @*/

/*@constant int FOPEN_MAX; @*/
/*@constant int FILENAME_MAX; @*/

/*@constant int L_tmpnam; @*/

/*@constant int SEEK_CUR; @*/
/*@constant int SEEK_END; @*/
/*@constant int SEEK_SET; @*/

/*@constant int TMP_MAX; @*/

# ifdef STRICT
/*@checked@*/ FILE *stderr;
/*@checked@*/ FILE *stdin;
/*@checked@*/ FILE *stdout;
# else
/*@unchecked@*/ FILE *stderr;
/*@unchecked@*/ FILE *stdin;
/*@unchecked@*/ FILE *stdout;
# endif

int remove (char *filename) /*@modifies fileSystem, errno@*/ ;
int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ;

/*@null@*/ FILE *tmpfile (void) /*@modifies fileSystem@*/ ;
/*@observer@*/ char *
  tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s) 
  /*@modifies *s, internalState@*/ ;

int fclose (FILE *stream) /*@modifies *stream, errno, fileSystem;@*/ ;
int fflush (/*@null@*/ FILE *stream) 
   /*@modifies *stream, errno, fileSystem;@*/ ;

/*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode) 
   /*@modifies fileSystem@*/ ;         

/*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream) 
  /*@modifies *stream, fileSystem, errno@*/ ;

  extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf) 
   /*@modifies fileSystem, *stream, *buf@*/ ;

   extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf, 
		    int mode, size_t size)
   /*@modifies fileSystem, *stream, *buf@*/ ;

# ifdef STRICT
/*@printflike@*/ 
int fprintf (FILE *stream, char *format, ...)
   /*@modifies fileSystem, *stream@*/ ;
# else
/*@printflike@*/ 
int /*@alt void@*/ fprintf (FILE *stream, char *format, ...)
   /*@modifies fileSystem, *stream@*/ ;
# endif

/*@scanflike@*/ 
int fscanf (FILE *stream, char *format, ...)
   /*@modifies fileSystem, *stream@*/ ;

# ifdef STRICT
/*@printflike@*/ 
int printf (char *format, ...) 
   /*@globals stdout@*/
   /*@modifies fileSystem, *stdout@*/ ;
# else
/*@printflike@*/ 
int /*@alt void@*/ printf (char *format, ...) 
   /*@globals stdout@*/
   /*@modifies fileSystem, *stdout@*/ ;
# endif

/*@scanflike@*/
int scanf(char *format, ...)
   /*@globals stdin@*/
   /*@modifies fileSystem, *stdin@*/ ;

# ifdef STRICT
/*@printflike@*/ 
int sprintf (/*@out@*/ char *s, char *format, ...) 
   /*@modifies *s@*/ ;
# else
/*@printflike@*/ 
int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...) 
   /*@modifies *s@*/ ;
# endif

/*@scanflike@*/ 
int sscanf (/*@out@*/ char *s, char *format, ...) /*@*/ ;
   /* modifies extra arguments */

int vprintf (const char *format, va_list arg)
   /*@globals stdout@*/
   /*@modifies fileSystem, *stdout@*/ ;

int vfprintf (FILE *stream, char *format, va_list arg)
   /*@modifies fileSystem, *stream, arg, errno@*/ ;

int vsprintf (/*@out@*/ char *str, const char *format, va_list ap)
     /*@warn bufferoverflowhigh "Use vsnprintf instead"@*/
     /*@modifies str@*/ ;

int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap)
     /*@requires maxSet(str) >= size@*/
     /*@modifies str@*/ ;

int fgetc (FILE *stream) 
   /*@modifies fileSystem, *stream, errno@*/ ;

/*@null@*/ char *
  fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream)
     /*@modifies fileSystem, *s, *stream, errno@*/
     /*@requires maxSet(s) >= (n -1); @*/
     /*@ensures maxRead(s) <= (n -1) /\ maxRead(s) >= 0; @*/
     ;

int fputc (int /*@alt char@*/ c, FILE *stream)
  /*:errorcode EOF:*/
  /*@modifies fileSystem, *stream, errno@*/ ;

int fputs (char *s, FILE *stream)
  /*@modifies fileSystem, *stream@*/ ;

/* note use of sef --- stream may be evaluated more than once */
int getc (/*@sef@*/ FILE *stream)
  /*@modifies fileSystem, *stream@*/ ;

int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/ ;

/*@null@*/ char *gets (/*@out@*/ char *s) 
   /*@warn bufferoverflowhigh
           "Use of gets leads to a buffer overflow vulnerability.  Use fgets instead"@*/
   /*@globals stdin@*/ /*@modifies fileSystem, *s, *stdin, errno@*/ ;

int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
   /*:errorcode EOF:*/
   /*@modifies fileSystem, *stream;@*/ ;

int putchar (int /*@alt char@*/ c)
   /*:errorcode EOF:*/
   /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ; 

int puts (const char *s)
   /*:errorcode EOF:*/
   /*@globals stdout@*/
   /*@modifies fileSystem, *stdout@*/ ; 

int ungetc (int /*@alt char@*/ c, FILE *stream)
  /*@modifies fileSystem, *stream, errno@*/ ;

size_t 
  fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream)
  /*@modifies fileSystem, *ptr, *stream, errno@*/ ;

size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream)
  /*@modifies fileSystem, *stream, errno@*/ ;

int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos)
  /*@modifies *pos, errno@*/ ;

int fseek (FILE *stream, long int offset, int whence)
   /*:errorcode -1:*/
   /*@modifies fileSystem, *stream, errno@*/ ;

int fsetpos (FILE *stream, fpos_t *pos)
   /*@modifies fileSystem, *stream, errno@*/ ;

long int ftell(FILE *stream) 
   /*:errorcode -1:*/ /*@modifies errno*/ ;

void rewind (FILE *stream) /*@modifies *stream@*/ ;
void clearerr (FILE *stream) /*@modifies *stream@*/ ;

int feof (FILE *stream) /*@modifies errno@*/ ;
int ferror (FILE *stream) /*@modifies errno@*/ ;

void perror (/*@null@*/ char *s) 
   /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ; 

/*
** stdlib.h
*/

double atof (char *s) /*@*/ ;
int atoi (char *s) /*@*/ ;
long int atol (char *s) /*@*/ ;

double strtod (char *s, /*@null@*/ /*@out@*/ char **endp)
  /*@modifies *endp, errno@*/ ;

long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
  /*@modifies *endp, errno@*/ ;

unsigned long 
  strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
  /*@modifies *endp, errno@*/ ;

/*@constant int RAND_MAX; @*/
int rand (void) /*@modifies internalState@*/ ;
void srand (unsigned int seed) /*@modifies internalState@*/ ;

/*
  drl
  changed 12/29/2000
*/

/*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/
     /*@ensures maxSet(result) == (nobj - 1); @*/ ;
/*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@*/
     /*@ensures maxSet(result) == (size - 1); @*/ ;

/*end drl changed */
     
/* 11 June 1997: removed out on return value */

# if 0
/*@null@*/ /*@only@*/ void *
   realloc (/*@null@*/ /*@only@*/ /*@special@*/ void *p, 
	    size_t size) /*@releases p@*/ /*@modifies *p@*/
     /*@ensures maxSet(result) == (size - 1) @*/;
# endif

/*
** LCLint annotations cannot fully describe realloc.  The semantics we
** want are:
**    realloc returns null: ownership of parameter is not changed
**    realloc returns non-null: ownership of parameter is transferred to return value
**
** Otherwise, storage is in the same state before and after the call.
*/

/*@null@*/ /*@only@*/ void *
   realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size) 
     /*@modifies *p@*/ /*@ensures maxSet(result) >= (size - 1) @*/;

void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies p@*/ ;

/*@constant int EXIT_FAILURE; @*/ 
/*@constant int EXIT_SUCCESS; @*/ 

/*@exits@*/ void abort (void) /*@*/ ;
/*@exits@*/ void exit (int status) /*@*/ ;
int atexit (void (*func)(void)) /*@modifies internalState@*/ ;

/*@observer@*/ /*@null@*/ char *getenv (char *name) /*@*/ ;

int system (/*@null@*/ char *s) /*@modifies fileSystem@*/ ;

/*@null@*/ /*@dependent@*/ void *
  bsearch (void *key, void *base, 
	   size_t n, size_t size, 
	   int (*compar)(void *, void *)) /*@*/ ;

void qsort (void *base, size_t n, size_t size, 
		   int (*compar)(void *, void *))
   /*@modifies *base, errno@*/ ;

int abs (int n) /*@*/ ;

typedef /*@concrete@*/ struct 
{
  int quot;
  int rem;
} div_t ;

div_t div (int num, int denom) /*@*/ ;

long int labs (long int n) /*@*/ ; 

typedef /*@concrete@*/ struct 
{
  long int quot;
  long int rem;
} ldiv_t ;

ldiv_t ldiv (long num, long denom) /*@*/ ;

/*@constant size_t MB_CUR_MAX; @*/

/*
** wchar_t and wint_t functions added by Amendment 1 to ISO.
*/

/*@constant int WCHAR_MAX@*/
/*@constant int WCHAR_MIN@*/
/*@constant wint_t WEOF@*/

wint_t btowc (int c) /*@*/ ;

wint_t fgetwc (FILE *fp)	/*@modifies fileSystem, *fp*/ ;

/*@null@*/ wchar_t *fgetws (/*@returned@*/ wchar_t *s, int n, FILE *stream)
   /*@modifies fileSystem, *s, *stream@*/;

wint_t fputwc (wchar_t c, FILE *stream)
   /*@modifies fileSystem, *stream@*/;

int fputws (const wchar_t *s, FILE *stream)
   /*@modifies fileSystem, *stream@*/ ;

int fwide (FILE *stream, int mode) /*@*/ ; 
   /* does not modify the stream */

/*@printflike@*/ int fwprintf (FILE *stream, const wchar_t *format, ...)
    /*@modifies *stream, fileSystem@*/ ;

/*@scanflike@*/ int fwscanf (FILE *stream, const wchar_t *format, ...)
	/*@modifies *stream, fileSystem@*/ ;

/* note use of sef --- stream may be evaluated more than once */
wint_t getwc (/*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ;

wint_t getwchar (void) /*@modifies fileSystem, *stdin@*/;

size_t mbrlen (const char *s, size_t n, /*@null@*/ mbstate_t *ps) /*@*/ ;

size_t mbrtowc (/*@null@*/ wchar_t *pwc, const char *s, size_t n,
		       /*@null@*/ mbstate_t *ps) 
   /*@modifies *pwc@*/ ;

int mbsinit (/*@null@*/ const mbstate_t *ps) /*@*/ ;

size_t mbsrtowcs (/*@null@*/ wchar_t *dst, const char **src, size_t len,
			 /*@null@*/ mbstate_t *ps) 
   /*@modifies *dst@*/ ;

/* note use of sef --- stream may be evaluated more than once */
wint_t putwc (wchar_t c, /*@sef@*/ FILE *stream)	/*@modifies fileSystem, *stream@*/ ;

wint_t putwchar (wchar_t c) /*@modifies fileSystem, *stdout@*/ ;

/*@printflike@*/ int swprintf (wchar_t *s, size_t n, const wchar_t *format, ...)
   /*@modifies *s@*/ ;

/*@scanflike@*/ int swscanf (const wchar_t *s, const wchar_t *format, ...)
   /*@modifies *stdin@*/ ;

wint_t ungetwc (wint_t c, FILE *stream) /*@modifies fileSystem, *stream@*/ ;

int vfwprintf (FILE *stream, const wchar_t *format, va_list arg)
   /*@modifies fileSystem, *stream@*/ ;

int vswprintf (wchar_t *s, size_t n, const wchar_t *format, va_list arg)
   /*@modifies *s@*/ ;

int vwprintf (const wchar_t *format, va_list arg)
   /*@modifies fileSystem, *stdout@*/ ;

size_t wcrtomb (/*@null@*/ /*@out@*/ char *s, wchar_t wc, /*@null@*/ mbstate_t *ps)
   /*@modifies *s@*/;

void /*@alt wchar_t *@*/
  wcscat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2)
  /*@modifies *s1@*/ ;

/*@exposed@*/ /*@null@*/ wchar_t *
  wcschr (/*@returned@*/ const wchar_t *s, wchar_t c)
  /*@*/ ;

int wcscmp (const wchar_t *s1, const wchar_t *s2) /*@*/ ;

int wcscoll (const wchar_t *s1, const wchar_t *s2) /*@*/ ;

void /*@alt wchar_t *@*/ 
  wcscpy (/*@unique@*/ /*@out@*/ /*@returned@*/ wchar_t *s1, const wchar_t *s2)
  /*@modifies *s1@*/ ;

size_t wcscspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;

size_t wcsftime (/*@out@*/ wchar_t *s, size_t maxsize, const wchar_t *format,
			const struct tm *timeptr) 
   /*@modifies *s@*/ ;

size_t wcslen (const wchar_t *s) /*@*/ ;

void /*@alt wchar_t *@*/
  wcsncat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
	   size_t n) 
  /*@modifies *s1@*/ ;

int wcsncmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;

void /*@alt wchar_t *@*/
  wcsncpy (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
	   size_t n) 
   /*@modifies *s1@*/ ;

/*@null@*/ wchar_t *
  wcspbrk (/*@returned@*/ const wchar_t *s1, const wchar_t *s2)
  /*@*/ ;

/*@null@*/ wchar_t *
  wcsrchr (/*@returned@*/ const wchar_t *s, wchar_t c)
  /*@*/ ;

size_t
  wcsrtombs (/*@null@*/ char *dst, const wchar_t **src, size_t len,
	     /*@null@*/ mbstate_t *ps) 
  /*@modifies *src@*/ ;

size_t wcsspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;

/*@null@*/ wchar_t *wcsstr (const wchar_t *s1, const wchar_t *s2) /*@*/ ;

double wcstod (const wchar_t *nptr, /*@null@*/ wchar_t **endptr)
   /*@modifies *endptr@*/ ;

/*@null@*/ wchar_t *
  wcstok (/*@null@*/ wchar_t *s1, const wchar_t *s2, wchar_t **ptr)
  /*@modifies *ptr@*/;

long wcstol (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
   /*@modifies *endptr@*/;

unsigned long
  wcstoul (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
  /*@modifies *endptr@*/;

size_t
  wcsxfrm (/*@null@*/ wchar_t *s1, const wchar_t *s2, size_t n)
  /*@modifies *s1@*/;

int wctob (wint_t c) /*@*/;

/*@null@*/ wchar_t *wmemchr (const wchar_t *s, wchar_t c, size_t n) /*@*/ ;

int wmemcmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;

wchar_t *wmemcpy (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
   /*@modifies *s1@*/;

wchar_t *wmemmove (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
   /*@modifies *s1@*/;

wchar_t *wmemset (/*@returned@*/ wchar_t *s, wchar_t c, size_t n)
   /*@modifies *s@*/;

/*@printflike@*/ int wprintf (const wchar_t *format, ...)
   /*@globals stdout@*/ /*@modifies errno, *stdout@*/;

/*@scanflike@*/ int
  wscanf (const wchar_t *format, ...)
  /*@globals stdin@*/ /*@modifies errno, *stdin@*/;

/*
** wctype.h (added by Amendment 1)
*/

/* Warning: not sure about these (maybe abstract?): */
typedef /*@integraltype@*/ wctype_t;
typedef /*@integraltype@*/ wctrans_t;

# ifdef STRICT
lltX_bool iswalnum (wint_t c) /*@*/ ;
lltX_bool iswalpha (wint_t c) /*@*/ ;
lltX_bool iswcntrl (wint_t c) /*@*/ ;
lltX_bool iswctype (wint_t c, wctype_t ctg) /*@*/ ;
lltX_bool iswdigit (wint_t c) /*@*/ ;
lltX_bool iswgraph (wint_t c) /*@*/ ;
lltX_bool iswlower (wint_t c) /*@*/ ;
lltX_bool iswprint (wint_t c) /*@*/ ;
lltX_bool iswpunct (wint_t c) /*@*/ ;
lltX_bool iswspace (wint_t c) /*@*/ ;
lltX_bool iswupper (wint_t c) /*@*/ ;
lltX_bool iswxdigit (wint_t c) /*@*/ ;

wint_t towctrans (wint_t c, wctrans_t ctg) /*@*/ ;
wint_t towlower (wint_t c) /*@*/ ;
wint_t towupper (wint_t c) /*@*/ ;
# else
lltX_bool /*@alt int@*/ iswalnum (wint_t c) /*@*/ ;
lltX_bool /*@alt int@*/ iswalpha (wint_t c) /*@*/ ;
lltX_bool /*@alt int@*/ iswcntrl (wint_t c) /*@*/ ;
lltX_bool /*@alt int@*/ iswctype (wint_t c, wctype_t ctg) /*@*/ ;
lltX_bool /*@alt int@*/ iswdigit (wint_t c) /*@*/ ;
lltX_bool /*@alt int@*/ iswgraph (wint_t c) /*@*/ ;
lltX_bool /*@alt int@*/ iswlower (wint_t c) /*@*/ ;
lltX_bool /*@alt int@*/ iswprint (wint_t c) /*@*/ ;
lltX_bool /*@alt int@*/ iswpunct (wint_t c) /*@*/ ;
lltX_bool /*@alt int@*/ iswspace (wint_t c) /*@*/ ;
lltX_bool /*@alt int@*/ iswupper (wint_t c) /*@*/ ;
lltX_bool /*@alt int@*/ iswxdigit (wint_t c) /*@*/ ;

wint_t /*@alt int@*/ towctrans (wint_t c, wctrans_t ctg)	/*@*/ ;
wint_t /*@alt int@*/ towlower (wint_t c)	/*@*/ ;
wint_t /*@alt int@*/ towupper (wint_t c)	/*@*/ ;
# endif

wctrans_t wctrans (const char *property)	/*@*/ ;
wctype_t wctype (const char *property) /*@*/ ;

int mblen (char *s, size_t n) /*@*/ ;
int mbtowc (/*@null@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n) 
   /*@modifies *pwc@*/ ;
int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar) 
   /*@modifies *s@*/ ;
size_t mbstowcs (/*@out@*/ wchar_t *pwcs, char *s, size_t n)
  /*@modifies *pwcs@*/ ;
size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n)
  /*@modifies *s@*/ ;

/*
** string.h
*/
     
void /*@alt void * @*/
  memcpy (/*@unique@*/ /*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n) 
  /*@modifies *s1@*/
     /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
     ;

void /*@alt void * @*/
  memmove (/*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
  /*@modifies *s1@*/
  /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
   ;

  
  /* drl
     modifed  12/29/2000
  */

void /*@alt char * @*/ 
  strcpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2) 
     /*@modifies *s1@*/ 
     /*@requires maxSet(s1) >= maxRead(s2) @*/
     /*@ensures maxRead(s1) == maxRead (s2) /\ maxRead(result) == maxRead(s2) /\ maxSet(result) == maxSet(s1); @*/;

void /*@alt char * @*/
  strncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2, size_t n) 
  /*@modifies *s1@*/      /*@requires maxSet(s1) >= ( n - 1 ); @*/ /*@ensures maxRead (s2) >= maxRead(s1) /\ maxRead (s1) <= n; @*/; 

void /*@alt char * @*/
  strcat (/*@unique@*/ /*@returned@*/ char *s1, char *s2) 
     /*@modifies *s1@*/ /*@requires maxSet(s1) >= (maxRead(s1) + maxRead(s2) );@*/
     /*@ensures maxRead(result) == (maxRead(s1) + maxRead(s2) );@*/;

void /*@alt char * @*/
  strncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, size_t n)
     /*@modifies *s1@*/ 
     /*@requires maxSet(s1) >= ( maxRead(s1) + n); @*/
      /*@ensures maxRead(s1) >= (maxRead(s1) + n); @*/;

     /*drl end*/
     
int memcmp (void *s1, void *s2, size_t n) /*@*/ ;
int strcmp (char *s1, char *s2) /*@*/ ;
int strcoll (char *s1, char *s2) /*@*/ ;
int strncmp (char *s1, char *s2, size_t n) /*@*/ ;
size_t strxfrm (/*@out@*/ /*@null@*/ char *s1, char *s2, size_t n) 
  /*@modifies *s1@*/ ;  /* s1 may be null only if n == 0 */ 

/*@null@*/ void *memchr (void *s, int c, size_t n) /*@*/ ;

# ifdef STRICT
/*@exposed@*/ /*@null@*/ char *
strchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
# else
/*@exposed@*/ /*@null@*/ char *
  strchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0; @*/ ;
# endif

size_t strcspn (char *s1, char *s2) /*@*/ ;
/*@null@*/ /*@exposed@*/ char *
  strpbrk (/*@returned@*/ char *s, char *t) /*@*/ ;

# ifdef STRICT
/*@null@*/ /*@exposed@*/ char *
  strrchr (/*@returned@*/ char *s, char c) /*@*/  /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
# else
/*@null@*/ /*@exposed@*/ char *
  strrchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/  /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
# endif

size_t strspn (char *s, char *t) /*@*/ ;

/*@null@*/ /*@exposed@*/  char *
  strstr (/*@returned@*/ /*@unique@*/ char *s, char *t) /*@*/
       /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 /\ maxRead(result) >= maxRead(t) /\ maxSet(result) >= maxRead(t)@*/ ;

/*@null@*/ /*@exposed@*/ char *
  strtok (/*@returned@*/ /*@null@*/ char *s, char *t)
  /*@modifies *s, internalState, errno@*/ ;

void /*@alt void *@*/ memset (/*@out@*/ /*@returned@*/ void *s, 
				     int c, size_t n)
     /*@modifies *s@*/ /*@requires maxSet(s) >= (n - 1) @*/ /*@ensures maxRead(s) >= (n - 1) @*/ ;

/*@observer@*/ char *strerror (int errnum) /*@*/ ;

/*drl */
size_t strlen (char *s) /*@*/ /*@ensures result == maxRead(s); @*/; 

/*
** time.h
*/

/*@constant int CLOCKS_PER_SEC;@*/

typedef /*@integraltype@*/ clock_t;
typedef /*@integraltype@*/ time_t;

struct tm
  {
    int tm_sec;
    int tm_min;
    int tm_hour;
    int tm_mday;
    int tm_mon;
    int tm_year;
    int tm_wday;
    int tm_yday;
    int tm_isdst;
  } ;

clock_t clock (void) /*@modifies internalState@*/ ;
double difftime (time_t time1, time_t time0) /*@*/ ;
time_t mktime (struct tm *timeptr) /*@*/ ;

time_t time (/*@null@*/ /*@out@*/ time_t *tp)
  /*@modifies *tp@*/ ;

/*@observer@*/ char *asctime (struct tm *timeptr) 
  /*@modifies errno*/ /*@ensures maxSet(result) == 25 /\  maxRead(result) == 25; @*/ ;

/*@observer@*/ char *ctime (time_t *tp) /*@*/
     /*@ensures maxSet(result) == 25 /\  maxRead(result) == 25; @*/;

/*@null@*/ /*@observer@*/ struct tm *gmtime (time_t *tp) /*@*/ ;

/*@null@*/ /*@observer@*/ struct tm *localtime (time_t *tp) 
  /*@modifies errno@*/ ;

size_t strftime (/*@out@*/ char *s, size_t smax,
			char *fmt, struct tm *timeptr)
  /*@modifies *s@*/ ;

/*
** ISO c99: 7.18 Integer types <stdint.h>
*/

/*
** These types are OPTIONAL.  Provide warnings on use.
*/

typedef /*@integraltype@*/ int8_t
   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least8_t instead."@*/ ;

typedef /*@integraltype@*/ int16_t
   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least16_t instead."@*/ ;

typedef /*@integraltype@*/ int32_t
   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least32_t instead."@*/ ;

typedef /*@integraltype@*/ int64_t
   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least64_t instead."@*/ ;

typedef /*@unsignedintegraltype@*/ uint8_t
   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least8_t instead."@*/ ;

typedef /*@unsignedintegraltype@*/ uint16_t
   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least16_t instead."@*/ ;

typedef /*@unsignedintegraltype@*/ uint32_t
   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least32_t instead."@*/ ;

typedef /*@unsignedintegraltype@*/ uint64_t
   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least64_t instead."@*/ ;

typedef /*@integraltype@*/ int_least8_t;
typedef /*@integraltype@*/ int_least16_t;
typedef /*@integraltype@*/ int_least32_t;
typedef /*@integraltype@*/ int_least64_t;

typedef /*@unsignedintegraltype@*/ uint_least8_t;
typedef /*@unsignedintegraltype@*/ uint_least16_t;
typedef /*@unsignedintegraltype@*/ uint_least32_t;
typedef /*@unsignedintegraltype@*/ uint_least64_t;

typedef /*@integraltype@*/ int_fast8_t;
typedef /*@integraltype@*/ int_fast16_t;
typedef /*@integraltype@*/ int_fast32_t;
typedef /*@integraltype@*/ int_fast64_t;

typedef /*@unsignedintegraltype@*/ uint_fast8_t;
typedef /*@unsignedintegraltype@*/ uint_fast16_t;
typedef /*@unsignedintegraltype@*/ uint_fast32_t;
typedef /*@unsignedintegraltype@*/ uint_fast64_t;

typedef int *intptr_t
   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;

typedef unsigned int *uintptr_t
   /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;

typedef /*@signedintegraltype@*/ intmax_t;
typedef /*@unsignedintegraltype@*/ uintmax_t;

/*
** What should the types be here? 
*/ /*#*/

/*@constant int INT8_MIN@*/
/*@constant int INT16_MIN@*/
/*@constant int INT32_MIN@*/
/*@constant int INT64_MIN@*/

/*@constant int INT8_MAX@*/
/*@constant int INT16_MAX@*/
/*@constant int INT32_MAX@*/
/*@constant int INT64_MAX@*/

/*@constant int UINT8_MIN@*/
/*@constant int UINT16_MIN@*/
/*@constant int UINT32_MIN@*/
/*@constant int UINT64_MIN@*/

/*@constant int INT_LEAST8_MIN@*/
/*@constant int INT_LEAST16_MIN@*/
/*@constant int INT_LEAST32_MIN@*/
/*@constant int INT_LEAST64_MIN@*/

/*@constant int INT_LEAST8_MAX@*/
/*@constant int INT_LEAST16_MAX@*/
/*@constant int INT_LEAST32_MAX@*/
/*@constant int INT_LEAST64_MAX@*/

/*@constant int UINT_LEAST8_MAX@*/
/*@constant int UINT_LEAST16_MAX@*/
/*@constant int UINT_LEAST32_MAX@*/
/*@constant int UINT_LEAST64_MAX@*/

/*@constant int INT_FAST8_MIN@*/
/*@constant int INT_FAST16_MIN@*/
/*@constant int INT_FAST32_MIN@*/
/*@constant int INT_FAST64_MIN@*/

/*@constant int INT_FAST8_MAX@*/
/*@constant int INT_FAST16_MAX@*/
/*@constant int INT_FAST32_MAX@*/
/*@constant int INT_FAST64_MAX@*/

/*@constant int UINT_FAST8_MAX@*/
/*@constant int UINT_FAST16_MAX@*/
/*@constant int UINT_FAST32_MAX@*/
/*@constant int UINT_FAST64_MAX@*/

/*@constant size_t INTPTR_MIN@*/
/*@constant size_t INTPTR_MAX@*/