X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/d1eb0f0ff3093be5a50dfddab2d70e8bc7e7fff5..99f5508d3fb3b5902083a6d043f251d21b2cf01c:/lib/ansi.h diff --git a/lib/ansi.h b/lib/ansi.h index 29c1964..524356c 100644 --- a/lib/ansi.h +++ b/lib/ansi.h @@ -1,5 +1,5 @@ /* -** ansi.h --- LCLint Standard C Library +** standard.h --- ISO C99 Standard Library for Splint. ** ** Process with -DSTRICT to get strict library. */ @@ -17,9 +17,9 @@ /*@constant int EILSEQ;@*/ # ifdef STRICT -/*@checkedstrict@*/ extern int errno; +/*@checkedstrict@*/ int errno; # else -/*@unchecked@*/ extern int errno; +/*@unchecked@*/ int errno; # endif /* @@ -47,10 +47,10 @@ typedef /*@abstract@*/ mbstate_t; /*@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 @@ -60,33 +60,37 @@ extern /*@falseexit@*/ void assert (/*@sef@*/ lltX_bool /*@alt int@*/ e) */ # 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 /* @@ -122,10 +126,10 @@ struct lconv /*@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 @@ -136,37 +140,37 @@ extern struct lconv *localeconv (void) /*@*/ ; ** 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 @@ -192,41 +196,167 @@ extern struct lconv *localeconv (void) /*@*/ ; /* ** 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 @@ -236,50 +366,50 @@ double fmod (double x, double y) /*@*/ ; # 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 @@ -289,8 +419,8 @@ extern long double tanhl (long double x) /*@*/ ; 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 @@ -314,10 +444,10 @@ typedef /*@integraltype@*/ sig_atomic_t; ** 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 @@ -325,8 +455,8 @@ extern /*@mayexit@*/ int raise (int sig) ; 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 @@ -339,11 +469,12 @@ extern void va_end (va_list va) /*@modifies va;@*/ ; 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; @*/ @@ -367,74 +498,90 @@ typedef /*@abstract@*/ /*@mutable@*/ void *fpos_t; /*@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) @@ -449,116 +596,131 @@ int vsprintf (/*@out@*/ char *str, const char *format, va_list ap) /*@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 /* @@ -570,33 +732,33 @@ extern /*@null@*/ /*@only@*/ void * ** 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 { @@ -604,9 +766,9 @@ 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 { @@ -614,7 +776,7 @@ 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; @*/ @@ -626,160 +788,160 @@ extern ldiv_t ldiv (long num, long denom) /*@*/ ; /*@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@*/; @@ -792,68 +954,68 @@ typedef /*@integraltype@*/ wctype_t; 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); @*/ ; @@ -861,74 +1023,78 @@ extern void /*@alt void * @*/ 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 @@ -952,35 +1118,172 @@ struct tm 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 +*/ + +/* +** 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