2 ** standard.h --- ISO C99 Standard Library for Splint.
4 ** Process with -DSTRICT to get strict library.
9 /*@+globsimpmodifiesnothing@*/
15 /*@constant int EDOM;@*/
16 /*@constant int ERANGE;@*/
17 /*@constant int EILSEQ;@*/
20 /*@checkedstrict@*/ int errno;
22 /*@unchecked@*/ int errno;
32 /*@constant bool true@*/
33 /*@constant bool false@*/
34 /*@constant int __bool_true_false_are_defined = 1@*/
40 typedef /*@integraltype@*/ ptrdiff_t;
41 typedef /*@unsignedintegraltype@*/ size_t;
42 typedef /*@signedintegraltype@*/ ssize_t;
43 typedef /*@integraltype@*/ wchar_t;
46 ** Added by Amendment 1 to ISO.
49 typedef /*@integraltype@*/ wint_t;
50 typedef /*@abstract@*/ mbstate_t;
52 /*@constant null anytype NULL = 0;@*/
58 /*@constant _Bool NDEBUG;@*/
61 /*@falseexit@*/ void assert (/*@sef@*/ _Bool e)
64 /*@falseexit@*/ void assert (/*@sef@*/ _Bool /*@alt int@*/ e)
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) /*@*/ ;
89 ** evans 2002-01-03: added alt char (was alt unsigned char)
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) /*@*/ ;
116 char *int_curr_symbol;
117 char *currency_symbol;
118 char *mon_decimal_point;
119 char *mon_thousands_sep;
123 char int_frac_digits;
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;@*/
140 /*@observer@*/ /*@null@*/ char *setlocale (int category, /*@null@*/ char *locale)
141 /*@modifies internalState, errno@*/ ;
143 struct lconv *localeconv (void) /*@*/ ;
150 ** Note, these are defined by macros, but NOT necessarily
151 ** constants. They may be used as lvalues.
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;
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;
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;
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; @*/
211 ** evans 2002-07-03: updated from ISO C99 (http://www.vmunix.com/~gabor/c/draft.html)
214 typedef float float_t;
215 typedef double double_t;
217 /*@constant double HUGE_VAL; @*/
218 /*@constant float HUGE_VALF; @*/
219 /*@constant long double HUGE_VALL; @*/
221 /*@constant float INFINITY; @*/
223 /*@constant float NAN; @*/
224 /*:warn implementationoptional "NAN is defined if and only if the implementation supports quiet float type NaNs.":*/ ;
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;@*/
232 /*@constant int FP_ILOGB0;@*/
233 /*@constant int FP_ILOGBNAN;@*/
235 /*@constant int DECIMAL_DIG;@*/
237 /* Defined for specs only - this type is any real type */
238 typedef float /*@alt double, long double@*/ s_real_t;
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) /*@*/ ;
248 ** math functions that may have a range error modify errno (implementation defined).
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) /*@*/ ;
256 double cos (double x) /*@*/ ;
257 double sin (double x) /*@*/ ;
258 double tan (double x) /*@*/ ;
260 double cosh (double x) /*@modifies errno@*/ ;
261 double sinh (double x) /*@modifies errno@*/ ;
262 double tanh (double x) /*@*/ ;
264 double acosh (double x) /*@modifies errno@*/ ;
265 double asinh (double x) /*@modifies errno@*/ ;
266 double atanh (double x) /*@modifies errno@*/ ;
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@*/ ;
272 double log (double x) /*@modifies errno@*/ ;
273 double log10 (double x) /*@modifies errno@*/ ;
275 double modf (double x, /*@out@*/ double *ip) /*@modifies *ip;@*/ ;
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@*/ ;
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@*/ ;
287 int ilogb (double x) /*@modifies errno@*/ ;
288 int ilogbf (float x) /*@modifies errno@*/ ;
289 int ilogbl (long double x) /*@modifies errno@*/ ;
291 double fabs (double x) /*@*/ ;
292 float fabsf (float x) /*@*/ ;
293 long double fabsl (long double x) /*@*/ ;
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@*/ ;
299 double sqrt (double x) /*@modifies errno@*/ ;
300 float sqrtf(float x) /*@modifies errno@*/ ;
301 long double sqrtl (long double x) /*@modifies errno@*/ ;
303 double cbrt (double x) /*@*/ ;
304 float cbrtf (float x) /*@*/ ;
305 long double cbrtl (long double x) /*@*/ ;
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@*/ ;
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) /*@*/ ;
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@*/ ;
325 double ceil (double x) /*@*/ ;
326 float ceilf(float x) /*@*/ ;
327 long double ceill(long double x) /*@*/ ;
329 double floor (double x) /*@*/ ;
330 float floorf (float x) /*@*/ ;
331 long double floorl (long double x) /*@*/ ;
333 double nearbyint (double x) /*@*/ ;
334 float nearbyintf (float x) /*@*/ ;
335 long double nearbyintl (long double x) /*@*/ ;
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@*/ ;
347 double round (double x) /*@*/ ;
348 long int lround (double x) /*@modifies errno@*/ ;
349 long long llround (double x) /*@modifies errno@*/ ;
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) /*@*/ ;
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) /*@*/ ;
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) /*@*/ ;
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.
378 # ifdef OPTIONAL_MATH
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) /*@*/ ;
431 typedef /*@abstract@*/ /*@mutable@*/ void *jmp_buf;
433 int setjmp (/*@out@*/ jmp_buf env) /*@modifies env;@*/ ;
434 /*@mayexit@*/ void longjmp (jmp_buf env, int val) /*@*/ ;
440 /*@constant int SIGABRT; @*/
441 /*@constant int SIGFPE; @*/
442 /*@constant int SIGILL; @*/
443 /*@constant int SIGINT; @*/
444 /*@constant int SIGSEGV; @*/
445 /*@constant int SIGTERM; @*/
447 typedef /*@integraltype@*/ sig_atomic_t;
449 /*@constant void (*SIG_DFL)(int); @*/
450 /*@constant void (*SIG_ERR)(int); @*/
451 /*@constant void (*SIG_IGN)(int); @*/
454 ** signal takes an int, and a function takes int returns void, and
455 ** returns the function (or NULL if unsuccessful).
458 /*@null@*/ void (*signal (int sig, /*@null@*/ void (*func)(int))) (int)
459 /*@modifies internalState, errno;@*/ ;
461 /*@mayexit@*/ int raise (int sig) ;
467 typedef /*@abstract@*/ /*@mutable@*/ void *va_list;
469 void va_start (/*@out@*/ va_list ap, ...) /*@modifies ap;@*/ ;
470 void va_end (va_list va) /*@modifies va;@*/ ;
480 typedef /*@abstract@*/ /*@mutable@*/ void *FILE;
481 typedef /*@abstract@*/ /*@mutable@*/ void *fpos_t;
483 /*@constant size_t _IOFBF; @*/
484 /*@constant size_t _IOLBF; @*/
485 /*@constant size_t _IONBF; @*/
487 /*@constant size_t BUFSIZ; @*/ /* evans 2002-02-27 change suggested by Walter Briscoe */
489 /*@constant int EOF; @*/
491 /*@constant int FOPEN_MAX; @*/
492 /*@constant int FILENAME_MAX; @*/
494 /*@constant int L_tmpnam; @*/
496 /*@constant int SEEK_CUR; @*/
497 /*@constant int SEEK_END; @*/
498 /*@constant int SEEK_SET; @*/
500 /*@constant int TMP_MAX; @*/
503 /*@checked@*/ FILE *stderr;
504 /*@checked@*/ FILE *stdin;
505 /*@checked@*/ FILE *stdout;
507 /*@unchecked@*/ FILE *stderr;
508 /*@unchecked@*/ FILE *stdin;
509 /*@unchecked@*/ FILE *stdout;
512 int remove (char *filename) /*@modifies fileSystem, errno@*/ ;
513 int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ;
515 /*@dependent@*/ /*@null@*/ FILE *tmpfile (void)
516 /*@modifies fileSystem, errno@*/ ;
518 /*@observer@*/ char *
519 tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s)
520 /*@modifies *s, internalState@*/ ;
522 int fclose (FILE *stream)
523 /*@modifies *stream, errno, fileSystem;@*/ ;
525 int fflush (/*@null@*/ FILE *stream)
526 /*@modifies *stream, errno, fileSystem;@*/ ;
528 /*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode)
529 /*@modifies fileSystem@*/ ;
531 /*@dependent@*/ /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream)
532 /*@modifies *stream, fileSystem, errno@*/ ;
534 void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf)
535 /*@modifies fileSystem, *stream, *buf@*/
536 /*:errorcode != 0*/ ;
537 /*:requires maxSet(buf) >= (BUFSIZ - 1):*/ ;
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) @*/ ;
546 int fprintf (FILE *stream, char *format, ...)
547 /*@modifies fileSystem, *stream@*/ ;
550 int /*@alt void@*/ fprintf (FILE *stream, char *format, ...)
551 /*@modifies fileSystem, *stream@*/ ;
555 int fscanf (FILE *stream, char *format, ...)
556 /*@modifies fileSystem, *stream, errno@*/ ;
560 int printf (char *format, ...)
562 /*@modifies fileSystem, *stdout@*/ ;
565 int /*@alt void@*/ printf (char *format, ...)
567 /*@modifies fileSystem, *stdout@*/ ;
571 int scanf(char *format, ...)
573 /*@modifies fileSystem, *stdin, errno@*/ ;
574 /*drl added errno 09-19-2001 */ ;
578 int sprintf (/*@out@*/ char *s, char *format, ...)
579 /*@warn bufferoverflowhigh "Buffer overflow possible with sprintf. Recommend using snprintf instead"@*/
583 int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...)
584 /*@warn bufferoverflowhigh "Buffer overflow possible with sprintf. Recommend using snprintf instead"@*/
588 /* evans 2002-07-09: snprintf added to standard.h (from unix.h) */
590 int snprintf (/*@out@*/ char * restrict s, size_t n, const char * restrict format, ...)
592 /*@requires maxSet(s) >= (n - 1)@*/ ;
595 int sscanf (/*@out@*/ char *s, char *format, ...) /*@modifies errno@*/ ;
596 /* modifies extra arguments */
598 int vprintf (const char *format, va_list arg)
600 /*@modifies fileSystem, *stdout@*/ ;
602 int vfprintf (FILE *stream, char *format, va_list arg)
603 /*@modifies fileSystem, *stream, arg, errno@*/ ;
605 int vsprintf (/*@out@*/ char *str, const char *format, va_list ap)
606 /*@warn bufferoverflowhigh "Use vsnprintf instead"@*/
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 */
613 int fgetc (FILE *stream)
614 /*@modifies fileSystem, *stream, errno@*/ ;
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; @*/
623 int fputc (int /*@alt char@*/ c, FILE *stream)
625 /*@modifies fileSystem, *stream, errno@*/ ;
627 int fputs (char *s, FILE *stream)
628 /*@modifies fileSystem, *stream@*/ ;
630 /* note use of sef --- stream may be evaluated more than once */
631 int getc (/*@sef@*/ FILE *stream)
632 /*@modifies fileSystem, *stream, errno@*/ ;
634 int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin, errno@*/ ;
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@*/ ;
641 int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
643 /*@modifies fileSystem, *stream, errno;@*/ ;
645 int putchar (int /*@alt char@*/ c)
648 /*@modifies fileSystem, *stdout, errno@*/ ;
650 int puts (const char *s)
653 /*@modifies fileSystem, *stdout, errno@*/ ;
655 int ungetc (int /*@alt char@*/ c, FILE *stream)
656 /*@modifies fileSystem, *stream@*/ ;
657 /*drl REMOVED errno 09-19-2001*/
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) @*/ ;
665 size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream)
666 /*@modifies fileSystem, *stream, errno@*/
667 /*@requires maxRead(ptr) >= size @*/ ;
669 int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos)
670 /*@modifies *pos, errno@*/
671 /*@requires maxSet(pos) >= 0@*/
672 /*@ensures maxRead(pos) >= 0 @*/;
674 int fseek (FILE *stream, long int offset, int whence)
676 /*@modifies fileSystem, *stream, errno@*/ ;
678 int fsetpos (FILE *stream, fpos_t *pos)
679 /*@modifies fileSystem, *stream, errno@*/ ;
681 long int ftell(FILE *stream)
682 /*:errorcode -1:*/ /*@modifies errno*/ ;
684 void rewind (FILE *stream) /*@modifies *stream@*/ ;
685 void clearerr (FILE *stream) /*@modifies *stream@*/ ;
687 int feof (FILE *stream) /*@modifies errno@*/ ;
689 int ferror (FILE *stream) /*@modifies errno@*/ ;
691 void perror (/*@null@*/ char *s)
692 /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ;
698 double atof (char *s) /*@*/ ;
699 int atoi (char *s) /*@*/ ;
700 long int atol (char *s) /*@*/ ;
702 double strtod (char *s, /*@null@*/ /*@out@*/ char **endp)
703 /*@modifies *endp, errno@*/ ;
705 long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
706 /*@modifies *endp, errno@*/ ;
709 strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
710 /*@modifies *endp, errno@*/ ;
712 /*@constant int RAND_MAX; @*/
713 int rand (void) /*@modifies internalState@*/ ;
714 void srand (unsigned int seed) /*@modifies internalState@*/ ;
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); @*/ ;
728 /* 11 June 1997: removed out on return value */
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) @*/;
738 ** LCLint annotations cannot fully describe realloc. The semantics we
740 ** realloc returns null: ownership of parameter is not changed
741 ** realloc returns non-null: ownership of parameter is transferred to return value
743 ** Otherwise, storage is in the same state before and after the call.
746 /*@null@*/ /*@only@*/ void *
747 realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size)
748 /*@modifies *p@*/ /*@ensures maxSet(result) >= (size - 1) @*/;
750 void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies p@*/ ;
752 /*@constant int EXIT_FAILURE; @*/
753 /*@constant int EXIT_SUCCESS; @*/
755 /*@exits@*/ void abort (void) /*@*/ ;
756 /*@exits@*/ void exit (int status) /*@*/ ;
757 int atexit (void (*func)(void)) /*@modifies internalState@*/ ;
759 /*@observer@*/ /*@null@*/ char *getenv (char *name) /*@*/ ;
761 int system (/*@null@*/ char *s) /*@modifies fileSystem@*/ ;
763 /*@null@*/ /*@dependent@*/ void *
764 bsearch (void *key, void *base,
765 size_t n, size_t size,
766 int (*compar)(void *, void *)) /*@*/ ;
768 void qsort (void *base, size_t n, size_t size,
769 int (*compar)(void *, void *))
770 /*@modifies *base, errno@*/ ;
772 int abs (int n) /*@*/ ;
774 typedef /*@concrete@*/ struct
780 div_t div (int num, int denom) /*@*/ ;
782 long int labs (long int n) /*@*/ ;
784 typedef /*@concrete@*/ struct
790 ldiv_t ldiv (long num, long denom) /*@*/ ;
792 /*@constant size_t MB_CUR_MAX; @*/
795 ** wchar_t and wint_t functions added by Amendment 1 to ISO.
798 /*@constant int WCHAR_MAX@*/
799 /*@constant int WCHAR_MIN@*/
800 /*@constant wint_t WEOF@*/
802 wint_t btowc (int c) /*@*/ ;
804 wint_t fgetwc (FILE *fp) /*@modifies fileSystem, *fp*/ ;
806 /*@null@*/ wchar_t *fgetws (/*@returned@*/ wchar_t *s, int n, FILE *stream)
807 /*@modifies fileSystem, *s, *stream@*/;
809 wint_t fputwc (wchar_t c, FILE *stream)
810 /*@modifies fileSystem, *stream@*/;
812 int fputws (const wchar_t *s, FILE *stream)
813 /*@modifies fileSystem, *stream@*/ ;
815 int fwide (FILE *stream, int mode) /*@*/ ;
816 /* does not modify the stream */
818 /*@printflike@*/ int fwprintf (FILE *stream, const wchar_t *format, ...)
819 /*@modifies *stream, fileSystem@*/ ;
821 /*@scanflike@*/ int fwscanf (FILE *stream, const wchar_t *format, ...)
822 /*@modifies *stream, fileSystem@*/ ;
824 /* note use of sef --- stream may be evaluated more than once */
825 wint_t getwc (/*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ;
827 wint_t getwchar (void) /*@modifies fileSystem, *stdin@*/;
829 size_t mbrlen (const char *s, size_t n, /*@null@*/ mbstate_t *ps) /*@*/ ;
831 size_t mbrtowc (/*@null@*/ wchar_t *pwc, const char *s, size_t n,
832 /*@null@*/ mbstate_t *ps)
833 /*@modifies *pwc@*/ ;
835 int mbsinit (/*@null@*/ const mbstate_t *ps) /*@*/ ;
837 size_t mbsrtowcs (/*@null@*/ wchar_t *dst, const char **src, size_t len,
838 /*@null@*/ mbstate_t *ps)
839 /*@modifies *dst@*/ ;
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@*/ ;
844 wint_t putwchar (wchar_t c) /*@modifies fileSystem, *stdout@*/ ;
846 /*@printflike@*/ int swprintf (wchar_t *s, size_t n, const wchar_t *format, ...)
849 /*@scanflike@*/ int swscanf (const wchar_t *s, const wchar_t *format, ...)
850 /*@modifies *stdin@*/ ;
852 wint_t ungetwc (wint_t c, FILE *stream) /*@modifies fileSystem, *stream@*/ ;
854 int vfwprintf (FILE *stream, const wchar_t *format, va_list arg)
855 /*@modifies fileSystem, *stream@*/ ;
857 int vswprintf (wchar_t *s, size_t n, const wchar_t *format, va_list arg)
860 int vwprintf (const wchar_t *format, va_list arg)
861 /*@modifies fileSystem, *stdout@*/ ;
863 size_t wcrtomb (/*@null@*/ /*@out@*/ char *s, wchar_t wc, /*@null@*/ mbstate_t *ps)
866 void /*@alt wchar_t *@*/
867 wcscat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2)
870 /*@exposed@*/ /*@null@*/ wchar_t *
871 wcschr (/*@returned@*/ const wchar_t *s, wchar_t c)
874 int wcscmp (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
876 int wcscoll (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
878 void /*@alt wchar_t *@*/
879 wcscpy (/*@unique@*/ /*@out@*/ /*@returned@*/ wchar_t *s1, const wchar_t *s2)
882 size_t wcscspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
884 size_t wcsftime (/*@out@*/ wchar_t *s, size_t maxsize, const wchar_t *format,
885 const struct tm *timeptr)
888 size_t wcslen (const wchar_t *s) /*@*/ ;
890 void /*@alt wchar_t *@*/
891 wcsncat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
895 int wcsncmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
897 void /*@alt wchar_t *@*/
898 wcsncpy (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
903 wcspbrk (/*@returned@*/ const wchar_t *s1, const wchar_t *s2)
907 wcsrchr (/*@returned@*/ const wchar_t *s, wchar_t c)
911 wcsrtombs (/*@null@*/ char *dst, const wchar_t **src, size_t len,
912 /*@null@*/ mbstate_t *ps)
913 /*@modifies *src@*/ ;
915 size_t wcsspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
917 /*@null@*/ wchar_t *wcsstr (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
919 double wcstod (const wchar_t *nptr, /*@null@*/ wchar_t **endptr)
920 /*@modifies *endptr@*/ ;
923 wcstok (/*@null@*/ wchar_t *s1, const wchar_t *s2, wchar_t **ptr)
926 long wcstol (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
927 /*@modifies *endptr@*/;
930 wcstoul (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
931 /*@modifies *endptr@*/;
934 wcsxfrm (/*@null@*/ wchar_t *s1, const wchar_t *s2, size_t n)
937 int wctob (wint_t c) /*@*/;
939 /*@null@*/ wchar_t *wmemchr (const wchar_t *s, wchar_t c, size_t n) /*@*/ ;
941 int wmemcmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
943 wchar_t *wmemcpy (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
946 wchar_t *wmemmove (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
949 wchar_t *wmemset (/*@returned@*/ wchar_t *s, wchar_t c, size_t n)
952 /*@printflike@*/ int wprintf (const wchar_t *format, ...)
953 /*@globals stdout@*/ /*@modifies errno, *stdout@*/;
956 wscanf (const wchar_t *format, ...)
957 /*@globals stdin@*/ /*@modifies errno, *stdin@*/;
960 ** wctype.h (added by Amendment 1)
963 /* Warning: not sure about these (maybe abstract?): */
964 typedef /*@integraltype@*/ wctype_t;
965 typedef /*@integraltype@*/ wctrans_t;
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) /*@*/ ;
981 wint_t towctrans (wint_t c, wctrans_t ctg) /*@*/ ;
982 wint_t towlower (wint_t c) /*@*/ ;
983 wint_t towupper (wint_t c) /*@*/ ;
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) /*@*/ ;
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) /*@*/ ;
1003 wctrans_t wctrans (const char *property) /*@*/ ;
1004 wctype_t wctype (const char *property) /*@*/ ;
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)
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)
1020 void /*@alt void * @*/
1021 memcpy (/*@unique@*/ /*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
1023 /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
1026 void /*@alt void * @*/
1027 memmove (/*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
1029 /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
1037 void /*@alt char * @*/
1038 strcpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2)
1040 /*@requires maxSet(s1) >= maxRead(s2) @*/
1041 /*@ensures maxRead(s1) == maxRead (s2) /\ maxRead(result) == maxRead(s2) /\ maxSet(result) == maxSet(s1); @*/;
1043 void /*@alt char * @*/
1044 strncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2, size_t n)
1046 /*@requires maxSet(s1) >= ( n - 1 ); @*/
1047 /*@ensures maxRead (s2) >= maxRead(s1) /\ maxRead (s1) <= n; @*/ ;
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) );@*/;
1054 void /*@alt char * @*/
1055 strncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, size_t n)
1057 /*@requires maxSet(s1) >= ( maxRead(s1) + n); @*/
1058 /*@ensures maxRead(s1) >= (maxRead(s1) + n); @*/;
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 */
1069 /*@null@*/ void *memchr (void *s, int c, size_t n) /*@*/ ;
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 @*/ ;
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; @*/ ;
1079 size_t strcspn (char *s1, char *s2) /*@*/ ;
1080 /*@null@*/ /*@exposed@*/ char *
1081 strpbrk (/*@returned@*/ char *s, char *t) /*@*/ ;
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 @*/ ;
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 @*/ ;
1091 size_t strspn (char *s, char *t) /*@*/ ;
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)@*/ ;
1097 /*@null@*/ /*@exposed@*/ char *
1098 strtok (/*@returned@*/ /*@null@*/ char *s, char *t)
1099 /*@modifies *s, internalState, errno@*/ ;
1101 void /*@alt void *@*/ memset (/*@out@*/ /*@returned@*/ void *s,
1103 /*@modifies *s@*/ /*@requires maxSet(s) >= (n - 1) @*/ /*@ensures maxRead(s) >= (n - 1) @*/ ;
1105 /*@observer@*/ char *strerror (int errnum) /*@*/ ;
1108 size_t strlen (char *s) /*@*/ /*@ensures result == maxRead(s); @*/;
1114 /*@constant int CLOCKS_PER_SEC;@*/
1116 typedef /*@integraltype@*/ clock_t;
1117 typedef /*@integraltype@*/ time_t;
1132 clock_t clock (void) /*@modifies internalState@*/ ;
1133 double difftime (time_t time1, time_t time0) /*@*/ ;
1134 time_t mktime (struct tm *timeptr) /*@*/ ;
1136 time_t time (/*@null@*/ /*@out@*/ time_t *tp)
1137 /*@modifies *tp@*/ ;
1139 /*@observer@*/ char *asctime (struct tm *timeptr)
1140 /*@modifies errno*/ /*@ensures maxSet(result) == 25 /\ maxRead(result) == 25; @*/ ;
1142 /*@observer@*/ char *ctime (time_t *tp) /*@*/
1143 /*@ensures maxSet(result) == 25 /\ maxRead(result) == 25; @*/;
1145 /*@null@*/ /*@observer@*/ struct tm *gmtime (time_t *tp) /*@*/ ;
1147 /*@null@*/ /*@observer@*/ struct tm *localtime (time_t *tp)
1148 /*@modifies errno@*/ ;
1150 size_t strftime (/*@out@*/ char *s, size_t smax,
1151 char *fmt, struct tm *timeptr)
1155 ** ISO c99: 7.18 Integer types <stdint.h>
1159 ** These types are OPTIONAL. Provide warnings on use.
1162 typedef /*@integraltype@*/ int8_t
1163 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least8_t instead."@*/ ;
1165 typedef /*@integraltype@*/ int16_t
1166 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least16_t instead."@*/ ;
1168 typedef /*@integraltype@*/ int32_t
1169 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least32_t instead."@*/ ;
1171 typedef /*@integraltype@*/ int64_t
1172 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least64_t instead."@*/ ;
1174 typedef /*@unsignedintegraltype@*/ uint8_t
1175 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least8_t instead."@*/ ;
1177 typedef /*@unsignedintegraltype@*/ uint16_t
1178 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least16_t instead."@*/ ;
1180 typedef /*@unsignedintegraltype@*/ uint32_t
1181 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least32_t instead."@*/ ;
1183 typedef /*@unsignedintegraltype@*/ uint64_t
1184 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least64_t instead."@*/ ;
1186 typedef /*@integraltype@*/ int_least8_t;
1187 typedef /*@integraltype@*/ int_least16_t;
1188 typedef /*@integraltype@*/ int_least32_t;
1189 typedef /*@integraltype@*/ int_least64_t;
1191 typedef /*@unsignedintegraltype@*/ uint_least8_t;
1192 typedef /*@unsignedintegraltype@*/ uint_least16_t;
1193 typedef /*@unsignedintegraltype@*/ uint_least32_t;
1194 typedef /*@unsignedintegraltype@*/ uint_least64_t;
1196 typedef /*@integraltype@*/ int_fast8_t;
1197 typedef /*@integraltype@*/ int_fast16_t;
1198 typedef /*@integraltype@*/ int_fast32_t;
1199 typedef /*@integraltype@*/ int_fast64_t;
1201 typedef /*@unsignedintegraltype@*/ uint_fast8_t;
1202 typedef /*@unsignedintegraltype@*/ uint_fast16_t;
1203 typedef /*@unsignedintegraltype@*/ uint_fast32_t;
1204 typedef /*@unsignedintegraltype@*/ uint_fast64_t;
1206 typedef int *intptr_t
1207 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;
1209 typedef unsigned int *uintptr_t
1210 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;
1212 typedef /*@signedintegraltype@*/ intmax_t;
1213 typedef /*@unsignedintegraltype@*/ uintmax_t;
1216 ** What should the types be here?
1219 /*@constant int INT8_MIN@*/
1220 /*@constant int INT16_MIN@*/
1221 /*@constant int INT32_MIN@*/
1222 /*@constant int INT64_MIN@*/
1224 /*@constant int INT8_MAX@*/
1225 /*@constant int INT16_MAX@*/
1226 /*@constant int INT32_MAX@*/
1227 /*@constant int INT64_MAX@*/
1229 /*@constant int UINT8_MIN@*/
1230 /*@constant int UINT16_MIN@*/
1231 /*@constant int UINT32_MIN@*/
1232 /*@constant int UINT64_MIN@*/
1234 /*@constant int INT_LEAST8_MIN@*/
1235 /*@constant int INT_LEAST16_MIN@*/
1236 /*@constant int INT_LEAST32_MIN@*/
1237 /*@constant int INT_LEAST64_MIN@*/
1239 /*@constant int INT_LEAST8_MAX@*/
1240 /*@constant int INT_LEAST16_MAX@*/
1241 /*@constant int INT_LEAST32_MAX@*/
1242 /*@constant int INT_LEAST64_MAX@*/
1244 /*@constant int UINT_LEAST8_MAX@*/
1245 /*@constant int UINT_LEAST16_MAX@*/
1246 /*@constant int UINT_LEAST32_MAX@*/
1247 /*@constant int UINT_LEAST64_MAX@*/
1249 /*@constant int INT_FAST8_MIN@*/
1250 /*@constant int INT_FAST16_MIN@*/
1251 /*@constant int INT_FAST32_MIN@*/
1252 /*@constant int INT_FAST64_MIN@*/
1254 /*@constant int INT_FAST8_MAX@*/
1255 /*@constant int INT_FAST16_MAX@*/
1256 /*@constant int INT_FAST32_MAX@*/
1257 /*@constant int INT_FAST64_MAX@*/
1259 /*@constant int UINT_FAST8_MAX@*/
1260 /*@constant int UINT_FAST16_MAX@*/
1261 /*@constant int UINT_FAST32_MAX@*/
1262 /*@constant int UINT_FAST64_MAX@*/
1264 /*@constant size_t INTPTR_MIN@*/
1265 /*@constant size_t INTPTR_MAX@*/