lib/ansi.h

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