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 /*
 473 ** va_arg is builtin
 474 */
 475
 476 /*
 477 ** stdio.h
 478 */
 479
 480 typedef /*@abstract@*/ /*@mutable@*/ void *FILE;
 481 typedef /*@abstract@*/ /*@mutable@*/ void *fpos_t;
 482
 483 /*@constant size_t _IOFBF; @*/
 484 /*@constant size_t _IOLBF; @*/
 485 /*@constant size_t _IONBF; @*/
 486
 487 /*@constant size_t BUFSIZ; @*/ /* evans 2002-02-27 change suggested by Walter Briscoe */
 488
 489 /*@constant int EOF; @*/
 490
 491 /*@constant int FOPEN_MAX; @*/
 492 /*@constant int FILENAME_MAX; @*/
 493
 494 /*@constant int L_tmpnam; @*/
 495
 496 /*@constant int SEEK_CUR; @*/
 497 /*@constant int SEEK_END; @*/
 498 /*@constant int SEEK_SET; @*/
 499
 500 /*@constant int TMP_MAX; @*/
 501
 502 # ifdef STRICT
 503 /*@checked@*/ FILE *stderr;
 504 /*@checked@*/ FILE *stdin;
 505 /*@checked@*/ FILE *stdout;
 506 # else
 507 /*@unchecked@*/ FILE *stderr;
 508 /*@unchecked@*/ FILE *stdin;
 509 /*@unchecked@*/ FILE *stdout;
 510 # endif
 511
 512 int remove (char *filename) /*@modifies fileSystem, errno@*/ ;
 513 int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ;
 514
 515 /*@dependent@*/ /*@null@*/ FILE *tmpfile (void)
 516    /*@modifies fileSystem, errno@*/ ;
 517
 518 /*@observer@*/ char *
 519   tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s)
 520   /*@modifies *s, internalState@*/ ;
 521
 522 int fclose (FILE *stream)
 523    /*@modifies *stream, errno, fileSystem;@*/ ;
 524
 525 int fflush (/*@null@*/ FILE *stream)
 526    /*@modifies *stream, errno, fileSystem;@*/ ;
 527
 528 /*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode)
 529    /*@modifies fileSystem@*/ ;
 530
 531 /*@dependent@*/ /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream)
 532   /*@modifies *stream, fileSystem, errno@*/ ;
 533
 534 void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf)
 535      /*@modifies fileSystem, *stream, *buf@*/
 536      /*:errorcode != 0*/ ;
 537      /*:requires maxSet(buf) >= (BUFSIZ - 1):*/ ;
 538
 539 int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf,
 540              int mode, size_t size)
 541       /*@modifies fileSystem, *stream, *buf@*/
 542      /*@requires maxSet(buf) >= (size - 1) @*/ ;
 543
 544 # ifdef STRICT
 545 /*@printflike@*/
 546 int fprintf (FILE *stream, char *format, ...)
 547    /*@modifies fileSystem, *stream@*/ ;
 548 # else
 549 /*@printflike@*/
 550 int /*@alt void@*/ fprintf (FILE *stream, char *format, ...)
 551    /*@modifies fileSystem, *stream@*/ ;
 552 # endif
 553
 554 /*@scanflike@*/
 555 int fscanf (FILE *stream, char *format, ...)
 556    /*@modifies fileSystem, *stream, errno@*/ ;
 557
 558 # ifdef STRICT
 559 /*@printflike@*/
 560 int printf (char *format, ...)
 561    /*@globals stdout@*/
 562    /*@modifies fileSystem, *stdout@*/ ;
 563 # else
 564 /*@printflike@*/
 565 int /*@alt void@*/ printf (char *format, ...)
 566    /*@globals stdout@*/
 567    /*@modifies fileSystem, *stdout@*/ ;
 568 # endif
 569
 570 /*@scanflike@*/
 571 int scanf(char *format, ...)
 572    /*@globals stdin@*/
 573    /*@modifies fileSystem, *stdin, errno@*/ ;
 574    /*drl added errno 09-19-2001 */ ;
 575
 576 # ifdef STRICT
 577 /*@printflike@*/
 578 int sprintf (/*@out@*/ char *s, char *format, ...)
 579    /*@warn bufferoverflowhigh "Buffer overflow possible with sprintf.  Recommend using snprintf instead"@*/
 580    /*@modifies *s@*/ ;
 581 # else
 582 /*@printflike@*/
 583 int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...)
 584    /*@warn bufferoverflowhigh "Buffer overflow possible with sprintf.  Recommend using snprintf instead"@*/
 585    /*@modifies *s@*/ ;
 586 # endif
 587
 588 /* evans 2002-07-09: snprintf added to standard.h (from unix.h) */
 589 /*@printflike@*/
 590 int snprintf (/*@out@*/ char * restrict s, size_t n, const char * restrict format, ...)
 591    /*@modifies s@*/
 592    /*@requires maxSet(s) >= (n - 1)@*/ ;
 593
 594 /*@scanflike@*/
 595 int sscanf (/*@out@*/ char *s, char *format, ...) /*@modifies errno@*/ ;
 596    /* modifies extra arguments */
 597
 598 int vprintf (const char *format, va_list arg)
 599    /*@globals stdout@*/
 600    /*@modifies fileSystem, *stdout@*/ ;
 601
 602 int vfprintf (FILE *stream, char *format, va_list arg)
 603    /*@modifies fileSystem, *stream, arg, errno@*/ ;
 604
 605 int vsprintf (/*@out@*/ char *str, const char *format, va_list ap)
 606      /*@warn bufferoverflowhigh "Use vsnprintf instead"@*/
 607      /*@modifies str@*/ ;
 608
 609 int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap)
 610      /*@requires maxSet(str) >= (size - 1)@*/ /* drl - this was size, size-1 in stdio.h */
 611      /*@modifies str@*/ ;
 612
 613 int fgetc (FILE *stream)
 614    /*@modifies fileSystem, *stream, errno@*/ ;
 615
 616 /*@null@*/ char *
 617   fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream)
 618      /*@modifies fileSystem, *s, *stream, errno@*/
 619      /*@requires maxSet(s) >= (n -1); @*/
 620      /*@ensures maxRead(s) <= (n -1) /\ maxRead(s) >= 0; @*/
 621      ;
 622
 623 int fputc (int /*@alt char@*/ c, FILE *stream)
 624   /*:errorcode EOF:*/
 625   /*@modifies fileSystem, *stream, errno@*/ ;
 626
 627 int fputs (char *s, FILE *stream)
 628   /*@modifies fileSystem, *stream@*/ ;
 629
 630 /* note use of sef --- stream may be evaluated more than once */
 631 int getc (/*@sef@*/ FILE *stream)
 632   /*@modifies fileSystem, *stream, errno@*/ ;
 633
 634 int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin, errno@*/ ;
 635
 636 /*@null@*/ char *gets (/*@out@*/ char *s)
 637    /*@warn bufferoverflowhigh
 638            "Use of gets leads to a buffer overflow vulnerability.  Use fgets instead"@*/
 639    /*@globals stdin@*/ /*@modifies fileSystem, *s, *stdin, errno@*/ ;
 640
 641 int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
 642    /*:errorcode EOF:*/
 643    /*@modifies fileSystem, *stream, errno;@*/ ;
 644
 645 int putchar (int /*@alt char@*/ c)
 646    /*:errorcode EOF:*/
 647    /*@globals stdout@*/
 648    /*@modifies fileSystem, *stdout, errno@*/ ;
 649
 650 int puts (const char *s)
 651    /*:errorcode EOF:*/
 652    /*@globals stdout@*/
 653    /*@modifies fileSystem, *stdout, errno@*/ ;
 654
 655 int ungetc (int /*@alt char@*/ c, FILE *stream)
 656   /*@modifies fileSystem, *stream@*/ ;
 657       /*drl REMOVED errno 09-19-2001*/
 658
 659 size_t
 660   fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream)
 661   /*@modifies fileSystem, *ptr, *stream, errno@*/
 662   /*requires maxSet(ptr) >= (size - 1) @*/
 663   /*@ensures maxRead(ptr) == (size - 1) @*/ ;
 664
 665 size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream)
 666   /*@modifies fileSystem, *stream, errno@*/
 667   /*@requires maxRead(ptr) >= size @*/ ;
 668
 669 int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos)
 670    /*@modifies *pos, errno@*/
 671    /*@requires maxSet(pos) >= 0@*/
 672    /*@ensures maxRead(pos) >= 0 @*/;
 673
 674 int fseek (FILE *stream, long int offset, int whence)
 675    /*:errorcode -1:*/
 676    /*@modifies fileSystem, *stream, errno@*/ ;
 677
 678 int fsetpos (FILE *stream, fpos_t *pos)
 679    /*@modifies fileSystem, *stream, errno@*/ ;
 680
 681 long int ftell(FILE *stream)
 682    /*:errorcode -1:*/ /*@modifies errno*/ ;
 683
 684 void rewind (FILE *stream) /*@modifies *stream@*/ ;
 685 void clearerr (FILE *stream) /*@modifies *stream@*/ ;
 686
 687 int feof (FILE *stream) /*@modifies errno@*/ ;
 688
 689 int ferror (FILE *stream) /*@modifies errno@*/ ;
 690
 691 void perror (/*@null@*/ char *s)
 692    /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ;
 693
 694 /*
 695 ** stdlib.h
 696 */
 697
 698 double atof (char *s) /*@*/ ;
 699 int atoi (char *s) /*@*/ ;
 700 long int atol (char *s) /*@*/ ;
 701
 702 double strtod (char *s, /*@null@*/ /*@out@*/ char **endp)
 703   /*@modifies *endp, errno@*/ ;
 704
 705 long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
 706   /*@modifies *endp, errno@*/ ;
 707
 708 unsigned long
 709   strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
 710   /*@modifies *endp, errno@*/ ;
 711
 712 /*@constant int RAND_MAX; @*/
 713 int rand (void) /*@modifies internalState@*/ ;
 714 void srand (unsigned int seed) /*@modifies internalState@*/ ;
 715
 716 /*
 717   drl
 718   changed 12/29/2000
 719 */
 720
 721 /*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/
 722      /*@ensures maxSet(result) == (nobj - 1); @*/ ;
 723 /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@*/
 724      /*@ensures maxSet(result) == (size - 1); @*/ ;
 725
 726 /*end drl changed */
 727
 728 /* 11 June 1997: removed out on return value */
 729
 730 # if 0
 731 /*@null@*/ /*@only@*/ void *
 732    realloc (/*@null@*/ /*@only@*/ /*@special@*/ void *p,
 733             size_t size) /*@releases p@*/ /*@modifies *p@*/
 734      /*@ensures maxSet(result) == (size - 1) @*/;
 735 # endif
 736
 737 /*
 738 ** LCLint annotations cannot fully describe realloc.  The semantics we
 739 ** want are:
 740 **    realloc returns null: ownership of parameter is not changed
 741 **    realloc returns non-null: ownership of parameter is transferred to return value
 742 **
 743 ** Otherwise, storage is in the same state before and after the call.
 744 */
 745
 746 /*@null@*/ /*@only@*/ void *
 747    realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size)
 748      /*@modifies *p@*/ /*@ensures maxSet(result) >= (size - 1) @*/;
 749
 750 void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies p@*/ ;
 751
 752 /*@constant int EXIT_FAILURE; @*/
 753 /*@constant int EXIT_SUCCESS; @*/
 754
 755 /*@exits@*/ void abort (void) /*@*/ ;
 756 /*@exits@*/ void exit (int status) /*@*/ ;
 757 int atexit (void (*func)(void)) /*@modifies internalState@*/ ;
 758
 759 /*@observer@*/ /*@null@*/ char *getenv (char *name) /*@*/ ;
 760
 761 int system (/*@null@*/ char *s) /*@modifies fileSystem@*/ ;
 762
 763 /*@null@*/ /*@dependent@*/ void *
 764   bsearch (void *key, void *base,
 765            size_t n, size_t size,
 766            int (*compar)(void *, void *)) /*@*/ ;
 767
 768 void qsort (void *base, size_t n, size_t size,
 769                    int (*compar)(void *, void *))
 770    /*@modifies *base, errno@*/ ;
 771
 772 int abs (int n) /*@*/ ;
 773
 774 typedef /*@concrete@*/ struct
 775 {
 776   int quot;
 777   int rem;
 778 } div_t ;
 779
 780 div_t div (int num, int denom) /*@*/ ;
 781
 782 long int labs (long int n) /*@*/ ;
 783
 784 typedef /*@concrete@*/ struct
 785 {
 786   long int quot;
 787   long int rem;
 788 } ldiv_t ;
 789
 790 ldiv_t ldiv (long num, long denom) /*@*/ ;
 791
 792 /*@constant size_t MB_CUR_MAX; @*/
 793
 794 /*
 795 ** wchar_t and wint_t functions added by Amendment 1 to ISO.
 796 */
 797
 798 /*@constant int WCHAR_MAX@*/
 799 /*@constant int WCHAR_MIN@*/
 800 /*@constant wint_t WEOF@*/
 801
 802 wint_t btowc (int c) /*@*/ ;
 803
 804 wint_t fgetwc (FILE *fp)        /*@modifies fileSystem, *fp*/ ;
 805
 806 /*@null@*/ wchar_t *fgetws (/*@returned@*/ wchar_t *s, int n, FILE *stream)
 807    /*@modifies fileSystem, *s, *stream@*/;
 808
 809 wint_t fputwc (wchar_t c, FILE *stream)
 810    /*@modifies fileSystem, *stream@*/;
 811
 812 int fputws (const wchar_t *s, FILE *stream)
 813    /*@modifies fileSystem, *stream@*/ ;
 814
 815 int fwide (FILE *stream, int mode) /*@*/ ;
 816    /* does not modify the stream */
 817
 818 /*@printflike@*/ int fwprintf (FILE *stream, const wchar_t *format, ...)
 819     /*@modifies *stream, fileSystem@*/ ;
 820
 821 /*@scanflike@*/ int fwscanf (FILE *stream, const wchar_t *format, ...)
 822         /*@modifies *stream, fileSystem@*/ ;
 823
 824 /* note use of sef --- stream may be evaluated more than once */
 825 wint_t getwc (/*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ;
 826
 827 wint_t getwchar (void) /*@modifies fileSystem, *stdin@*/;
 828
 829 size_t mbrlen (const char *s, size_t n, /*@null@*/ mbstate_t *ps) /*@*/ ;
 830
 831 size_t mbrtowc (/*@null@*/ wchar_t *pwc, const char *s, size_t n,
 832                        /*@null@*/ mbstate_t *ps)
 833    /*@modifies *pwc@*/ ;
 834
 835 int mbsinit (/*@null@*/ const mbstate_t *ps) /*@*/ ;
 836
 837 size_t mbsrtowcs (/*@null@*/ wchar_t *dst, const char **src, size_t len,
 838                          /*@null@*/ mbstate_t *ps)
 839    /*@modifies *dst@*/ ;
 840
 841 /* note use of sef --- stream may be evaluated more than once */
 842 wint_t putwc (wchar_t c, /*@sef@*/ FILE *stream)        /*@modifies fileSystem, *stream@*/ ;
 843
 844 wint_t putwchar (wchar_t c) /*@modifies fileSystem, *stdout@*/ ;
 845
 846 /*@printflike@*/ int swprintf (wchar_t *s, size_t n, const wchar_t *format, ...)
 847    /*@modifies *s@*/ ;
 848
 849 /*@scanflike@*/ int swscanf (const wchar_t *s, const wchar_t *format, ...)
 850    /*@modifies *stdin@*/ ;
 851
 852 wint_t ungetwc (wint_t c, FILE *stream) /*@modifies fileSystem, *stream@*/ ;
 853
 854 int vfwprintf (FILE *stream, const wchar_t *format, va_list arg)
 855    /*@modifies fileSystem, *stream@*/ ;
 856
 857 int vswprintf (wchar_t *s, size_t n, const wchar_t *format, va_list arg)
 858    /*@modifies *s@*/ ;
 859
 860 int vwprintf (const wchar_t *format, va_list arg)
 861    /*@modifies fileSystem, *stdout@*/ ;
 862
 863 size_t wcrtomb (/*@null@*/ /*@out@*/ char *s, wchar_t wc, /*@null@*/ mbstate_t *ps)
 864    /*@modifies *s@*/;
 865
 866 void /*@alt wchar_t *@*/
 867   wcscat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2)
 868   /*@modifies *s1@*/ ;
 869
 870 /*@exposed@*/ /*@null@*/ wchar_t *
 871   wcschr (/*@returned@*/ const wchar_t *s, wchar_t c)
 872   /*@*/ ;
 873
 874 int wcscmp (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
 875
 876 int wcscoll (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
 877
 878 void /*@alt wchar_t *@*/
 879   wcscpy (/*@unique@*/ /*@out@*/ /*@returned@*/ wchar_t *s1, const wchar_t *s2)
 880   /*@modifies *s1@*/ ;
 881
 882 size_t wcscspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
 883
 884 size_t wcsftime (/*@out@*/ wchar_t *s, size_t maxsize, const wchar_t *format,
 885                         const struct tm *timeptr)
 886    /*@modifies *s@*/ ;
 887
 888 size_t wcslen (const wchar_t *s) /*@*/ ;
 889
 890 void /*@alt wchar_t *@*/
 891   wcsncat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
 892            size_t n)
 893   /*@modifies *s1@*/ ;
 894
 895 int wcsncmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
 896
 897 void /*@alt wchar_t *@*/
 898   wcsncpy (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
 899            size_t n)
 900    /*@modifies *s1@*/ ;
 901
 902 /*@null@*/ wchar_t *
 903   wcspbrk (/*@returned@*/ const wchar_t *s1, const wchar_t *s2)
 904   /*@*/ ;
 905
 906 /*@null@*/ wchar_t *
 907   wcsrchr (/*@returned@*/ const wchar_t *s, wchar_t c)
 908   /*@*/ ;
 909
 910 size_t
 911   wcsrtombs (/*@null@*/ char *dst, const wchar_t **src, size_t len,
 912              /*@null@*/ mbstate_t *ps)
 913   /*@modifies *src@*/ ;
 914
 915 size_t wcsspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
 916
 917 /*@null@*/ wchar_t *wcsstr (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
 918
 919 double wcstod (const wchar_t *nptr, /*@null@*/ wchar_t **endptr)
 920    /*@modifies *endptr@*/ ;
 921
 922 /*@null@*/ wchar_t *
 923   wcstok (/*@null@*/ wchar_t *s1, const wchar_t *s2, wchar_t **ptr)
 924   /*@modifies *ptr@*/;
 925
 926 long wcstol (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
 927    /*@modifies *endptr@*/;
 928
 929 unsigned long
 930   wcstoul (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
 931   /*@modifies *endptr@*/;
 932
 933 size_t
 934   wcsxfrm (/*@null@*/ wchar_t *s1, const wchar_t *s2, size_t n)
 935   /*@modifies *s1@*/;
 936
 937 int wctob (wint_t c) /*@*/;
 938
 939 /*@null@*/ wchar_t *wmemchr (const wchar_t *s, wchar_t c, size_t n) /*@*/ ;
 940
 941 int wmemcmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
 942
 943 wchar_t *wmemcpy (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
 944    /*@modifies *s1@*/;
 945
 946 wchar_t *wmemmove (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
 947    /*@modifies *s1@*/;
 948
 949 wchar_t *wmemset (/*@returned@*/ wchar_t *s, wchar_t c, size_t n)
 950    /*@modifies *s@*/;
 951
 952 /*@printflike@*/ int wprintf (const wchar_t *format, ...)
 953    /*@globals stdout@*/ /*@modifies errno, *stdout@*/;
 954
 955 /*@scanflike@*/ int
 956   wscanf (const wchar_t *format, ...)
 957   /*@globals stdin@*/ /*@modifies errno, *stdin@*/;
 958
 959 /*
 960 ** wctype.h (added by Amendment 1)
 961 */
 962
 963 /* Warning: not sure about these (maybe abstract?): */
 964 typedef /*@integraltype@*/ wctype_t;
 965 typedef /*@integraltype@*/ wctrans_t;
 966
 967 # ifdef STRICT
 968 _Bool iswalnum (wint_t c) /*@*/ ;
 969 _Bool iswalpha (wint_t c) /*@*/ ;
 970 _Bool iswcntrl (wint_t c) /*@*/ ;
 971 _Bool iswctype (wint_t c, wctype_t ctg) /*@*/ ;
 972 _Bool iswdigit (wint_t c) /*@*/ ;
 973 _Bool iswgraph (wint_t c) /*@*/ ;
 974 _Bool iswlower (wint_t c) /*@*/ ;
 975 _Bool iswprint (wint_t c) /*@*/ ;
 976 _Bool iswpunct (wint_t c) /*@*/ ;
 977 _Bool iswspace (wint_t c) /*@*/ ;
 978 _Bool iswupper (wint_t c) /*@*/ ;
 979 _Bool iswxdigit (wint_t c) /*@*/ ;
 980
 981 wint_t towctrans (wint_t c, wctrans_t ctg) /*@*/ ;
 982 wint_t towlower (wint_t c) /*@*/ ;
 983 wint_t towupper (wint_t c) /*@*/ ;
 984 # else
 985 _Bool /*@alt int@*/ iswalnum (wint_t c) /*@*/ ;
 986 _Bool /*@alt int@*/ iswalpha (wint_t c) /*@*/ ;
 987 _Bool /*@alt int@*/ iswcntrl (wint_t c) /*@*/ ;
 988 _Bool /*@alt int@*/ iswctype (wint_t c, wctype_t ctg) /*@*/ ;
 989 _Bool /*@alt int@*/ iswdigit (wint_t c) /*@*/ ;
 990 _Bool /*@alt int@*/ iswgraph (wint_t c) /*@*/ ;
 991 _Bool /*@alt int@*/ iswlower (wint_t c) /*@*/ ;
 992 _Bool /*@alt int@*/ iswprint (wint_t c) /*@*/ ;
 993 _Bool /*@alt int@*/ iswpunct (wint_t c) /*@*/ ;
 994 _Bool /*@alt int@*/ iswspace (wint_t c) /*@*/ ;
 995 _Bool /*@alt int@*/ iswupper (wint_t c) /*@*/ ;
 996 _Bool /*@alt int@*/ iswxdigit (wint_t c) /*@*/ ;
 997
 998 wint_t /*@alt int@*/ towctrans (wint_t c, wctrans_t ctg)        /*@*/ ;
 999 wint_t /*@alt int@*/ towlower (wint_t c)        /*@*/ ;
1000 wint_t /*@alt int@*/ towupper (wint_t c)        /*@*/ ;
1001 # endif
1002
1003 wctrans_t wctrans (const char *property)        /*@*/ ;
1004 wctype_t wctype (const char *property) /*@*/ ;
1005
1006 int mblen (char *s, size_t n) /*@*/ ;
1007 int mbtowc (/*@null@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n)
1008    /*@modifies *pwc@*/ ;
1009 int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar)
1010    /*@modifies *s@*/ ;
1011 size_t mbstowcs (/*@out@*/ wchar_t *pwcs, char *s, size_t n)
1012   /*@modifies *pwcs@*/ ;
1013 size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n)
1014   /*@modifies *s@*/ ;
1015
1016 /*
1017 ** string.h
1018 */
1019
1020 void /*@alt void * @*/
1021   memcpy (/*@unique@*/ /*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
1022   /*@modifies *s1@*/
1023      /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
1024      ;
1025
1026 void /*@alt void * @*/
1027   memmove (/*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
1028   /*@modifies *s1@*/
1029   /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
1030    ;
1031
1032
1033   /* drl
1034      modifed  12/29/2000
1035   */
1036
1037 void /*@alt char * @*/
1038   strcpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2)
1039      /*@modifies *s1@*/
1040      /*@requires maxSet(s1) >= maxRead(s2) @*/
1041      /*@ensures maxRead(s1) == maxRead (s2) /\ maxRead(result) == maxRead(s2) /\ maxSet(result) == maxSet(s1); @*/;
1042
1043 void /*@alt char * @*/
1044   strncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2, size_t n)
1045      /*@modifies *s1@*/
1046      /*@requires maxSet(s1) >= ( n - 1 ); @*/
1047      /*@ensures maxRead (s2) >= maxRead(s1) /\ maxRead (s1) <= n; @*/ ;
1048
1049 void /*@alt char * @*/
1050   strcat (/*@unique@*/ /*@returned@*/ char *s1, char *s2)
1051      /*@modifies *s1@*/ /*@requires maxSet(s1) >= (maxRead(s1) + maxRead(s2) );@*/
1052      /*@ensures maxRead(result) == (maxRead(s1) + maxRead(s2) );@*/;
1053
1054 void /*@alt char * @*/
1055   strncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, size_t n)
1056      /*@modifies *s1@*/
1057      /*@requires maxSet(s1) >= ( maxRead(s1) + n); @*/
1058       /*@ensures maxRead(s1) >= (maxRead(s1) + n); @*/;
1059
1060      /*drl end*/
1061
1062 int memcmp (void *s1, void *s2, size_t n) /*@*/ ;
1063 int strcmp (char *s1, char *s2) /*@*/ ;
1064 int strcoll (char *s1, char *s2) /*@*/ ;
1065 int strncmp (char *s1, char *s2, size_t n) /*@*/ ;
1066 size_t strxfrm (/*@out@*/ /*@null@*/ char *s1, char *s2, size_t n)
1067   /*@modifies *s1@*/ ;  /* s1 may be null only if n == 0 */
1068
1069 /*@null@*/ void *memchr (void *s, int c, size_t n) /*@*/ ;
1070
1071 # ifdef STRICT
1072 /*@exposed@*/ /*@null@*/ char *
1073 strchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
1074 # else
1075 /*@exposed@*/ /*@null@*/ char *
1076   strchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0; @*/ ;
1077 # endif
1078
1079 size_t strcspn (char *s1, char *s2) /*@*/ ;
1080 /*@null@*/ /*@exposed@*/ char *
1081   strpbrk (/*@returned@*/ char *s, char *t) /*@*/ ;
1082
1083 # ifdef STRICT
1084 /*@null@*/ /*@exposed@*/ char *
1085   strrchr (/*@returned@*/ char *s, char c) /*@*/  /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
1086 # else
1087 /*@null@*/ /*@exposed@*/ char *
1088   strrchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/  /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
1089 # endif
1090
1091 size_t strspn (char *s, char *t) /*@*/ ;
1092
1093 /*@null@*/ /*@exposed@*/  char *
1094   strstr (/*@returned@*/ const char *s, const char *t) /*@*/
1095        /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 /\ maxRead(result) >= maxRead(t) /\ maxSet(result) >= maxRead(t)@*/ ;
1096
1097 /*@null@*/ /*@exposed@*/ char *
1098   strtok (/*@returned@*/ /*@null@*/ char *s, char *t)
1099   /*@modifies *s, internalState, errno@*/ ;
1100
1101 void /*@alt void *@*/ memset (/*@out@*/ /*@returned@*/ void *s,
1102                                      int c, size_t n)
1103      /*@modifies *s@*/ /*@requires maxSet(s) >= (n - 1) @*/ /*@ensures maxRead(s) >= (n - 1) @*/ ;
1104
1105 /*@observer@*/ char *strerror (int errnum) /*@*/ ;
1106
1107 /*drl */
1108 size_t strlen (char *s) /*@*/ /*@ensures result == maxRead(s); @*/;
1109
1110 /*
1111 ** time.h
1112 */
1113
1114 /*@constant int CLOCKS_PER_SEC;@*/
1115
1116 typedef /*@integraltype@*/ clock_t;
1117 typedef /*@integraltype@*/ time_t;
1118
1119 struct tm
1120   {
1121     int tm_sec;
1122     int tm_min;
1123     int tm_hour;
1124     int tm_mday;
1125     int tm_mon;
1126     int tm_year;
1127     int tm_wday;
1128     int tm_yday;
1129     int tm_isdst;
1130   } ;
1131
1132 clock_t clock (void) /*@modifies internalState@*/ ;
1133 double difftime (time_t time1, time_t time0) /*@*/ ;
1134 time_t mktime (struct tm *timeptr) /*@*/ ;
1135
1136 time_t time (/*@null@*/ /*@out@*/ time_t *tp)
1137   /*@modifies *tp@*/ ;
1138
1139 /*@observer@*/ char *asctime (struct tm *timeptr)
1140   /*@modifies errno*/ /*@ensures maxSet(result) == 25 /\  maxRead(result) == 25; @*/ ;
1141
1142 /*@observer@*/ char *ctime (time_t *tp) /*@*/
1143      /*@ensures maxSet(result) == 25 /\  maxRead(result) == 25; @*/;
1144
1145 /* 2003-11-01: remove null annotation: gmtima and localtime cannot return null */
1146 /*@observer@*/ struct tm *gmtime (time_t *tp) /*@*/ ;
1147
1148 /*@observer@*/ struct tm *localtime (time_t *tp)
1149   /*@modifies errno@*/ ;
1150
1151 size_t strftime (/*@out@*/ char *s, size_t smax,
1152                         char *fmt, struct tm *timeptr)
1153   /*@modifies *s@*/ ;
1154
1155 /*
1156 ** ISO c99: 7.18 Integer types <stdint.h>
1157 */
1158
1159 /*
1160 ** These types are OPTIONAL.  Provide warnings on use.
1161 */
1162
1163 typedef /*@integraltype@*/ int8_t
1164    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least8_t instead."@*/ ;
1165
1166 typedef /*@integraltype@*/ int16_t
1167    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least16_t instead."@*/ ;
1168
1169 typedef /*@integraltype@*/ int32_t
1170    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least32_t instead."@*/ ;
1171
1172 typedef /*@integraltype@*/ int64_t
1173    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least64_t instead."@*/ ;
1174
1175 typedef /*@unsignedintegraltype@*/ uint8_t
1176    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least8_t instead."@*/ ;
1177
1178 typedef /*@unsignedintegraltype@*/ uint16_t
1179    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least16_t instead."@*/ ;
1180
1181 typedef /*@unsignedintegraltype@*/ uint32_t
1182    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least32_t instead."@*/ ;
1183
1184 typedef /*@unsignedintegraltype@*/ uint64_t
1185    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least64_t instead."@*/ ;
1186
1187 typedef /*@integraltype@*/ int_least8_t;
1188 typedef /*@integraltype@*/ int_least16_t;
1189 typedef /*@integraltype@*/ int_least32_t;
1190 typedef /*@integraltype@*/ int_least64_t;
1191
1192 typedef /*@unsignedintegraltype@*/ uint_least8_t;
1193 typedef /*@unsignedintegraltype@*/ uint_least16_t;
1194 typedef /*@unsignedintegraltype@*/ uint_least32_t;
1195 typedef /*@unsignedintegraltype@*/ uint_least64_t;
1196
1197 typedef /*@integraltype@*/ int_fast8_t;
1198 typedef /*@integraltype@*/ int_fast16_t;
1199 typedef /*@integraltype@*/ int_fast32_t;
1200 typedef /*@integraltype@*/ int_fast64_t;
1201
1202 typedef /*@unsignedintegraltype@*/ uint_fast8_t;
1203 typedef /*@unsignedintegraltype@*/ uint_fast16_t;
1204 typedef /*@unsignedintegraltype@*/ uint_fast32_t;
1205 typedef /*@unsignedintegraltype@*/ uint_fast64_t;
1206
1207 typedef int *intptr_t
1208    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;
1209
1210 typedef unsigned int *uintptr_t
1211    /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;
1212
1213 typedef /*@signedintegraltype@*/ intmax_t;
1214 typedef /*@unsignedintegraltype@*/ uintmax_t;
1215
1216 /*
1217 ** What should the types be here?
1218 */ /*#*/
1219
1220 /*@constant int INT8_MIN@*/
1221 /*@constant int INT16_MIN@*/
1222 /*@constant int INT32_MIN@*/
1223 /*@constant int INT64_MIN@*/
1224
1225 /*@constant int INT8_MAX@*/
1226 /*@constant int INT16_MAX@*/
1227 /*@constant int INT32_MAX@*/
1228 /*@constant int INT64_MAX@*/
1229
1230 /*@constant int UINT8_MIN@*/
1231 /*@constant int UINT16_MIN@*/
1232 /*@constant int UINT32_MIN@*/
1233 /*@constant int UINT64_MIN@*/
1234
1235 /*@constant int INT_LEAST8_MIN@*/
1236 /*@constant int INT_LEAST16_MIN@*/
1237 /*@constant int INT_LEAST32_MIN@*/
1238 /*@constant int INT_LEAST64_MIN@*/
1239
1240 /*@constant int INT_LEAST8_MAX@*/
1241 /*@constant int INT_LEAST16_MAX@*/
1242 /*@constant int INT_LEAST32_MAX@*/
1243 /*@constant int INT_LEAST64_MAX@*/
1244
1245 /*@constant int UINT_LEAST8_MAX@*/
1246 /*@constant int UINT_LEAST16_MAX@*/
1247 /*@constant int UINT_LEAST32_MAX@*/
1248 /*@constant int UINT_LEAST64_MAX@*/
1249
1250 /*@constant int INT_FAST8_MIN@*/
1251 /*@constant int INT_FAST16_MIN@*/
1252 /*@constant int INT_FAST32_MIN@*/
1253 /*@constant int INT_FAST64_MIN@*/
1254
1255 /*@constant int INT_FAST8_MAX@*/
1256 /*@constant int INT_FAST16_MAX@*/
1257 /*@constant int INT_FAST32_MAX@*/
1258 /*@constant int INT_FAST64_MAX@*/
1259
1260 /*@constant int UINT_FAST8_MAX@*/
1261 /*@constant int UINT_FAST16_MAX@*/
1262 /*@constant int UINT_FAST32_MAX@*/
1263 /*@constant int UINT_FAST64_MAX@*/
1264
1265 /*@constant size_t INTPTR_MIN@*/
1266 /*@constant size_t INTPTR_MAX@*/