lib/standard.h

   1 /*
   2 ** standard.h --- ISO C99 Standard Library for Splint.
   3 **
   4 ** Process with -DSTRICT to get strict library.
   5 */
   6
   7 /*@-nextlinemacros@*/
   8 /*@+allimponly@*/
   9 /*@+globsimpmodifiesnothing@*/
  10
  11 /*
  12 ** errno.h
  13 */
  14
  15 /*@constant int EDOM;@*/
  16 /*@constant int ERANGE;@*/
  17 /*@constant int EILSEQ;@*/
  18
  19 # ifdef STRICT
  20 /*@checkedstrict@*/ int errno;
  21 # else
  22 /*@unchecked@*/ int errno;
  23 # endif
  24
  25 /*
  26 ** types
  27 */
  28
  29 typedef /*@integraltype@*/ ptrdiff_t;
  30 typedef /*@unsignedintegraltype@*/ size_t;
  31 typedef /*@signedintegraltype@*/ ssize_t;
  32 typedef /*@integraltype@*/ wchar_t;
  33
  34 /*
  35 ** Added by Amendment 1 to ISO.
  36 */
  37
  38 typedef /*@integraltype@*/ wint_t;
  39 typedef /*@abstract@*/ mbstate_t;
  40
  41 /*@constant null anytype NULL = 0;@*/
  42
  43 /*
  44 ** assert.h
  45 */
  46
  47 /*@constant lltX_bool NDEBUG;@*/
  48
  49 # ifdef STRICT
  50 /*@falseexit@*/ void assert (/*@sef@*/ lltX_bool e)
  51   /*@*/ ;
  52 # else
  53 /*@falseexit@*/ void assert (/*@sef@*/ lltX_bool /*@alt int@*/ e)
  54   /*@*/ ;
  55 # endif
  56
  57
  58 /*
  59 ** ctype.h
  60 */
  61
  62 # ifdef STRICT
  63 lltX_bool isalnum (int c) /*@*/ ;
  64 lltX_bool isalpha (int c) /*@*/ ;
  65 lltX_bool iscntrl (int c) /*@*/ ;
  66 lltX_bool isdigit (int c) /*@*/ ;
  67 lltX_bool isgraph (int c) /*@*/ ;
  68 lltX_bool islower (int c) /*@*/ ;
  69 lltX_bool isprint (int c) /*@*/ ;
  70 lltX_bool ispunct (int c) /*@*/ ;
  71 lltX_bool isspace (int c) /*@*/ ;
  72 lltX_bool isupper (int c) /*@*/ ;
  73 lltX_bool isxdigit (int c) /*@*/ ;
  74 char tolower (int c) /*@*/ ;
  75 char toupper (int c) /*@*/ ;
  76 # else
  77 /*
  78 ** evans 2002-01-03: added alt char (was alt unsigned char)
  79 */
  80
  81 lltX_bool /*@alt int@*/ isalnum (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  82 lltX_bool /*@alt int@*/ isalpha (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  83 lltX_bool /*@alt int@*/ iscntrl (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  84 lltX_bool /*@alt int@*/ isdigit (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  85 lltX_bool /*@alt int@*/ isgraph (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  86 lltX_bool /*@alt int@*/ islower (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  87 lltX_bool /*@alt int@*/ isprint (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  88 lltX_bool /*@alt int@*/ ispunct (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  89 lltX_bool /*@alt int@*/ isspace (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  90 lltX_bool /*@alt int@*/ isupper (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  91 lltX_bool /*@alt int@*/ isxdigit (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  92 char /*@alt int@*/ tolower (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  93 char /*@alt int@*/ toupper (int /*@alt char, unsigned char@*/ c) /*@*/ ;
  94 # endif
  95
  96 /*
  97 ** locale.h
  98 */
  99
 100 struct lconv
 101 {
 102   char *decimal_point;
 103   char *thousands_sep;
 104   char *grouping;
 105   char *int_curr_symbol;
 106   char *currency_symbol;
 107   char *mon_decimal_point;
 108   char *mon_thousands_sep;
 109   char *mon_grouping;
 110   char *positive_sign;
 111   char *negative_sign;
 112   char int_frac_digits;
 113   char frac_digits;
 114   char p_cs_precedes;
 115   char p_sep_by_space;
 116   char n_cs_precedes;
 117   char n_sep_by_space;
 118   char p_sign_posn;
 119   char n_sign_posn;
 120 } ;
 121
 122 /*@constant int LC_ALL;@*/
 123 /*@constant int LC_COLLATE;@*/
 124 /*@constant int LC_CTYPE;@*/
 125 /*@constant int LC_MONETARY;@*/
 126 /*@constant int LC_NUMERIC;@*/
 127 /*@constant int LC_TIME;@*/
 128
 129 /*@observer@*/ /*@null@*/ char *setlocale (int category, /*@null@*/ char *locale)
 130    /*@modifies internalState, errno@*/ ;
 131
 132 struct lconv *localeconv (void) /*@*/ ;
 133
 134 /*
 135 ** float.h
 136 */
 137
 138 /*
 139 ** Note, these are defined by macros, but NOT necessarily
 140 ** constants.  They may be used as lvalues.
 141 */
 142
 143 /*@unchecked@*/ int    DBL_DIG;
 144 /*@unchecked@*/ double DBL_EPSILON;
 145 /*@unchecked@*/ int    DBL_MANT_DIG;
 146 /*@unchecked@*/ double DBL_MAX;
 147 /*@unchecked@*/ int    DBL_MAX_10_EXP;
 148 /*@unchecked@*/ int    DBL_MAX_EXP;
 149 /*@unchecked@*/ double DBL_MIN;
 150 /*@unchecked@*/ int    DBL_MIN_10_EXP;
 151 /*@unchecked@*/ int    DBL_MIN_EXP;
 152
 153 /*@unchecked@*/ int   FLT_DIG;
 154 /*@unchecked@*/ float FLT_EPSILON;
 155 /*@unchecked@*/ int   FLT_MANT_DIG;
 156 /*@unchecked@*/ float FLT_MAX;
 157 /*@unchecked@*/ int   FLT_MAX_10_EXP;
 158 /*@unchecked@*/ int   FLT_MAX_EXP;
 159 /*@unchecked@*/ float FLT_MIN;
 160 /*@unchecked@*/ int   FLT_MIN_10_EXP;
 161 /*@unchecked@*/ int   FLT_MIN_EXP;
 162 /*@constant            int   FLT_RADIX@*/
 163 /*@unchecked@*/ int   FLT_ROUNDS;
 164
 165 /*@unchecked@*/ int         LDBL_DIG;
 166 /*@unchecked@*/ long double LDBL_EPSILON;
 167 /*@unchecked@*/ int         LDBL_MANT_DIG;
 168 /*@unchecked@*/ long double LDBL_MAX;
 169 /*@unchecked@*/ int         LDBL_MAX_10_EXP;
 170 /*@unchecked@*/ int         LDBL_MAX_EXP;
 171 /*@unchecked@*/ long double LDBL_MIN;
 172 /*@unchecked@*/ int         LDBL_MIN_10_EXP;
 173 /*@unchecked@*/ int         LDBL_MIN_EXP;
 174
 175 /*
 176 ** limits.h
 177 */
 178
 179 /*@constant int CHAR_BIT; @*/
 180 /*@constant char CHAR_MAX; @*/
 181 /*@constant char CHAR_MIN; @*/
 182 /*@constant int INT_MAX; @*/
 183 /*@constant int INT_MIN; @*/
 184 /*@constant long int LONG_MAX; @*/
 185 /*@constant long int LONG_MIN; @*/
 186 /*@constant long int MB_LEN_MAX@*/
 187 /*@constant signed char SCHAR_MAX; @*/
 188 /*@constant signed char SCHAR_MIN; @*/
 189 /*@constant short SHRT_MAX; @*/
 190 /*@constant short SHRT_MIN; @*/
 191 /*@constant unsigned char UCHAR_MAX; @*/
 192 /*@constant unsigned char UCHAR_MIN; @*/
 193 /*@constant unsigned int UINT_MAX; @*/
 194 /*@constant unsigned long ULONG_MAX; @*/
 195 /*@constant unsigned short USHRT_MAX; @*/
 196
 197 /*
 198 ** math.h
 199 */
 200
 201 /*@constant double HUGE_VAL; @*/
 202
 203 /*
 204 ** math functions that may have a range error modify errno
 205 */
 206
 207 double sin (double x) /*@*/ ;
 208 double cos (double x) /*@*/ ;
 209 double tan (double x) /*@*/ ;
 210 double asin (double x) /*@modifies errno@*/ ;
 211 double acos (double x) /*@modifies errno@*/ ;
 212 double atan (double x) /*@*/ ;
 213 double atan2 (double y, double x) /*@*/ ;
 214 double sinh (double x) /*@*/ ;
 215 double cosh (double x) /*@modifies errno@*/ ;
 216 double tanh (double x) /*@*/ ;
 217
 218 double exp (double x) /*@modifies errno@*/ ;
 219 double ldexp (double x, int n) /*@modifies errno@*/ ;
 220 double frexp (double x, /*@out@*/ int *xp) /*@modifies *xp;@*/ ;
 221
 222 double log (double x) /*@modifies errno@*/ ;
 223 double log10 (double x) /*@modifies errno@*/ ;
 224
 225 double pow (double x, double y) /*@modifies errno@*/ ;
 226 double sqrt (double x) /*@modifies errno@*/ ;
 227
 228 double ceil (double x) /*@*/ ;
 229 double floor (double x) /*@*/ ;
 230 double fabs (double x) /*@*/ ;
 231
 232 double modf (double x, /*@out@*/ double *ip) /*@modifies *ip;@*/ ;
 233 double fmod (double x, double y) /*@*/ ;
 234
 235 /*
 236 ** These functions are optional in iso C.  An implementation does not
 237 ** have to provide them.  They are included in comments here, but
 238 ** are not required to be part of the standard library.
 239 */
 240
 241 # ifdef OPTIONAL_MATH
 242
 243 float acosf (float x) /*@modifies errno@*/ ;
 244 long double acosl (long double x) /*@modifies errno@*/ ;
 245 float asinf (float x)   /*@modifies errno@*/ ;
 246 long double asinl (long double x) /*@modifies errno@*/ ;
 247 float atanf (float x)   /*@*/ ;
 248 long double atanl (long double x) /*@*/ ;
 249 float atan2f (float y, float x) /*@*/ ;
 250 long double atan2l (long double y, long double x) /*@*/ ;
 251 float ceilf (float x)   /*@*/ ;
 252 long double ceill (long double x) /*@*/ ;
 253 float cosf (float x) /*@*/ ;
 254 long double cosl (long double x) /*@*/ ;
 255 float coshf (float x)   /*@modifies errno@*/ ;
 256 long double coshl (long double x) /*@modifies errno@*/ ;
 257 float expf (float x) /*@modifies errno@*/ ;
 258 long double expl (long double x) /*@modifies errno@*/;
 259 float fabsf (float x)   /*@*/ ;
 260 long double fabsl (long double x) /*@*/ ;
 261 float floorf (float x) /*@*/ ;
 262 long double floorl (long double x) /*@*/ ;
 263 float fmodf (float x, float y) /*@*/ ;
 264 long double fmodl (long double x, long double y)        /*@*/ ;
 265 float frexpf (float x, /*@out@*/ int *xp) /*@modifies *xp@*/;
 266 long double frexpl (long double x, /*@out@*/ int *xp) /*@modifies *xp@*/;
 267 float ldexpf (float x, int n) /*@modifies errno@*/ ;
 268 long double ldexpl (long double x, int n) /*@modifies errno@*/ ;
 269 float logf (float x) /*@modifies errno@*/ ;
 270 long double logl (long double x) /*@modifies errno@*/ ;
 271 float log10f (float x) /*@modifies errno@*/;
 272 long double log10l (long double x) /*@modifies errno@*/;
 273 float modff (float x, /*@out@*/ float *xp) /*@modifies *xp@*/ ;
 274 long double modfl (long double x, /*@out@*/ long double *xp) /*@modifies *xp@*/ ;
 275 float powf (float x, float y) /*@modifies errno@*/ ;
 276 long double powl (long double x, long double y) /*@modifies errno@*/ ;
 277 float sinf (float x) /*@*/ ;
 278 long double sinl (long double x)        /*@*/ ;
 279 float sinhf (float x) /*@*/ ;
 280 long double sinhl (long double x) /*@*/ ;
 281 float sqrtf (float x) /*@modifies errno@*/ ;
 282 long double sqrtl (long double x) /*@modifies errno@*/ ;
 283 float tanf (float x) /*@*/ ;
 284 long double tanl (long double x)        /*@*/ ;
 285 float tanhf (float x) /*@*/ ;
 286 long double tanhl (long double x) /*@*/ ;
 287
 288 # endif
 289
 290 /*
 291 ** setjmp.h
 292 */
 293
 294 typedef /*@abstract@*/ /*@mutable@*/ void *jmp_buf;
 295
 296 int setjmp (/*@out@*/ jmp_buf env) /*@modifies env;@*/ ;
 297 /*@mayexit@*/ void longjmp (jmp_buf env, int val) /*@*/ ;
 298
 299 /*
 300 ** signal.h
 301 */
 302
 303 /*@constant int SIGABRT; @*/
 304 /*@constant int SIGFPE; @*/
 305 /*@constant int SIGILL; @*/
 306 /*@constant int SIGINT; @*/
 307 /*@constant int SIGSEGV; @*/
 308 /*@constant int SIGTERM; @*/
 309
 310 typedef /*@integraltype@*/ sig_atomic_t;
 311
 312 /*@constant void (*SIG_DFL)(int); @*/
 313 /*@constant void (*SIG_ERR)(int); @*/
 314 /*@constant void (*SIG_IGN)(int); @*/
 315
 316 /*
 317 ** signal takes an int, and a function takes int returns void, and
 318 ** returns the function (or NULL if unsuccessful).
 319 */
 320
 321 /*@null@*/ void (*signal (int sig, /*@null@*/ void (*func)(int))) (int)
 322    /*@modifies internalState, errno;@*/ ;
 323
 324 /*@mayexit@*/ int raise (int sig) ;
 325
 326 /*
 327 ** stdarg.h
 328 */
 329
 330 typedef /*@abstract@*/ /*@mutable@*/ void *va_list;
 331
 332 void va_start (/*@out@*/ va_list ap, ...) /*@modifies ap;@*/ ;
 333 void va_end (va_list va) /*@modifies va;@*/ ;
 334
 335 /*
 336 ** va_arg is builtin
 337 */
 338
 339 /*
 340 ** stdio.h
 341 */
 342
 343 typedef /*@abstract@*/ /*@mutable@*/ void *FILE;
 344 typedef /*@abstract@*/ /*@mutable@*/ void *fpos_t;
 345
 346 /*@constant size_t _IOFBF; @*/
 347 /*@constant size_t _IOLBF; @*/
 348 /*@constant size_t _IONBF; @*/
 349
 350 /*@constant size_t BUFSIZ; @*/ /* evans 2002-02-27 change suggested by Walter Briscoe */
 351
 352 /*@constant int EOF; @*/
 353
 354 /*@constant int FOPEN_MAX; @*/
 355 /*@constant int FILENAME_MAX; @*/
 356
 357 /*@constant int L_tmpnam; @*/
 358
 359 /*@constant int SEEK_CUR; @*/
 360 /*@constant int SEEK_END; @*/
 361 /*@constant int SEEK_SET; @*/
 362
 363 /*@constant int TMP_MAX; @*/
 364
 365 # ifdef STRICT
 366 /*@checked@*/ FILE *stderr;
 367 /*@checked@*/ FILE *stdin;
 368 /*@checked@*/ FILE *stdout;
 369 # else
 370 /*@unchecked@*/ FILE *stderr;
 371 /*@unchecked@*/ FILE *stdin;
 372 /*@unchecked@*/ FILE *stdout;
 373 # endif
 374
 375 int remove (char *filename) /*@modifies fileSystem, errno@*/ ;
 376 int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ;
 377
 378 /*@dependent@*/ /*@null@*/ FILE *tmpfile (void)
 379    /*@modifies fileSystem, errno@*/ ;
 380
 381 /*@observer@*/ char *
 382   tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s)
 383   /*@modifies *s, internalState@*/ ;
 384
 385 int fclose (FILE *stream)
 386    /*@modifies *stream, errno, fileSystem;@*/ ;
 387
 388 int fflush (/*@null@*/ FILE *stream)
 389    /*@modifies *stream, errno, fileSystem;@*/ ;
 390
 391 /*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode)
 392    /*@modifies fileSystem@*/ ;
 393
 394 /*@dependent@*/ /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream)
 395   /*@modifies *stream, fileSystem, errno@*/ ;
 396
 397 extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf)
 398      /*@modifies fileSystem, *stream, *buf@*/ ;
 399
 400 extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf,
 401                     int mode, size_t size)
 402      /*@modifies fileSystem, *stream, *buf@*/ ;
 403
 404 # ifdef STRICT
 405 /*@printflike@*/
 406 int fprintf (FILE *stream, char *format, ...)
 407    /*@modifies fileSystem, *stream@*/ ;
 408 # else
 409 /*@printflike@*/
 410 int /*@alt void@*/ fprintf (FILE *stream, char *format, ...)
 411    /*@modifies fileSystem, *stream@*/ ;
 412 # endif
 413
 414 /*@scanflike@*/
 415 int fscanf (FILE *stream, char *format, ...)
 416    /*@modifies fileSystem, *stream@*/ ;
 417
 418 # ifdef STRICT
 419 /*@printflike@*/
 420 int printf (char *format, ...)
 421    /*@globals stdout@*/
 422    /*@modifies fileSystem, *stdout@*/ ;
 423 # else
 424 /*@printflike@*/
 425 int /*@alt void@*/ printf (char *format, ...)
 426    /*@globals stdout@*/
 427    /*@modifies fileSystem, *stdout@*/ ;
 428 # endif
 429
 430 /*@scanflike@*/
 431 int scanf(char *format, ...)
 432    /*@globals stdin@*/
 433    /*@modifies fileSystem, *stdin@*/ ;
 434
 435 # ifdef STRICT
 436 /*@printflike@*/
 437 int sprintf (/*@out@*/ char *s, char *format, ...)
 438    /*@modifies *s@*/ ;
 439 # else
 440 /*@printflike@*/
 441 int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...)
 442    /*@modifies *s@*/ ;
 443 # endif
 444
 445 /*@scanflike@*/
 446 int sscanf (/*@out@*/ char *s, char *format, ...) /*@*/ ;
 447    /* modifies extra arguments */
 448
 449 int vprintf (const char *format, va_list arg)
 450    /*@globals stdout@*/
 451    /*@modifies fileSystem, *stdout@*/ ;
 452
 453 int vfprintf (FILE *stream, char *format, va_list arg)
 454    /*@modifies fileSystem, *stream, arg, errno@*/ ;
 455
 456 int vsprintf (/*@out@*/ char *str, const char *format, va_list ap)
 457      /*@warn bufferoverflowhigh "Use vsnprintf instead"@*/
 458      /*@modifies str@*/ ;
 459
 460 int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap)
 461      /*@requires maxSet(str) >= size@*/
 462      /*@modifies str@*/ ;
 463
 464 int fgetc (FILE *stream)
 465    /*@modifies fileSystem, *stream, errno@*/ ;
 466
 467 /*@null@*/ char *
 468   fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream)
 469      /*@modifies fileSystem, *s, *stream, errno@*/
 470      /*@requires maxSet(s) >= (n -1); @*/
 471      /*@ensures maxRead(s) <= (n -1) /\ maxRead(s) >= 0; @*/
 472      ;
 473
 474 int fputc (int /*@alt char@*/ c, FILE *stream)
 475   /*:errorcode EOF:*/
 476   /*@modifies fileSystem, *stream, errno@*/ ;
 477
 478 int fputs (char *s, FILE *stream)
 479   /*@modifies fileSystem, *stream@*/ ;
 480
 481 /* note use of sef --- stream may be evaluated more than once */
 482 int getc (/*@sef@*/ FILE *stream)
 483   /*@modifies fileSystem, *stream@*/ ;
 484
 485 int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/ ;
 486
 487 /*@null@*/ char *gets (/*@out@*/ char *s)
 488    /*@warn bufferoverflowhigh
 489            "Use of gets leads to a buffer overflow vulnerability.  Use fgets instead"@*/
 490    /*@globals stdin@*/ /*@modifies fileSystem, *s, *stdin, errno@*/ ;
 491
 492 int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
 493    /*:errorcode EOF:*/
 494    /*@modifies fileSystem, *stream;@*/ ;
 495
 496 int putchar (int /*@alt char@*/ c)
 497    /*:errorcode EOF:*/
 498    /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ;
 499
 500 int puts (const char *s)
 501    /*:errorcode EOF:*/
 502    /*@globals stdout@*/
 503    /*@modifies fileSystem, *stdout@*/ ;
 504
 505 int ungetc (int /*@alt char@*/ c, FILE *stream)
 506   /*@modifies fileSystem, *stream, errno@*/ ;
 507
 508 size_t
 509   fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream)
 510   /*@modifies fileSystem, *ptr, *stream, errno@*/ ;
 511
 512 size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream)
 513   /*@modifies fileSystem, *stream, errno@*/ ;
 514
 515 int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos)
 516   /*@modifies *pos, errno@*/ ;
 517
 518 int fseek (FILE *stream, long int offset, int whence)
 519    /*:errorcode -1:*/
 520    /*@modifies fileSystem, *stream, errno@*/ ;
 521
 522 int fsetpos (FILE *stream, fpos_t *pos)
 523    /*@modifies fileSystem, *stream, errno@*/ ;
 524
 525 long int ftell(FILE *stream)
 526    /*:errorcode -1:*/ /*@modifies errno*/ ;
 527
 528 void rewind (FILE *stream) /*@modifies *stream@*/ ;
 529 void clearerr (FILE *stream) /*@modifies *stream@*/ ;
 530
 531 int feof (FILE *stream) /*@modifies errno@*/ ;
 532
 533 int ferror (FILE *stream) /*@modifies errno@*/ ;
 534
 535 void perror (/*@null@*/ char *s)
 536    /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ;
 537
 538 /*
 539 ** stdlib.h
 540 */
 541
 542 double atof (char *s) /*@*/ ;
 543 int atoi (char *s) /*@*/ ;
 544 long int atol (char *s) /*@*/ ;
 545
 546 double strtod (char *s, /*@null@*/ /*@out@*/ char **endp)
 547   /*@modifies *endp, errno@*/ ;
 548
 549 long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
 550   /*@modifies *endp, errno@*/ ;
 551
 552 unsigned long
 553   strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
 554   /*@modifies *endp, errno@*/ ;
 555
 556 /*@constant int RAND_MAX; @*/
 557 int rand (void) /*@modifies internalState@*/ ;
 558 void srand (unsigned int seed) /*@modifies internalState@*/ ;
 559
 560 /*
 561   drl
 562   changed 12/29/2000
 563 */
 564
 565 /*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/
 566      /*@ensures maxSet(result) == (nobj - 1); @*/ ;
 567 /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@*/
 568      /*@ensures maxSet(result) == (size - 1); @*/ ;
 569
 570 /*end drl changed */
 571
 572 /* 11 June 1997: removed out on return value */
 573
 574 # if 0
 575 /*@null@*/ /*@only@*/ void *
 576    realloc (/*@null@*/ /*@only@*/ /*@special@*/ void *p,
 577             size_t size) /*@releases p@*/ /*@modifies *p@*/
 578      /*@ensures maxSet(result) == (size - 1) @*/;
 579 # endif
 580
 581 /*
 582 ** LCLint annotations cannot fully describe realloc.  The semantics we
 583 ** want are:
 584 **    realloc returns null: ownership of parameter is not changed
 585 **    realloc returns non-null: ownership of parameter is transferred to return value
 586 **
 587 ** Otherwise, storage is in the same state before and after the call.
 588 */
 589
 590 /*@null@*/ /*@only@*/ void *
 591    realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size)
 592      /*@modifies *p@*/ /*@ensures maxSet(result) >= (size - 1) @*/;
 593
 594 void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies p@*/ ;
 595
 596 /*@constant int EXIT_FAILURE; @*/
 597 /*@constant int EXIT_SUCCESS; @*/
 598
 599 /*@exits@*/ void abort (void) /*@*/ ;
 600 /*@exits@*/ void exit (int status) /*@*/ ;
 601 int atexit (void (*func)(void)) /*@modifies internalState@*/ ;
 602
 603 /*@observer@*/ /*@null@*/ char *getenv (char *name) /*@*/ ;
 604
 605 int system (/*@null@*/ char *s) /*@modifies fileSystem@*/ ;
 606
 607 /*@null@*/ /*@dependent@*/ void *
 608   bsearch (void *key, void *base,
 609            size_t n, size_t size,
 610            int (*compar)(void *, void *)) /*@*/ ;
 611
 612 void qsort (void *base, size_t n, size_t size,
 613                    int (*compar)(void *, void *))
 614    /*@modifies *base, errno@*/ ;
 615
 616 int abs (int n) /*@*/ ;
 617
 618 typedef /*@concrete@*/ struct
 619 {
 620   int quot;
 621   int rem;
 622 } div_t ;
 623
 624 div_t div (int num, int denom) /*@*/ ;
 625
 626 long int labs (long int n) /*@*/ ;
 627
 628 typedef /*@concrete@*/ struct
 629 {
 630   long int quot;
 631   long int rem;
 632 } ldiv_t ;
 633
 634 ldiv_t ldiv (long num, long denom) /*@*/ ;
 635
 636 /*@constant size_t MB_CUR_MAX; @*/
 637
 638 /*
 639 ** wchar_t and wint_t functions added by Amendment 1 to ISO.
 640 */
 641
 642 /*@constant int WCHAR_MAX@*/
 643 /*@constant int WCHAR_MIN@*/
 644 /*@constant wint_t WEOF@*/
 645
 646 wint_t btowc (int c) /*@*/ ;
 647
 648 wint_t fgetwc (FILE *fp)        /*@modifies fileSystem, *fp*/ ;
 649
 650 /*@null@*/ wchar_t *fgetws (/*@returned@*/ wchar_t *s, int n, FILE *stream)
 651    /*@modifies fileSystem, *s, *stream@*/;
 652
 653 wint_t fputwc (wchar_t c, FILE *stream)
 654    /*@modifies fileSystem, *stream@*/;
 655
 656 int fputws (const wchar_t *s, FILE *stream)
 657    /*@modifies fileSystem, *stream@*/ ;
 658
 659 int fwide (FILE *stream, int mode) /*@*/ ;
 660    /* does not modify the stream */
 661
 662 /*@printflike@*/ int fwprintf (FILE *stream, const wchar_t *format, ...)
 663     /*@modifies *stream, fileSystem@*/ ;
 664
 665 /*@scanflike@*/ int fwscanf (FILE *stream, const wchar_t *format, ...)
 666         /*@modifies *stream, fileSystem@*/ ;
 667
 668 /* note use of sef --- stream may be evaluated more than once */
 669 wint_t getwc (/*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ;
 670
 671 wint_t getwchar (void) /*@modifies fileSystem, *stdin@*/;
 672
 673 size_t mbrlen (const char *s, size_t n, /*@null@*/ mbstate_t *ps) /*@*/ ;
 674
 675 size_t mbrtowc (/*@null@*/ wchar_t *pwc, const char *s, size_t n,
 676                        /*@null@*/ mbstate_t *ps)
 677    /*@modifies *pwc@*/ ;
 678
 679 int mbsinit (/*@null@*/ const mbstate_t *ps) /*@*/ ;
 680
 681 size_t mbsrtowcs (/*@null@*/ wchar_t *dst, const char **src, size_t len,
 682                          /*@null@*/ mbstate_t *ps)
 683    /*@modifies *dst@*/ ;
 684
 685 /* note use of sef --- stream may be evaluated more than once */
 686 wint_t putwc (wchar_t c, /*@sef@*/ FILE *stream)        /*@modifies fileSystem, *stream@*/ ;
 687
 688 wint_t putwchar (wchar_t c) /*@modifies fileSystem, *stdout@*/ ;
 689
 690 /*@printflike@*/ int swprintf (wchar_t *s, size_t n, const wchar_t *format, ...)
 691    /*@modifies *s@*/ ;
 692
 693 /*@scanflike@*/ int swscanf (const wchar_t *s, const wchar_t *format, ...)
 694    /*@modifies *stdin@*/ ;
 695
 696 wint_t ungetwc (wint_t c, FILE *stream) /*@modifies fileSystem, *stream@*/ ;
 697
 698 int vfwprintf (FILE *stream, const wchar_t *format, va_list arg)
 699    /*@modifies fileSystem, *stream@*/ ;
 700
 701 int vswprintf (wchar_t *s, size_t n, const wchar_t *format, va_list arg)
 702    /*@modifies *s@*/ ;
 703
 704 int vwprintf (const wchar_t *format, va_list arg)
 705    /*@modifies fileSystem, *stdout@*/ ;
 706
 707 size_t wcrtomb (/*@null@*/ /*@out@*/ char *s, wchar_t wc, /*@null@*/ mbstate_t *ps)
 708    /*@modifies *s@*/;
 709
 710 void /*@alt wchar_t *@*/
 711   wcscat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2)
 712   /*@modifies *s1@*/ ;
 713
 714 /*@exposed@*/ /*@null@*/ wchar_t *
 715   wcschr (/*@returned@*/ const wchar_t *s, wchar_t c)
 716   /*@*/ ;
 717
 718 int wcscmp (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
 719
 720 int wcscoll (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
 721
 722 void /*@alt wchar_t *@*/
 723   wcscpy (/*@unique@*/ /*@out@*/ /*@returned@*/ wchar_t *s1, const wchar_t *s2)
 724   /*@modifies *s1@*/ ;
 725
 726 size_t wcscspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
 727
 728 size_t wcsftime (/*@out@*/ wchar_t *s, size_t maxsize, const wchar_t *format,
 729                         const struct tm *timeptr)
 730    /*@modifies *s@*/ ;
 731
 732 size_t wcslen (const wchar_t *s) /*@*/ ;
 733
 734 void /*@alt wchar_t *@*/
 735   wcsncat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
 736            size_t n)
 737   /*@modifies *s1@*/ ;
 738
 739 int wcsncmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
 740
 741 void /*@alt wchar_t *@*/
 742   wcsncpy (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
 743            size_t n)
 744    /*@modifies *s1@*/ ;
 745
 746 /*@null@*/ wchar_t *
 747   wcspbrk (/*@returned@*/ const wchar_t *s1, const wchar_t *s2)
 748   /*@*/ ;
 749
 750 /*@null@*/ wchar_t *
 751   wcsrchr (/*@returned@*/ const wchar_t *s, wchar_t c)
 752   /*@*/ ;
 753
 754 size_t
 755   wcsrtombs (/*@null@*/ char *dst, const wchar_t **src, size_t len,
 756              /*@null@*/ mbstate_t *ps)
 757   /*@modifies *src@*/ ;
 758
 759 size_t wcsspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
 760
 761 /*@null@*/ wchar_t *wcsstr (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
 762
 763 double wcstod (const wchar_t *nptr, /*@null@*/ wchar_t **endptr)
 764    /*@modifies *endptr@*/ ;
 765
 766 /*@null@*/ wchar_t *
 767   wcstok (/*@null@*/ wchar_t *s1, const wchar_t *s2, wchar_t **ptr)
 768   /*@modifies *ptr@*/;
 769
 770 long wcstol (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
 771    /*@modifies *endptr@*/;
 772
 773 unsigned long
 774   wcstoul (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
 775   /*@modifies *endptr@*/;
 776
 777 size_t
 778   wcsxfrm (/*@null@*/ wchar_t *s1, const wchar_t *s2, size_t n)
 779   /*@modifies *s1@*/;
 780
 781 int wctob (wint_t c) /*@*/;
 782
 783 /*@null@*/ wchar_t *wmemchr (const wchar_t *s, wchar_t c, size_t n) /*@*/ ;
 784
 785 int wmemcmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
 786
 787 wchar_t *wmemcpy (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
 788    /*@modifies *s1@*/;
 789
 790 wchar_t *wmemmove (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
 791    /*@modifies *s1@*/;
 792
 793 wchar_t *wmemset (/*@returned@*/ wchar_t *s, wchar_t c, size_t n)
 794    /*@modifies *s@*/;
 795
 796 /*@printflike@*/ int wprintf (const wchar_t *format, ...)
 797    /*@globals stdout@*/ /*@modifies errno, *stdout@*/;
 798
 799 /*@scanflike@*/ int
 800   wscanf (const wchar_t *format, ...)
 801   /*@globals stdin@*/ /*@modifies errno, *stdin@*/;
 802
 803 /*
 804 ** wctype.h (added by Amendment 1)
 805 */
 806
 807 /* Warning: not sure about these (maybe abstract?): */
 808 typedef /*@integraltype@*/ wctype_t;
 809 typedef /*@integraltype@*/ wctrans_t;
 810
 811 # ifdef STRICT
 812 lltX_bool iswalnum (wint_t c) /*@*/ ;
 813 lltX_bool iswalpha (wint_t c) /*@*/ ;
 814 lltX_bool iswcntrl (wint_t c) /*@*/ ;
 815 lltX_bool iswctype (wint_t c, wctype_t ctg) /*@*/ ;
 816 lltX_bool iswdigit (wint_t c) /*@*/ ;
 817 lltX_bool iswgraph (wint_t c) /*@*/ ;
 818 lltX_bool iswlower (wint_t c) /*@*/ ;
 819 lltX_bool iswprint (wint_t c) /*@*/ ;
 820 lltX_bool iswpunct (wint_t c) /*@*/ ;
 821 lltX_bool iswspace (wint_t c) /*@*/ ;
 822 lltX_bool iswupper (wint_t c) /*@*/ ;
 823 lltX_bool iswxdigit (wint_t c) /*@*/ ;
 824
 825 wint_t towctrans (wint_t c, wctrans_t ctg) /*@*/ ;
 826 wint_t towlower (wint_t c) /*@*/ ;
 827 wint_t towupper (wint_t c) /*@*/ ;
 828 # else
 829 lltX_bool /*@alt int@*/ iswalnum (wint_t c) /*@*/ ;
 830 lltX_bool /*@alt int@*/ iswalpha (wint_t c) /*@*/ ;
 831 lltX_bool /*@alt int@*/ iswcntrl (wint_t c) /*@*/ ;
 832 lltX_bool /*@alt int@*/ iswctype (wint_t c, wctype_t ctg) /*@*/ ;
 833 lltX_bool /*@alt int@*/ iswdigit (wint_t c) /*@*/ ;
 834 lltX_bool /*@alt int@*/ iswgraph (wint_t c) /*@*/ ;
 835 lltX_bool /*@alt int@*/ iswlower (wint_t c) /*@*/ ;
 836 lltX_bool /*@alt int@*/ iswprint (wint_t c) /*@*/ ;
 837 lltX_bool /*@alt int@*/ iswpunct (wint_t c) /*@*/ ;
 838 lltX_bool /*@alt int@*/ iswspace (wint_t c) /*@*/ ;
 839 lltX_bool /*@alt int@*/ iswupper (wint_t c) /*@*/ ;
 840 lltX_bool /*@alt int@*/ iswxdigit (wint_t c) /*@*/ ;
 841
 842 wint_t /*@alt int@*/ towctrans (wint_t c, wctrans_t ctg)        /*@*/ ;
 843 wint_t /*@alt int@*/ towlower (wint_t c)        /*@*/ ;
 844 wint_t /*@alt int@*/ towupper (wint_t c)        /*@*/ ;
 845 # endif
 846
 847 wctrans_t wctrans (const char *property)        /*@*/ ;
 848 wctype_t wctype (const char *property) /*@*/ ;
 849
 850 int mblen (char *s, size_t n) /*@*/ ;
 851 int mbtowc (/*@null@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n)
 852    /*@modifies *pwc@*/ ;
 853 int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar)
 854    /*@modifies *s@*/ ;
 855 size_t mbstowcs (/*@out@*/ wchar_t *pwcs, char *s, size_t n)
 856   /*@modifies *pwcs@*/ ;
 857 size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n)
 858   /*@modifies *s@*/ ;
 859
 860 /*
 861 ** string.h
 862 */
 863
 864 void /*@alt void * @*/
 865   memcpy (/*@unique@*/ /*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
 866   /*@modifies *s1@*/
 867      /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
 868      ;
 869
 870 void /*@alt void * @*/
 871   memmove (/*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
 872   /*@modifies *s1@*/
 873   /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
 874    ;
 875
 876
 877   /* drl
 878      modifed  12/29/2000
 879   */
 880
 881 void /*@alt char * @*/
 882   strcpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2)
 883      /*@modifies *s1@*/
 884      /*@requires maxSet(s1) >= maxRead(s2) @*/
 885      /*@ensures maxRead(s1) == maxRead (s2) /\ maxRead(result) == maxRead(s2) /\ maxSet(result) == maxSet(s1); @*/;
 886
 887 void /*@alt char * @*/
 888   strncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2, size_t n)
 889      /*@modifies *s1@*/
 890      /*@requires maxSet(s1) >= ( n - 1 ); @*/
 891      /*@ensures maxRead (s2) >= maxRead(s1) /\ maxRead (s1) <= n; @*/ ;
 892
 893 void /*@alt char * @*/
 894   strcat (/*@unique@*/ /*@returned@*/ char *s1, char *s2)
 895      /*@modifies *s1@*/ /*@requires maxSet(s1) >= (maxRead(s1) + maxRead(s2) );@*/
 896      /*@ensures maxRead(result) == (maxRead(s1) + maxRead(s2) );@*/;
 897
 898 void /*@alt char * @*/
 899   strncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, size_t n)
 900      /*@modifies *s1@*/
 901      /*@requires maxSet(s1) >= ( maxRead(s1) + n); @*/
 902       /*@ensures maxRead(s1) >= (maxRead(s1) + n); @*/;
 903
 904      /*drl end*/
 905
 906 int memcmp (void *s1, void *s2, size_t n) /*@*/ ;
 907 int strcmp (char *s1, char *s2) /*@*/ ;
 908 int strcoll (char *s1, char *s2) /*@*/ ;
 909 int strncmp (char *s1, char *s2, size_t n) /*@*/ ;
 910 size_t strxfrm (/*@out@*/ /*@null@*/ char *s1, char *s2, size_t n)
 911   /*@modifies *s1@*/ ;  /* s1 may be null only if n == 0 */
 912
 913 /*@null@*/ void *memchr (void *s, int c, size_t n) /*@*/ ;
 914
 915 # ifdef STRICT
 916 /*@exposed@*/ /*@null@*/ char *
 917 strchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
 918 # else
 919 /*@exposed@*/ /*@null@*/ char *
 920   strchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0; @*/ ;
 921 # endif
 922
 923 size_t strcspn (char *s1, char *s2) /*@*/ ;
 924 /*@null@*/ /*@exposed@*/ char *
 925   strpbrk (/*@returned@*/ char *s, char *t) /*@*/ ;
 926
 927 # ifdef STRICT
 928 /*@null@*/ /*@exposed@*/ char *
 929   strrchr (/*@returned@*/ char *s, char c) /*@*/  /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
 930 # else
 931 /*@null@*/ /*@exposed@*/ char *
 932   strrchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/  /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
 933 # endif
 934
 935 size_t strspn (char *s, char *t) /*@*/ ;
 936
 937 /*@null@*/ /*@exposed@*/  char *
 938   strstr (/*@returned@*/ const char *s, const char *t) /*@*/
 939        /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 /\ maxRead(result) >= maxRead(t) /\ maxSet(result) >= maxRead(t)@*/ ;
 940
 941 /*@null@*/ /*@exposed@*/ char *
 942   strtok (/*@returned@*/ /*@null@*/ char *s, char *t)
 943   /*@modifies *s, internalState, errno@*/ ;
 944
 945 void /*@alt void *@*/ memset (/*@out@*/ /*@returned@*/ void *s,
 946                                      int c, size_t n)
 947      /*@modifies *s@*/ /*@requires maxSet(s) >= (n - 1) @*/ /*@ensures maxRead(s) >= (n - 1) @*/ ;
 948
 949 /*@observer@*/ char *strerror (int errnum) /*@*/ ;
 950
 951 /*drl */
 952 size_t strlen (char *s) /*@*/ /*@ensures result == maxRead(s); @*/;
 953
 954 /*
 955 ** time.h
 956 */
 957
 958 /*@constant int CLOCKS_PER_SEC;@*/
 959
 960 typedef /*@integraltype@*/ clock_t;
 961 typedef /*@integraltype@*/ time_t;
 962
 963 struct tm
 964   {
 965     int tm_sec;
 966     int tm_min;
 967     int tm_hour;
 968     int tm_mday;
 969     int tm_mon;
 970     int tm_year;
 971     int tm_wday;
 972     int tm_yday;
 973     int tm_isdst;
 974   } ;
 975
 976 clock_t clock (void) /*@modifies internalState@*/ ;
 977 double difftime (time_t time1, time_t time0) /*@*/ ;
 978 time_t mktime (struct tm *timeptr) /*@*/ ;
 979
 980 time_t time (/*@null@*/ /*@out@*/ time_t *tp)
 981   /*@modifies *tp@*/ ;
 982
 983 /*@observer@*/ char *asctime (struct tm *timeptr)
 984   /*@modifies errno*/ /*@ensures maxSet(result) == 25 /\  maxRead(result) == 25; @*/ ;
 985
 986 /*@observer@*/ char *ctime (time_t *tp) /*@*/
 987      /*@ensures maxSet(result) == 25 /\  maxRead(result) == 25; @*/;
 988
 989 /*@null@*/ /*@observer@*/ struct tm *gmtime (time_t *tp) /*@*/ ;
 990
 991 /*@null@*/ /*@observer@*/ struct tm *localtime (time_t *tp)
 992   /*@modifies errno@*/ ;
 993
 994 size_t strftime (/*@out@*/ char *s, size_t smax,
 995                         char *fmt, struct tm *timeptr)
 996   /*@modifies *s@*/ ;
 997
 998 /*
 999 ** ISO c99: 7.18 Integer types <stdint.h>
1000 */
1001
1002 /*
1003 ** These types are OPTIONAL.  Provide warnings on use.
1004 */
1005
1006 typedef /*@integraltype@*/ int8_t
1007    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least8_t instead."@*/ ;
1008
1009 typedef /*@integraltype@*/ int16_t
1010    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least16_t instead."@*/ ;
1011
1012 typedef /*@integraltype@*/ int32_t
1013    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least32_t instead."@*/ ;
1014
1015 typedef /*@integraltype@*/ int64_t
1016    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least64_t instead."@*/ ;
1017
1018 typedef /*@unsignedintegraltype@*/ uint8_t
1019    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least8_t instead."@*/ ;
1020
1021 typedef /*@unsignedintegraltype@*/ uint16_t
1022    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least16_t instead."@*/ ;
1023
1024 typedef /*@unsignedintegraltype@*/ uint32_t
1025    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least32_t instead."@*/ ;
1026
1027 typedef /*@unsignedintegraltype@*/ uint64_t
1028    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least64_t instead."@*/ ;
1029
1030 typedef /*@integraltype@*/ int_least8_t;
1031 typedef /*@integraltype@*/ int_least16_t;
1032 typedef /*@integraltype@*/ int_least32_t;
1033 typedef /*@integraltype@*/ int_least64_t;
1034
1035 typedef /*@unsignedintegraltype@*/ uint_least8_t;
1036 typedef /*@unsignedintegraltype@*/ uint_least16_t;
1037 typedef /*@unsignedintegraltype@*/ uint_least32_t;
1038 typedef /*@unsignedintegraltype@*/ uint_least64_t;
1039
1040 typedef /*@integraltype@*/ int_fast8_t;
1041 typedef /*@integraltype@*/ int_fast16_t;
1042 typedef /*@integraltype@*/ int_fast32_t;
1043 typedef /*@integraltype@*/ int_fast64_t;
1044
1045 typedef /*@unsignedintegraltype@*/ uint_fast8_t;
1046 typedef /*@unsignedintegraltype@*/ uint_fast16_t;
1047 typedef /*@unsignedintegraltype@*/ uint_fast32_t;
1048 typedef /*@unsignedintegraltype@*/ uint_fast64_t;
1049
1050 typedef int *intptr_t
1051    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;
1052
1053 typedef unsigned int *uintptr_t
1054    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;
1055
1056 typedef /*@signedintegraltype@*/ intmax_t;
1057 typedef /*@unsignedintegraltype@*/ uintmax_t;
1058
1059 /*
1060 ** What should the types be here?
1061 */ /*#*/
1062
1063 /*@constant int INT8_MIN@*/
1064 /*@constant int INT16_MIN@*/
1065 /*@constant int INT32_MIN@*/
1066 /*@constant int INT64_MIN@*/
1067
1068 /*@constant int INT8_MAX@*/
1069 /*@constant int INT16_MAX@*/
1070 /*@constant int INT32_MAX@*/
1071 /*@constant int INT64_MAX@*/
1072
1073 /*@constant int UINT8_MIN@*/
1074 /*@constant int UINT16_MIN@*/
1075 /*@constant int UINT32_MIN@*/
1076 /*@constant int UINT64_MIN@*/
1077
1078 /*@constant int INT_LEAST8_MIN@*/
1079 /*@constant int INT_LEAST16_MIN@*/
1080 /*@constant int INT_LEAST32_MIN@*/
1081 /*@constant int INT_LEAST64_MIN@*/
1082
1083 /*@constant int INT_LEAST8_MAX@*/
1084 /*@constant int INT_LEAST16_MAX@*/
1085 /*@constant int INT_LEAST32_MAX@*/
1086 /*@constant int INT_LEAST64_MAX@*/
1087
1088 /*@constant int UINT_LEAST8_MAX@*/
1089 /*@constant int UINT_LEAST16_MAX@*/
1090 /*@constant int UINT_LEAST32_MAX@*/
1091 /*@constant int UINT_LEAST64_MAX@*/
1092
1093 /*@constant int INT_FAST8_MIN@*/
1094 /*@constant int INT_FAST16_MIN@*/
1095 /*@constant int INT_FAST32_MIN@*/
1096 /*@constant int INT_FAST64_MIN@*/
1097
1098 /*@constant int INT_FAST8_MAX@*/
1099 /*@constant int INT_FAST16_MAX@*/
1100 /*@constant int INT_FAST32_MAX@*/
1101 /*@constant int INT_FAST64_MAX@*/
1102
1103 /*@constant int UINT_FAST8_MAX@*/
1104 /*@constant int UINT_FAST16_MAX@*/
1105 /*@constant int UINT_FAST32_MAX@*/
1106 /*@constant int UINT_FAST64_MAX@*/
1107
1108 /*@constant size_t INTPTR_MIN@*/
1109 /*@constant size_t INTPTR_MAX@*/