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