/*
-** ansi.h --- LCLint Standard C Library
+** standard.h --- ISO C99 Standard Library for Splint.
**
** Process with -DSTRICT to get strict library.
*/
/*@constant int EILSEQ;@*/
# ifdef STRICT
-/*@checkedstrict@*/ extern int errno;
+/*@checkedstrict@*/ int errno;
# else
-/*@unchecked@*/ extern int errno;
+/*@unchecked@*/ int errno;
# endif
/*
/*@constant lltX_bool NDEBUG;@*/
# ifdef STRICT
-extern /*@falseexit@*/ void assert (/*@sef@*/ lltX_bool e)
+/*@falseexit@*/ void assert (/*@sef@*/ lltX_bool e)
/*@*/ ;
# else
-extern /*@falseexit@*/ void assert (/*@sef@*/ lltX_bool /*@alt int@*/ e)
+/*@falseexit@*/ void assert (/*@sef@*/ lltX_bool /*@alt int@*/ e)
/*@*/ ;
# endif
*/
# ifdef STRICT
-extern lltX_bool isalnum (int c) /*@*/ ;
-extern lltX_bool isalpha (int c) /*@*/ ;
-extern lltX_bool iscntrl (int c) /*@*/ ;
-extern lltX_bool isdigit (int c) /*@*/ ;
-extern lltX_bool isgraph (int c) /*@*/ ;
-extern lltX_bool islower (int c) /*@*/ ;
-extern lltX_bool isprint (int c) /*@*/ ;
-extern lltX_bool ispunct (int c) /*@*/ ;
-extern lltX_bool isspace (int c) /*@*/ ;
-extern lltX_bool isupper (int c) /*@*/ ;
-extern lltX_bool isxdigit (int c) /*@*/ ;
-extern char tolower (int c) /*@*/ ;
-extern char toupper (int c) /*@*/ ;
+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
-extern lltX_bool /*@alt int@*/ isalnum (int /*@alt unsigned char@*/ c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ isalpha (int /*@alt unsigned char@*/ c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ iscntrl (int /*@alt unsigned char@*/ c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ isdigit (int /*@alt unsigned char@*/ c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ isgraph (int /*@alt unsigned char@*/ c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ islower (int /*@alt unsigned char@*/ c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ isprint (int /*@alt unsigned char@*/ c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ ispunct (int /*@alt unsigned char@*/ c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ isspace (int /*@alt unsigned char@*/ c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ isupper (int /*@alt unsigned char@*/ c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ isxdigit (int /*@alt unsigned char@*/ c) /*@*/ ;
-extern char /*@alt int@*/ tolower (int /*@alt unsigned char@*/ c) /*@*/ ;
-extern char /*@alt int@*/ toupper (int /*@alt unsigned char@*/ c) /*@*/ ;
+/*
+** 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
/*
/*@constant int LC_NUMERIC;@*/
/*@constant int LC_TIME;@*/
-extern /*@observer@*/ /*@null@*/ char *setlocale (int category, /*@null@*/ char *locale)
+/*@observer@*/ /*@null@*/ char *setlocale (int category, /*@null@*/ char *locale)
/*@modifies internalState, errno@*/ ;
-extern struct lconv *localeconv (void) /*@*/ ;
+struct lconv *localeconv (void) /*@*/ ;
/*
** float.h
** constants. They may be used as lvalues.
*/
-/*@unchecked@*/ extern int DBL_DIG;
-/*@unchecked@*/ extern double DBL_EPSILON;
-/*@unchecked@*/ extern int DBL_MANT_DIG;
-/*@unchecked@*/ extern double DBL_MAX;
-/*@unchecked@*/ extern int DBL_MAX_10_EXP;
-/*@unchecked@*/ extern int DBL_MAX_EXP;
-/*@unchecked@*/ extern double DBL_MIN;
-/*@unchecked@*/ extern int DBL_MIN_10_EXP;
-/*@unchecked@*/ extern int DBL_MIN_EXP;
-
-/*@unchecked@*/ extern int FLT_DIG;
-/*@unchecked@*/ extern float FLT_EPSILON;
-/*@unchecked@*/ extern int FLT_MANT_DIG;
-/*@unchecked@*/ extern float FLT_MAX;
-/*@unchecked@*/ extern int FLT_MAX_10_EXP;
-/*@unchecked@*/ extern int FLT_MAX_EXP;
-/*@unchecked@*/ extern float FLT_MIN;
-/*@unchecked@*/ extern int FLT_MIN_10_EXP;
-/*@unchecked@*/ extern int FLT_MIN_EXP;
+/*@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@*/ extern int FLT_ROUNDS;
-
-/*@unchecked@*/ extern int LDBL_DIG;
-/*@unchecked@*/ extern long double LDBL_EPSILON;
-/*@unchecked@*/ extern int LDBL_MANT_DIG;
-/*@unchecked@*/ extern long double LDBL_MAX;
-/*@unchecked@*/ extern int LDBL_MAX_10_EXP;
-/*@unchecked@*/ extern int LDBL_MAX_EXP;
-/*@unchecked@*/ extern long double LDBL_MIN;
-/*@unchecked@*/ extern int LDBL_MIN_10_EXP;
-/*@unchecked@*/ extern int LDBL_MIN_EXP;
+/*@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
/*
** math.h
+**
+** evans 2002-07-03: updated from ISO C99 (http://www.vmunix.com/~gabor/c/draft.html)
*/
+typedef float float_t;
+typedef double double_t;
+
/*@constant double HUGE_VAL; @*/
+/*@constant float HUGE_VALF; @*/
+/*@constant long double HUGE_VALL; @*/
+
+/*@constant float INFINITY; @*/
+
+/*@constant float NAN; @*/
+ /*:warn implementationoptional "NAN is defined if and only if the implementation supports quiet float type NaNs.":*/ ;
+
+/*@constant int FP_INFINITE;@*/
+/*@constant int FP_NAN;@*/
+/*@constant int FP_NORMAL;@*/
+/*@constant int FP_SUBNORMAL;@*/
+/*@constant int FP_ZERO;@*/
+
+/*@constant int FP_ILOGB0;@*/
+/*@constant int FP_ILOGBNAN;@*/
+
+/*@constant int DECIMAL_DIG;@*/
+
+/* Defined for specs only - this type is any real type */
+typedef float /*@alt double, long double@*/ s_real_t;
+
+int fpclassify (/*@sef@*/ s_real_t) /*@*/ ;
+int signbit (/*@sef@*/ s_real_t) /*@*/ ;
+int isfinite (/*@sef@*/ s_real_t) /*@*/ ;
+int isnormal (/*@sef@*/ s_real_t) /*@*/ ;
+int isnan (/*@sef@*/ s_real_t) /*@*/ ;
+int isinf (/*@sef@*/ s_real_t) /*@*/ ;
/*
-** math functions that may have a range error modify errno
+** math functions that may have a range error modify errno (implementation defined).
*/
-extern double sin (double x) /*@*/ ;
-extern double cos (double x) /*@*/ ;
-extern double tan (double x) /*@*/ ;
-extern double asin (double x) /*@modifies errno@*/ ;
-extern double acos (double x) /*@modifies errno@*/ ;
-extern double atan (double x) /*@*/ ;
-extern double atan2 (double y, double x) /*@*/ ;
-extern double sinh (double x) /*@*/ ;
-extern double cosh (double x) /*@modifies errno@*/ ;
-extern double tanh (double x) /*@*/ ;
+double acos (double x) /*@modifies errno@*/ ;
+double asin (double x) /*@modifies errno@*/ ;
+double atan (double x) /*@*/ ;
+double atan2 (double y, double x) /*@*/ ;
-extern double exp (double x) /*@modifies errno@*/ ;
-extern double ldexp (double x, int n) /*@modifies errno@*/ ;
-extern double frexp (double x, /*@out@*/ int *xp) /*@modifies *xp;@*/ ;
+double cos (double x) /*@*/ ;
+double sin (double x) /*@*/ ;
+double tan (double x) /*@*/ ;
-extern double log (double x) /*@modifies errno@*/ ;
-extern double log10 (double x) /*@modifies errno@*/ ;
+double cosh (double x) /*@modifies errno@*/ ;
+double sinh (double x) /*@modifies errno@*/ ;
+double tanh (double x) /*@*/ ;
-extern double pow (double x, double y) /*@modifies errno@*/ ;
-extern double sqrt (double x) /*@modifies errno@*/ ;
+double acosh (double x) /*@modifies errno@*/ ;
+double asinh (double x) /*@modifies errno@*/ ;
+double atanh (double x) /*@modifies errno@*/ ;
-extern double ceil (double x) /*@*/ ;
-extern double floor (double x) /*@*/ ;
-extern double fabs (double x) /*@*/ ;
+double exp (double x) /*@modifies errno@*/ ;
+double frexp (double x, /*@out@*/ int *xp) /*@modifies *xp;@*/ ;
+double ldexp (double x, int n) /*@modifies errno@*/ ;
+
+double log (double x) /*@modifies errno@*/ ;
+double log10 (double x) /*@modifies errno@*/ ;
double modf (double x, /*@out@*/ double *ip) /*@modifies *ip;@*/ ;
+
+double exp2 (double x) /*@modifies errno@*/ ;
+double expm1 (double x) /*@modifies errno@*/ ;
+double log1p (double x) /*@modifies errno@*/ ;
+double log2 (double x) /*@modifies errno@*/ ;
+double logb (double x) /*@modifies errno@*/ ;
+
+double scalbn (double x, int n) /*@modifies errno@*/ ;
+double scalbln (double x, long int n) /*@modifies errno@*/ ;
+long double scalblnl(long double x, long int n) /*@modifies errno@*/ ;
+
+int ilogb (double x) /*@modifies errno@*/ ;
+int ilogbf (float x) /*@modifies errno@*/ ;
+int ilogbl (long double x) /*@modifies errno@*/ ;
+
+double fabs (double x) /*@*/ ;
+float fabsf (float x) /*@*/ ;
+long double fabsl (long double x) /*@*/ ;
+
+double pow (double x, double y) /*@modifies errno@*/ ;
+float powf(float x, float y) /*@modifies errno@*/ ;
+long double powl(long double x, long double y) /*@modifies errno@*/ ;
+
+double sqrt (double x) /*@modifies errno@*/ ;
+float sqrtf(float x) /*@modifies errno@*/ ;
+long double sqrtl (long double x) /*@modifies errno@*/ ;
+
+double cbrt (double x) /*@*/ ;
+float cbrtf (float x) /*@*/ ;
+long double cbrtl (long double x) /*@*/ ;
+
+double hypot (double x, double y) /*@modifies errno@*/ ;
+float hypotf (float x, float y) /*@modifies errno@*/ ;
+long double hypotl (long double x, long double y) /*@modifies errno@*/ ;
+
+double erf (double x) /*@*/ ;
+double erfc (double x) /*@*/ ;
+float erff (float x) /*@*/ ;
+long double erfl (long double x) /*@*/ ;
+float erfcf (float x) /*@*/ ;
+long double erfcl (long double x) /*@*/ ;
+
+double gamma (double x) /*@modifies errno@*/ ;
+float gammaf(float x) /*@modifies errno@*/ ;
+long double gammal (long double x) /*@modifies errno@*/ ;
+double lgamma (double x) /*@modifies errno@*/ ;
+float lgammaf (float x) /*@modifies errno@*/ ;
+long double lgammal (long double x) /*@modifies errno@*/ ;
+
+double ceil (double x) /*@*/ ;
+float ceilf(float x) /*@*/ ;
+long double ceill(long double x) /*@*/ ;
+
+double floor (double x) /*@*/ ;
+float floorf (float x) /*@*/ ;
+long double floorl (long double x) /*@*/ ;
+
+double nearbyint (double x) /*@*/ ;
+float nearbyintf (float x) /*@*/ ;
+long double nearbyintl (long double x) /*@*/ ;
+
+double rint (double x) /*@*/;
+float rintf (float x) /*@*/ ;
+long double rintl (long double x) /*@*/ ;
+long int lrint (double x) /*@modifies errno@*/ ;
+long int lrintf (float x) /*@modifies errno@*/ ;
+long int lrintl (long double x) /*@modifies errno@*/ ;
+long long llrint (double x) /*@modifies errno@*/ ;
+long long llrintf(float x) /*@modifies errno@*/ ;
+long long llrintl(long double x) /*@modifies errno@*/ ;
+
+double round (double x) /*@*/ ;
+long int lround (double x) /*@modifies errno@*/ ;
+long long llround (double x) /*@modifies errno@*/ ;
+
+double trunc (double x) /*@*/ ;
double fmod (double x, double y) /*@*/ ;
+double remainder (double x, double y) /*@*/ ;
+double remquo (double x, double y, /*@out@*/ int *quo) /*@modifies *quo@*/ ;
+double copysign (double x, double y) /*@*/ ;
+double nan (/*@nullterminated@*/ const char *tagp) /*@*/ ;
+double nextafter (double x, double y) /*@*/ ;
+double nextafterx (double x, long double y) /*@*/ ;
+
+double fdim (double x, double y) /*@modifies errno@*/ ;
+double fmax (double x, double y) /*@*/ ;
+double fmin (double x, double y) /*@*/ ;
+double fma (double x, double y, double z) /*@*/ ;
+
+int isgreater (s_real_t x, s_real_t y) /*@*/ ;
+int isgreaterequal (s_real_t x, s_real_t y) /*@*/ ;
+int isless (s_real_t x, s_real_t y) /*@*/ ;
+int islessequal (s_real_t x, s_real_t y) /*@*/ ;
+int islessgreater (s_real_t x, s_real_t y) /*@*/ ;
+int isunordered (s_real_t x, s_real_t y) /*@*/ ;
/*
** These functions are optional in iso C. An implementation does not
# ifdef OPTIONAL_MATH
-extern float acosf (float x) /*@modifies errno@*/ ;
-extern long double acosl (long double x) /*@modifies errno@*/ ;
-extern float asinf (float x) /*@modifies errno@*/ ;
-extern long double asinl (long double x) /*@modifies errno@*/ ;
-extern float atanf (float x) /*@*/ ;
-extern long double atanl (long double x) /*@*/ ;
-extern float atan2f (float y, float x) /*@*/ ;
-extern long double atan2l (long double y, long double x) /*@*/ ;
-extern float ceilf (float x) /*@*/ ;
-extern long double ceill (long double x) /*@*/ ;
-extern float cosf (float x) /*@*/ ;
-extern long double cosl (long double x) /*@*/ ;
-extern float coshf (float x) /*@modifies errno@*/ ;
-extern long double coshl (long double x) /*@modifies errno@*/ ;
-extern float expf (float x) /*@modifies errno@*/ ;
-extern long double expl (long double x) /*@modifies errno@*/;
-extern float fabsf (float x) /*@*/ ;
-extern long double fabsl (long double x) /*@*/ ;
-extern float floorf (float x) /*@*/ ;
-extern long double floorl (long double x) /*@*/ ;
-extern float fmodf (float x, float y) /*@*/ ;
-extern long double fmodl (long double x, long double y) /*@*/ ;
-extern float frexpf (float x, /*@out@*/ int *xp) /*@modifies *xp@*/;
-extern long double frexpl (long double x, /*@out@*/ int *xp) /*@modifies *xp@*/;
-extern float ldexpf (float x, int n) /*@modifies errno@*/ ;
-extern long double ldexpl (long double x, int n) /*@modifies errno@*/ ;
-extern float logf (float x) /*@modifies errno@*/ ;
-extern long double logl (long double x) /*@modifies errno@*/ ;
-extern float log10f (float x) /*@modifies errno@*/;
-extern long double log10l (long double x) /*@modifies errno@*/;
-extern float modff (float x, /*@out@*/ float *xp) /*@modifies *xp@*/ ;
-extern long double modfl (long double x, /*@out@*/ long double *xp) /*@modifies *xp@*/ ;
-extern float powf (float x, float y) /*@modifies errno@*/ ;
-extern long double powl (long double x, long double y) /*@modifies errno@*/ ;
-extern float sinf (float x) /*@*/ ;
-extern long double sinl (long double x) /*@*/ ;
-extern float sinhf (float x) /*@*/ ;
-extern long double sinhl (long double x) /*@*/ ;
-extern float sqrtf (float x) /*@modifies errno@*/ ;
-extern long double sqrtl (long double x) /*@modifies errno@*/ ;
-extern float tanf (float x) /*@*/ ;
-extern long double tanl (long double x) /*@*/ ;
-extern float tanhf (float x) /*@*/ ;
-extern long double tanhl (long double x) /*@*/ ;
+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
typedef /*@abstract@*/ /*@mutable@*/ void *jmp_buf;
-extern int setjmp (/*@out@*/ jmp_buf env) /*@modifies env;@*/ ;
-extern /*@mayexit@*/ void longjmp (jmp_buf env, int val) /*@*/ ;
+int setjmp (/*@out@*/ jmp_buf env) /*@modifies env;@*/ ;
+/*@mayexit@*/ void longjmp (jmp_buf env, int val) /*@*/ ;
/*
** signal.h
** returns the function (or NULL if unsuccessful).
*/
-extern /*@null@*/ void (*signal (int sig, /*@null@*/ void (*func)(int))) (int)
+/*@null@*/ void (*signal (int sig, /*@null@*/ void (*func)(int))) (int)
/*@modifies internalState, errno;@*/ ;
-extern /*@mayexit@*/ int raise (int sig) ;
+/*@mayexit@*/ int raise (int sig) ;
/*
** stdarg.h
typedef /*@abstract@*/ /*@mutable@*/ void *va_list;
-extern void va_start (/*@out@*/ va_list ap, ...) /*@modifies ap;@*/ ;
-extern void va_end (va_list va) /*@modifies va;@*/ ;
+void va_start (/*@out@*/ va_list ap, ...) /*@modifies ap;@*/ ;
+void va_end (va_list va) /*@modifies va;@*/ ;
/*
** va_arg is builtin
typedef /*@abstract@*/ /*@mutable@*/ void *FILE;
typedef /*@abstract@*/ /*@mutable@*/ void *fpos_t;
-/*@constant int _IOFBF; @*/
-/*@constant int _IOLBF; @*/
-/*@constant int _IONBF; @*/
+/*@constant size_t _IOFBF; @*/
+/*@constant size_t _IOLBF; @*/
+/*@constant size_t _IONBF; @*/
+
+/*@constant size_t BUFSIZ; @*/ /* evans 2002-02-27 change suggested by Walter Briscoe */
-/*@constant int BUFSIZ; @*/
/*@constant int EOF; @*/
/*@constant int FOPEN_MAX; @*/
/*@unchecked@*/ FILE *stdout;
# endif
-extern int remove (char *filename) /*@modifies fileSystem, errno@*/ ;
-extern int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ;
+int remove (char *filename) /*@modifies fileSystem, errno@*/ ;
+int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ;
+
+/*@dependent@*/ /*@null@*/ FILE *tmpfile (void)
+ /*@modifies fileSystem, errno@*/ ;
-extern /*@null@*/ FILE *tmpfile (void) /*@modifies fileSystem@*/ ;
-extern /*@observer@*/ char *
+/*@observer@*/ char *
tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s)
/*@modifies *s, internalState@*/ ;
-extern int fclose (FILE *stream) /*@modifies *stream, errno, fileSystem;@*/ ;
-extern int fflush (/*@null@*/ FILE *stream)
+int fclose (FILE *stream)
/*@modifies *stream, errno, fileSystem;@*/ ;
-extern /*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode)
+int fflush (/*@null@*/ FILE *stream)
+ /*@modifies *stream, errno, fileSystem;@*/ ;
+
+/*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode)
/*@modifies fileSystem@*/ ;
-extern /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream)
+/*@dependent@*/ /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream)
/*@modifies *stream, fileSystem, errno@*/ ;
-extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf)
- /*@modifies fileSystem, *stream, *buf@*/ ;
+void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf)
+ /*@modifies fileSystem, *stream, *buf@*/
+ /*:errorcode != 0*/ ;
+ /*:requires maxSet(buf) >= (BUFSIZ - 1):*/ ;
-extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf,
- int mode, size_t size)
- /*@modifies fileSystem, *stream, *buf@*/ ;
+int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf,
+ int mode, size_t size)
+ /*@modifies fileSystem, *stream, *buf@*/
+ /*@requires maxSet(buf) >= (size - 1) @*/ ;
# ifdef STRICT
/*@printflike@*/
-extern int fprintf (FILE *stream, char *format, ...)
+int fprintf (FILE *stream, char *format, ...)
/*@modifies fileSystem, *stream@*/ ;
# else
/*@printflike@*/
-extern int /*@alt void@*/ fprintf (FILE *stream, char *format, ...)
+int /*@alt void@*/ fprintf (FILE *stream, char *format, ...)
/*@modifies fileSystem, *stream@*/ ;
# endif
/*@scanflike@*/
-extern int fscanf (FILE *stream, char *format, ...)
- /*@modifies fileSystem, *stream@*/ ;
+int fscanf (FILE *stream, char *format, ...)
+ /*@modifies fileSystem, *stream, errno@*/ ;
# ifdef STRICT
/*@printflike@*/
-extern int printf (char *format, ...)
+int printf (char *format, ...)
/*@globals stdout@*/
/*@modifies fileSystem, *stdout@*/ ;
# else
/*@printflike@*/
-extern int /*@alt void@*/ printf (char *format, ...)
+int /*@alt void@*/ printf (char *format, ...)
/*@globals stdout@*/
/*@modifies fileSystem, *stdout@*/ ;
# endif
/*@scanflike@*/
-extern int scanf(char *format, ...)
+int scanf(char *format, ...)
/*@globals stdin@*/
- /*@modifies fileSystem, *stdin@*/ ;
+ /*@modifies fileSystem, *stdin, errno@*/ ;
+ /*drl added errno 09-19-2001 */ ;
# ifdef STRICT
/*@printflike@*/
-extern int sprintf (/*@out@*/ char *s, char *format, ...)
+int sprintf (/*@out@*/ char *s, char *format, ...)
+ /*@warn bufferoverflowhigh "Buffer overflow possible with sprintf. Recommend using snprintf instead"@*/
/*@modifies *s@*/ ;
# else
/*@printflike@*/
-extern int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...)
+int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...)
+ /*@warn bufferoverflowhigh "Buffer overflow possible with sprintf. Recommend using snprintf instead"@*/
/*@modifies *s@*/ ;
# endif
+/* evans 2002-07-09: snprintf added to standard.h (from unix.h) */
+/*@printflike@*/
+int snprintf (/*@out@*/ char * restrict s, size_t n, const char * restrict format, ...)
+ /*@modifies s@*/
+ /*@requires maxSet(s) >= (n - 1)@*/ ;
+
/*@scanflike@*/
-int sscanf (/*@out@*/ char *s, char *format, ...) /*@*/ ;
+int sscanf (/*@out@*/ char *s, char *format, ...) /*@modifies errno@*/ ;
/* modifies extra arguments */
int vprintf (const char *format, va_list arg)
/*@modifies str@*/ ;
int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap)
- /*@requires maxSet(str) >= size@*/
+ /*@requires maxSet(str) >= (size - 1)@*/ /* drl - this was size, size-1 in stdio.h */
/*@modifies str@*/ ;
-extern int fgetc (FILE *stream)
+int fgetc (FILE *stream)
/*@modifies fileSystem, *stream, errno@*/ ;
-extern /*@null@*/ char *
+/*@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; @*/
+ /*@requires maxSet(s) >= (n -1); @*/
+ /*@ensures maxRead(s) <= (n -1) /\ maxRead(s) >= 0; @*/
;
-extern int fputc (int /*@alt char@*/ c, FILE *stream)
+int fputc (int /*@alt char@*/ c, FILE *stream)
+ /*:errorcode EOF:*/
/*@modifies fileSystem, *stream, errno@*/ ;
-extern int fputs (char *s, FILE *stream)
+int fputs (char *s, FILE *stream)
/*@modifies fileSystem, *stream@*/ ;
/* note use of sef --- stream may be evaluated more than once */
-extern int getc (/*@sef@*/ FILE *stream)
- /*@modifies fileSystem, *stream@*/ ;
+int getc (/*@sef@*/ FILE *stream)
+ /*@modifies fileSystem, *stream, errno@*/ ;
-extern int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/ ;
+int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin, errno@*/ ;
-extern /*@null@*/ char *gets (/*@out@*/ char *s)
+/*@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@*/ ;
-extern int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
- /*@modifies fileSystem, *stream;@*/ ;
+int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
+ /*:errorcode EOF:*/
+ /*@modifies fileSystem, *stream, errno;@*/ ;
-extern int putchar (int /*@alt char@*/ c)
- /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ;
+int putchar (int /*@alt char@*/ c)
+ /*:errorcode EOF:*/
+ /*@globals stdout@*/
+ /*@modifies fileSystem, *stdout, errno@*/ ;
-extern int puts (const char *s)
- /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ;
+int puts (const char *s)
+ /*:errorcode EOF:*/
+ /*@globals stdout@*/
+ /*@modifies fileSystem, *stdout, errno@*/ ;
-extern int ungetc (int /*@alt char@*/ c, FILE *stream)
- /*@modifies fileSystem, *stream, errno@*/ ;
+int ungetc (int /*@alt char@*/ c, FILE *stream)
+ /*@modifies fileSystem, *stream@*/ ;
+ /*drl REMOVED errno 09-19-2001*/
-extern size_t
+size_t
fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream)
- /*@modifies fileSystem, *ptr, *stream, errno@*/ ;
+ /*@modifies fileSystem, *ptr, *stream, errno@*/
+ /*requires maxSet(ptr) >= (size - 1) @*/
+ /*@ensures maxRead(ptr) == (size - 1) @*/ ;
-extern size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream)
- /*@modifies fileSystem, *stream, errno@*/ ;
+size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream)
+ /*@modifies fileSystem, *stream, errno@*/
+ /*@requires maxRead(ptr) >= size @*/ ;
-extern int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos)
- /*@modifies *pos, errno@*/ ;
+int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos)
+ /*@modifies *pos, errno@*/
+ /*@requires maxSet(pos) >= 0@*/
+ /*@ensures maxRead(pos) >= 0 @*/;
-extern int fseek (FILE *stream, long int offset, int whence)
- /*@modifies fileSystem, *stream, errno@*/ ;
+int fseek (FILE *stream, long int offset, int whence)
+ /*:errorcode -1:*/
+ /*@modifies fileSystem, *stream, errno@*/ ;
-extern int fsetpos (FILE *stream, fpos_t *pos)
+int fsetpos (FILE *stream, fpos_t *pos)
/*@modifies fileSystem, *stream, errno@*/ ;
-extern long int ftell(FILE *stream) /*@modifies errno@*/ ;
+long int ftell(FILE *stream)
+ /*:errorcode -1:*/ /*@modifies errno*/ ;
+
+void rewind (FILE *stream) /*@modifies *stream@*/ ;
+void clearerr (FILE *stream) /*@modifies *stream@*/ ;
-extern void rewind (FILE *stream) /*@modifies *stream@*/ ;
-extern void clearerr (FILE *stream) /*@modifies *stream@*/ ;
+int feof (FILE *stream) /*@modifies errno@*/ ;
-extern int feof (FILE *stream) /*@modifies errno@*/ ;
-extern int ferror (FILE *stream) /*@modifies errno@*/ ;
+int ferror (FILE *stream) /*@modifies errno@*/ ;
-extern void perror (/*@null@*/ char *s)
+void perror (/*@null@*/ char *s)
/*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ;
/*
** stdlib.h
*/
-extern double atof (char *s) /*@*/ ;
-extern int atoi (char *s) /*@*/ ;
-extern long int atol (char *s) /*@*/ ;
+double atof (char *s) /*@*/ ;
+int atoi (char *s) /*@*/ ;
+long int atol (char *s) /*@*/ ;
-extern double strtod (char *s, /*@null@*/ /*@out@*/ char **endp)
+double strtod (char *s, /*@null@*/ /*@out@*/ char **endp)
/*@modifies *endp, errno@*/ ;
-extern long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
+long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
/*@modifies *endp, errno@*/ ;
-extern unsigned long
+unsigned long
strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
/*@modifies *endp, errno@*/ ;
/*@constant int RAND_MAX; @*/
-extern int rand (void) /*@modifies internalState@*/ ;
-extern void srand (unsigned int seed) /*@modifies internalState@*/ ;
+int rand (void) /*@modifies internalState@*/ ;
+void srand (unsigned int seed) /*@modifies internalState@*/ ;
/*
drl
changed 12/29/2000
*/
-extern /*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/
- /*@ensures MaxSet(result) == (nobj - 1); @*/ ;
-extern /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@*/
- /*@ensures MaxSet(result) == (size - 1); @*/ ;
+/*@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
-extern /*@null@*/ /*@only@*/ void *
+/*@null@*/ /*@only@*/ void *
realloc (/*@null@*/ /*@only@*/ /*@special@*/ void *p,
size_t size) /*@releases p@*/ /*@modifies *p@*/
- /*@ensures MaxSet(result) >= (size - 1) @*/;
+ /*@ensures maxSet(result) == (size - 1) @*/;
# endif
/*
** Otherwise, storage is in the same state before and after the call.
*/
-extern /*@null@*/ /*@only@*/ void *
+/*@null@*/ /*@only@*/ void *
realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size)
- /*@modifies *p@*/ /*@ensures MaxSet(result) >= (size - 1) @*/;
+ /*@modifies *p@*/ /*@ensures maxSet(result) >= (size - 1) @*/;
-extern void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies p@*/ ;
+void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies p@*/ ;
/*@constant int EXIT_FAILURE; @*/
/*@constant int EXIT_SUCCESS; @*/
-extern /*@exits@*/ void abort (void) /*@*/ ;
-extern /*@exits@*/ void exit (int status) /*@*/ ;
-extern int atexit (void (*func)(void)) /*@modifies internalState@*/ ;
+/*@exits@*/ void abort (void) /*@*/ ;
+/*@exits@*/ void exit (int status) /*@*/ ;
+int atexit (void (*func)(void)) /*@modifies internalState@*/ ;
-extern /*@observer@*/ /*@null@*/ char *getenv (char *name) /*@*/ ;
+/*@observer@*/ /*@null@*/ char *getenv (char *name) /*@*/ ;
-extern int system (/*@null@*/ char *s) /*@modifies fileSystem@*/ ;
+int system (/*@null@*/ char *s) /*@modifies fileSystem@*/ ;
-extern /*@null@*/ /*@dependent@*/ void *
+/*@null@*/ /*@dependent@*/ void *
bsearch (void *key, void *base,
size_t n, size_t size,
int (*compar)(void *, void *)) /*@*/ ;
-extern void qsort (void *base, size_t n, size_t size,
+void qsort (void *base, size_t n, size_t size,
int (*compar)(void *, void *))
/*@modifies *base, errno@*/ ;
-extern int abs (int n) /*@*/ ;
+int abs (int n) /*@*/ ;
typedef /*@concrete@*/ struct
{
int rem;
} div_t ;
-extern div_t div (int num, int denom) /*@*/ ;
+div_t div (int num, int denom) /*@*/ ;
-extern long int labs (long int n) /*@*/ ;
+long int labs (long int n) /*@*/ ;
typedef /*@concrete@*/ struct
{
long int rem;
} ldiv_t ;
-extern ldiv_t ldiv (long num, long denom) /*@*/ ;
+ldiv_t ldiv (long num, long denom) /*@*/ ;
/*@constant size_t MB_CUR_MAX; @*/
/*@constant int WCHAR_MIN@*/
/*@constant wint_t WEOF@*/
-extern wint_t btowc (int c) /*@*/ ;
+wint_t btowc (int c) /*@*/ ;
-extern wint_t fgetwc (FILE *fp) /*@modifies fileSystem, *fp*/ ;
+wint_t fgetwc (FILE *fp) /*@modifies fileSystem, *fp*/ ;
-extern /*@null@*/ wchar_t *fgetws (/*@returned@*/ wchar_t *s, int n, FILE *stream)
+/*@null@*/ wchar_t *fgetws (/*@returned@*/ wchar_t *s, int n, FILE *stream)
/*@modifies fileSystem, *s, *stream@*/;
-extern wint_t fputwc (wchar_t c, FILE *stream)
+wint_t fputwc (wchar_t c, FILE *stream)
/*@modifies fileSystem, *stream@*/;
-extern int fputws (const wchar_t *s, FILE *stream)
+int fputws (const wchar_t *s, FILE *stream)
/*@modifies fileSystem, *stream@*/ ;
-extern int fwide (FILE *stream, int mode) /*@*/ ;
+int fwide (FILE *stream, int mode) /*@*/ ;
/* does not modify the stream */
-/*@printflike@*/ extern int fwprintf (FILE *stream, const wchar_t *format, ...)
+/*@printflike@*/ int fwprintf (FILE *stream, const wchar_t *format, ...)
/*@modifies *stream, fileSystem@*/ ;
-/*@scanflike@*/ extern int fwscanf (FILE *stream, const wchar_t *format, ...)
+/*@scanflike@*/ int fwscanf (FILE *stream, const wchar_t *format, ...)
/*@modifies *stream, fileSystem@*/ ;
/* note use of sef --- stream may be evaluated more than once */
-extern wint_t getwc (/*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ;
+wint_t getwc (/*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ;
-extern wint_t getwchar (void) /*@modifies fileSystem, *stdin@*/;
+wint_t getwchar (void) /*@modifies fileSystem, *stdin@*/;
-extern size_t mbrlen (const char *s, size_t n, /*@null@*/ mbstate_t *ps) /*@*/ ;
+size_t mbrlen (const char *s, size_t n, /*@null@*/ mbstate_t *ps) /*@*/ ;
-extern size_t mbrtowc (/*@null@*/ wchar_t *pwc, const char *s, size_t n,
+size_t mbrtowc (/*@null@*/ wchar_t *pwc, const char *s, size_t n,
/*@null@*/ mbstate_t *ps)
/*@modifies *pwc@*/ ;
-extern int mbsinit (/*@null@*/ const mbstate_t *ps) /*@*/ ;
+int mbsinit (/*@null@*/ const mbstate_t *ps) /*@*/ ;
-extern size_t mbsrtowcs (/*@null@*/ wchar_t *dst, const char **src, size_t len,
+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 */
-extern wint_t putwc (wchar_t c, /*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ;
+wint_t putwc (wchar_t c, /*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ;
-extern wint_t putwchar (wchar_t c) /*@modifies fileSystem, *stdout@*/ ;
+wint_t putwchar (wchar_t c) /*@modifies fileSystem, *stdout@*/ ;
-/*@printflike@*/ extern int swprintf (wchar_t *s, size_t n, const wchar_t *format, ...)
+/*@printflike@*/ int swprintf (wchar_t *s, size_t n, const wchar_t *format, ...)
/*@modifies *s@*/ ;
-/*@scanflike@*/ extern int swscanf (const wchar_t *s, const wchar_t *format, ...)
+/*@scanflike@*/ int swscanf (const wchar_t *s, const wchar_t *format, ...)
/*@modifies *stdin@*/ ;
-extern wint_t ungetwc (wint_t c, FILE *stream) /*@modifies fileSystem, *stream@*/ ;
+wint_t ungetwc (wint_t c, FILE *stream) /*@modifies fileSystem, *stream@*/ ;
-extern int vfwprintf (FILE *stream, const wchar_t *format, va_list arg)
+int vfwprintf (FILE *stream, const wchar_t *format, va_list arg)
/*@modifies fileSystem, *stream@*/ ;
-extern int vswprintf (wchar_t *s, size_t n, const wchar_t *format, va_list arg)
+int vswprintf (wchar_t *s, size_t n, const wchar_t *format, va_list arg)
/*@modifies *s@*/ ;
-extern int vwprintf (const wchar_t *format, va_list arg)
+int vwprintf (const wchar_t *format, va_list arg)
/*@modifies fileSystem, *stdout@*/ ;
-extern size_t wcrtomb (/*@null@*/ /*@out@*/ char *s, wchar_t wc, /*@null@*/ mbstate_t *ps)
+size_t wcrtomb (/*@null@*/ /*@out@*/ char *s, wchar_t wc, /*@null@*/ mbstate_t *ps)
/*@modifies *s@*/;
-extern void /*@alt wchar_t *@*/
+void /*@alt wchar_t *@*/
wcscat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2)
/*@modifies *s1@*/ ;
-extern /*@exposed@*/ /*@null@*/ wchar_t *
+/*@exposed@*/ /*@null@*/ wchar_t *
wcschr (/*@returned@*/ const wchar_t *s, wchar_t c)
/*@*/ ;
-extern int wcscmp (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
+int wcscmp (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
-extern int wcscoll (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
+int wcscoll (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
-extern void /*@alt wchar_t *@*/
+void /*@alt wchar_t *@*/
wcscpy (/*@unique@*/ /*@out@*/ /*@returned@*/ wchar_t *s1, const wchar_t *s2)
/*@modifies *s1@*/ ;
-extern size_t wcscspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
+size_t wcscspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
-extern size_t wcsftime (/*@out@*/ wchar_t *s, size_t maxsize, const wchar_t *format,
+size_t wcsftime (/*@out@*/ wchar_t *s, size_t maxsize, const wchar_t *format,
const struct tm *timeptr)
/*@modifies *s@*/ ;
-extern size_t wcslen (const wchar_t *s) /*@*/ ;
+size_t wcslen (const wchar_t *s) /*@*/ ;
-extern void /*@alt wchar_t *@*/
+void /*@alt wchar_t *@*/
wcsncat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
size_t n)
/*@modifies *s1@*/ ;
-extern int wcsncmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
+int wcsncmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
-extern void /*@alt wchar_t *@*/
+void /*@alt wchar_t *@*/
wcsncpy (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
size_t n)
/*@modifies *s1@*/ ;
-extern /*@null@*/ wchar_t *
+/*@null@*/ wchar_t *
wcspbrk (/*@returned@*/ const wchar_t *s1, const wchar_t *s2)
/*@*/ ;
-extern /*@null@*/ wchar_t *
+/*@null@*/ wchar_t *
wcsrchr (/*@returned@*/ const wchar_t *s, wchar_t c)
/*@*/ ;
-extern size_t
+size_t
wcsrtombs (/*@null@*/ char *dst, const wchar_t **src, size_t len,
/*@null@*/ mbstate_t *ps)
/*@modifies *src@*/ ;
-extern size_t wcsspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
+size_t wcsspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
-extern /*@null@*/ wchar_t *wcsstr (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
+/*@null@*/ wchar_t *wcsstr (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
-extern double wcstod (const wchar_t *nptr, /*@null@*/ wchar_t **endptr)
+double wcstod (const wchar_t *nptr, /*@null@*/ wchar_t **endptr)
/*@modifies *endptr@*/ ;
-extern /*@null@*/ wchar_t *
+/*@null@*/ wchar_t *
wcstok (/*@null@*/ wchar_t *s1, const wchar_t *s2, wchar_t **ptr)
/*@modifies *ptr@*/;
-extern long wcstol (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
+long wcstol (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
/*@modifies *endptr@*/;
-extern unsigned long
+unsigned long
wcstoul (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
/*@modifies *endptr@*/;
-extern size_t
+size_t
wcsxfrm (/*@null@*/ wchar_t *s1, const wchar_t *s2, size_t n)
/*@modifies *s1@*/;
-extern int wctob (wint_t c) /*@*/;
+int wctob (wint_t c) /*@*/;
-extern /*@null@*/ wchar_t *wmemchr (const wchar_t *s, wchar_t c, size_t n) /*@*/ ;
+/*@null@*/ wchar_t *wmemchr (const wchar_t *s, wchar_t c, size_t n) /*@*/ ;
-extern int wmemcmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
+int wmemcmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
-extern wchar_t *wmemcpy (/*@returned@*/ 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@*/;
-extern wchar_t *wmemmove (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
+wchar_t *wmemmove (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
/*@modifies *s1@*/;
-extern wchar_t *wmemset (/*@returned@*/ wchar_t *s, wchar_t c, size_t n)
+wchar_t *wmemset (/*@returned@*/ wchar_t *s, wchar_t c, size_t n)
/*@modifies *s@*/;
-/*@printflike@*/ extern int wprintf (const wchar_t *format, ...)
+/*@printflike@*/ int wprintf (const wchar_t *format, ...)
/*@globals stdout@*/ /*@modifies errno, *stdout@*/;
-/*@scanflike@*/ extern int
+/*@scanflike@*/ int
wscanf (const wchar_t *format, ...)
/*@globals stdin@*/ /*@modifies errno, *stdin@*/;
typedef /*@integraltype@*/ wctrans_t;
# ifdef STRICT
-extern lltX_bool iswalnum (wint_t c) /*@*/ ;
-extern lltX_bool iswalpha (wint_t c) /*@*/ ;
-extern lltX_bool iswcntrl (wint_t c) /*@*/ ;
-extern lltX_bool iswctype (wint_t c, wctype_t ctg) /*@*/ ;
-extern lltX_bool iswdigit (wint_t c) /*@*/ ;
-extern lltX_bool iswgraph (wint_t c) /*@*/ ;
-extern lltX_bool iswlower (wint_t c) /*@*/ ;
-extern lltX_bool iswprint (wint_t c) /*@*/ ;
-extern lltX_bool iswpunct (wint_t c) /*@*/ ;
-extern lltX_bool iswspace (wint_t c) /*@*/ ;
-extern lltX_bool iswupper (wint_t c) /*@*/ ;
-extern lltX_bool iswxdigit (wint_t c) /*@*/ ;
-
-extern wint_t towctrans (wint_t c, wctrans_t ctg) /*@*/ ;
-extern wint_t towlower (wint_t c) /*@*/ ;
-extern wint_t towupper (wint_t c) /*@*/ ;
+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
-extern lltX_bool /*@alt int@*/ iswalnum (wint_t c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ iswalpha (wint_t c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ iswcntrl (wint_t c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ iswctype (wint_t c, wctype_t ctg) /*@*/ ;
-extern lltX_bool /*@alt int@*/ iswdigit (wint_t c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ iswgraph (wint_t c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ iswlower (wint_t c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ iswprint (wint_t c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ iswpunct (wint_t c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ iswspace (wint_t c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ iswupper (wint_t c) /*@*/ ;
-extern lltX_bool /*@alt int@*/ iswxdigit (wint_t c) /*@*/ ;
-
-extern wint_t /*@alt int@*/ towctrans (wint_t c, wctrans_t ctg) /*@*/ ;
-extern wint_t /*@alt int@*/ towlower (wint_t c) /*@*/ ;
-extern wint_t /*@alt int@*/ towupper (wint_t c) /*@*/ ;
+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
-extern wctrans_t wctrans (const char *property) /*@*/ ;
-extern wctype_t wctype (const char *property) /*@*/ ;
+wctrans_t wctrans (const char *property) /*@*/ ;
+wctype_t wctype (const char *property) /*@*/ ;
-extern int mblen (char *s, size_t n) /*@*/ ;
-extern int mbtowc (/*@null@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n)
+int mblen (char *s, size_t n) /*@*/ ;
+int mbtowc (/*@null@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n)
/*@modifies *pwc@*/ ;
-extern int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar)
+int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar)
/*@modifies *s@*/ ;
-extern size_t mbstowcs (/*@out@*/ wchar_t *pwcs, char *s, size_t n)
+size_t mbstowcs (/*@out@*/ wchar_t *pwcs, char *s, size_t n)
/*@modifies *pwcs@*/ ;
-extern size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n)
+size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n)
/*@modifies *s@*/ ;
/*
** string.h
*/
-extern void /*@alt void * @*/
+void /*@alt void * @*/
memcpy (/*@unique@*/ /*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
/*@modifies *s1@*/
- /*@requires MaxRead(s2) >= n /\ MaxSet(s1) >= n; @*/
+ /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
;
-extern void /*@alt void * @*/
+void /*@alt void * @*/
memmove (/*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
/*@modifies *s1@*/
- /*@requires MaxRead(s2) >= n /\ MaxSet(s1) >= n; @*/
+ /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
;
modifed 12/29/2000
*/
-extern void /*@alt char * @*/
+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); @*/;
+ /*@requires maxSet(s1) >= maxRead(s2) @*/
+ /*@ensures maxRead(s1) == maxRead (s2) /\ maxRead(result) == maxRead(s2) /\ maxSet(result) == maxSet(s1); @*/;
-extern void /*@alt char * @*/
+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; @*/;
+ /*@modifies *s1@*/
+ /*@requires maxSet(s1) >= ( n - 1 ); @*/
+ /*@ensures maxRead (s2) >= maxRead(s1) /\ maxRead (s1) <= n; @*/ ;
-extern void /*@alt char * @*/
+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) );@*/;
+ /*@modifies *s1@*/ /*@requires maxSet(s1) >= (maxRead(s1) + maxRead(s2) );@*/
+ /*@ensures maxRead(result) == (maxRead(s1) + maxRead(s2) );@*/;
-extern void /*@alt char * @*/
+void /*@alt char * @*/
strncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, size_t n)
- /*@modifies *s1@*/ /*@requires MaxSet(s1) >= ( MaxRead(s1) + n); @*/ /*@ensures MaxRead(result) >= (MaxRead(s1) + n); @*/;
+ /*@modifies *s1@*/
+ /*@requires maxSet(s1) >= ( maxRead(s1) + n); @*/
+ /*@ensures maxRead(s1) >= (maxRead(s1) + n); @*/;
/*drl end*/
-extern int memcmp (void *s1, void *s2, size_t n) /*@*/ ;
-extern int strcmp (char *s1, char *s2) /*@*/ ;
-extern int strcoll (char *s1, char *s2) /*@*/ ;
-extern int strncmp (char *s1, char *s2, size_t n) /*@*/ ;
-extern size_t strxfrm (/*@out@*/ /*@null@*/ char *s1, char *s2, size_t n)
+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 */
-extern /*@null@*/ void *memchr (void *s, int c, size_t n) /*@*/ ;
+/*@null@*/ void *memchr (void *s, int c, size_t n) /*@*/ ;
# ifdef STRICT
-extern /*@exposed@*/ /*@null@*/ char *
-strchr (char *s, char c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0 @*/ ;
+/*@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
-extern /*@exposed@*/ /*@null@*/ char *
- strchr ( char *s, int /*@alt char@*/ c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0; @*/ ;
+/*@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
-extern size_t strcspn (char *s1, char *s2) /*@*/ ;
-extern /*@null@*/ /*@exposed@*/ char *
+size_t strcspn (char *s1, char *s2) /*@*/ ;
+/*@null@*/ /*@exposed@*/ char *
strpbrk (/*@returned@*/ char *s, char *t) /*@*/ ;
# ifdef STRICT
-extern /*@null@*/ /*@exposed@*/ char *
- strrchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0 @*/ ;
+/*@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
-extern /*@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 @*/ ;
+/*@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
-extern size_t strspn (char *s, char *t) /*@*/ ;
+size_t strspn (char *s, char *t) /*@*/ ;
-extern /*@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 @*/ ;
+/*@null@*/ /*@exposed@*/ char *
+ strstr (/*@returned@*/ const char *s, const 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)@*/ ;
-extern /*@null@*/ /*@exposed@*/ char *
+/*@null@*/ /*@exposed@*/ char *
strtok (/*@returned@*/ /*@null@*/ char *s, char *t)
/*@modifies *s, internalState, errno@*/ ;
-extern void /*@alt void *@*/ memset (/*@out@*/ /*@returned@*/ void *s,
+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) @*/ ;
+ /*@modifies *s@*/ /*@requires maxSet(s) >= (n - 1) @*/ /*@ensures maxRead(s) >= (n - 1) @*/ ;
-extern /*@observer@*/ char *strerror (int errnum) /*@*/ ;
+/*@observer@*/ char *strerror (int errnum) /*@*/ ;
/*drl */
-extern size_t strlen (char *s) /*@*/ /*@ensures result == MaxRead(s); @*/;
+size_t strlen (char *s) /*@*/ /*@ensures result == maxRead(s); @*/;
/*
** time.h
int tm_isdst;
} ;
-extern clock_t clock (void) /*@modifies internalState@*/ ;
-extern double difftime (time_t time1, time_t time0) /*@*/ ;
-extern time_t mktime (struct tm *timeptr) /*@*/ ;
+clock_t clock (void) /*@modifies internalState@*/ ;
+double difftime (time_t time1, time_t time0) /*@*/ ;
+time_t mktime (struct tm *timeptr) /*@*/ ;
-extern time_t time (/*@null@*/ /*@out@*/ time_t *tp)
+time_t time (/*@null@*/ /*@out@*/ time_t *tp)
/*@modifies *tp@*/ ;
-extern /*@observer@*/ char *asctime (struct tm *timeptr)
- /*@modifies errno*/ /*@ensures MaxSet(result) == 25 /\ MaxRead(result) == 25; @*/ ;
+/*@observer@*/ char *asctime (struct tm *timeptr)
+ /*@modifies errno*/ /*@ensures maxSet(result) == 25 /\ maxRead(result) == 25; @*/ ;
-extern /*@observer@*/ char *ctime (time_t *tp) /*@*/
- /*@ensures MaxSet(result) == 25 /\ MaxRead(result) == 25; @*/;
+/*@observer@*/ char *ctime (time_t *tp) /*@*/
+ /*@ensures maxSet(result) == 25 /\ maxRead(result) == 25; @*/;
-extern /*@null@*/ /*@observer@*/ struct tm *gmtime (time_t *tp) /*@*/ ;
+/*@null@*/ /*@observer@*/ struct tm *gmtime (time_t *tp) /*@*/ ;
-extern /*@null@*/ /*@observer@*/ struct tm *localtime (time_t *tp)
+/*@null@*/ /*@observer@*/ struct tm *localtime (time_t *tp)
/*@modifies errno@*/ ;
-extern size_t strftime (/*@out@*/ char *s, size_t smax,
+size_t strftime (/*@out@*/ char *s, size_t smax,
char *fmt, struct tm *timeptr)
/*@modifies *s@*/ ;
/*
-** inttypes.h
+** ISO c99: 7.18 Integer types <stdint.h>
+*/
+
+/*
+** These types are OPTIONAL. Provide warnings on use.
*/
-typedef char int8_t;
-typedef short int int16_t;
-typedef int int32_t;
-typedef unsigned char u_int8_t;
-typedef unsigned short int u_int16_t;
-typedef unsigned int u_int32_t;
+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@*/
+
+/*drl 3/5/2003
+ added the __func__ identifier from C99
+ This won't follow the same semantics as
+ __func__ in C99
+
+ FWIW C99 says that __func__ should have the value of the
+ lexically enclosing function
+ e.g. in the function foo __func__ == "foo"
+ in bar __func__ == "bar"
+
+ We're just having the value be constant here and picking
+ an arbitary value.
+*/
+static const char _ _func_ _[] = "function-name";
+
+
+/* drl 3/5/2003
+ added limited supported for _Bool */
+
+/*__Bool shouled really be a basic type but edited the grammar and ripping
+ apart the rest of Splint would probably break too much stuff...
+*/
+
+typedef /*@unsignedintegraltype@*/ _Bool;
+
+/*support stdbool.h */
+
+#define bool _Bool
+
+#define true 1
+
+#define false 0
+
+#define __bool_true_false_are_defined 1
andersk / splint.git / blobdiff