lib/ansi.h

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