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;
29 typedef /*@integraltype@*/ ptrdiff_t;
30 typedef /*@unsignedintegraltype@*/ size_t;
31 typedef /*@signedintegraltype@*/ ssize_t;
32 typedef /*@integraltype@*/ wchar_t;
35 ** Added by Amendment 1 to ISO.
38 typedef /*@integraltype@*/ wint_t;
39 typedef /*@abstract@*/ mbstate_t;
41 /*@constant null anytype NULL = 0;@*/
47 /*@constant lltX_bool NDEBUG;@*/
50 /*@falseexit@*/ void assert (/*@sef@*/ lltX_bool e)
53 /*@falseexit@*/ void assert (/*@sef@*/ lltX_bool /*@alt int@*/ e)
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) /*@*/ ;
78 ** evans 2002-01-03: added alt char (was alt unsigned char)
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) /*@*/ ;
105 char *int_curr_symbol;
106 char *currency_symbol;
107 char *mon_decimal_point;
108 char *mon_thousands_sep;
112 char int_frac_digits;
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;@*/
129 /*@observer@*/ /*@null@*/ char *setlocale (int category, /*@null@*/ char *locale)
130 /*@modifies internalState, errno@*/ ;
132 struct lconv *localeconv (void) /*@*/ ;
139 ** Note, these are defined by macros, but NOT necessarily
140 ** constants. They may be used as lvalues.
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;
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;
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;
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; @*/
200 ** evans 2002-07-03: updated from ISO C99 (http://www.vmunix.com/~gabor/c/draft.html)
203 typedef float float_t;
204 typedef double double_t;
206 /*@constant double HUGE_VAL; @*/
207 /*@constant float HUGE_VALF; @*/
208 /*@constant long double HUGE_VALL; @*/
210 /*@constant float INFINITY; @*/
212 /*@constant float NAN; @*/
213 /*:warn implementationoptional "NAN is defined if and only if the implementation supports quiet float type NaNs.":*/ ;
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;@*/
221 /*@constant int FP_ILOGB0;@*/
222 /*@constant int FP_ILOGBNAN;@*/
224 /*@constant int DECIMAL_DIG;@*/
226 /* Defined for specs only - this type is any real type */
227 typedef float /*@alt double, long double@*/ s_real_t;
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) /*@*/ ;
237 ** math functions that may have a range error modify errno (implementation defined).
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) /*@*/ ;
245 double cos (double x) /*@*/ ;
246 double sin (double x) /*@*/ ;
247 double tan (double x) /*@*/ ;
249 double cosh (double x) /*@modifies errno@*/ ;
250 double sinh (double x) /*@modifies errno@*/ ;
251 double tanh (double x) /*@*/ ;
253 double acosh (double x) /*@modifies errno@*/ ;
254 double asinh (double x) /*@modifies errno@*/ ;
255 double atanh (double x) /*@modifies errno@*/ ;
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@*/ ;
261 double log (double x) /*@modifies errno@*/ ;
262 double log10 (double x) /*@modifies errno@*/ ;
264 double modf (double x, /*@out@*/ double *ip) /*@modifies *ip;@*/ ;
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@*/ ;
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@*/ ;
276 int ilogb (double x) /*@modifies errno@*/ ;
277 int ilogbf (float x) /*@modifies errno@*/ ;
278 int ilogbl (long double x) /*@modifies errno@*/ ;
280 double fabs (double x) /*@*/ ;
281 float fabsf (float x) /*@*/ ;
282 long double fabsl (long double x) /*@*/ ;
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@*/ ;
288 double sqrt (double x) /*@modifies errno@*/ ;
289 float sqrtf(float x) /*@modifies errno@*/ ;
290 long double sqrtl (long double x) /*@modifies errno@*/ ;
292 double cbrt (double x) /*@*/ ;
293 float cbrtf (float x) /*@*/ ;
294 long double cbrtl (long double x) /*@*/ ;
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@*/ ;
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) /*@*/ ;
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@*/ ;
314 double ceil (double x) /*@*/ ;
315 float ceilf(float x) /*@*/ ;
316 long double ceill(long double x) /*@*/ ;
318 double floor (double x) /*@*/ ;
319 float floorf (float x) /*@*/ ;
320 long double floorl (long double x) /*@*/ ;
322 double nearbyint (double x) /*@*/ ;
323 float nearbyintf (float x) /*@*/ ;
324 long double nearbyintl (long double x) /*@*/ ;
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@*/ ;
336 double round (double x) /*@*/ ;
337 long int lround (double x) /*@modifies errno@*/ ;
338 long long llround (double x) /*@modifies errno@*/ ;
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) /*@*/ ;
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) /*@*/ ;
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) /*@*/ ;
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.
367 # ifdef OPTIONAL_MATH
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) /*@*/ ;
420 typedef /*@abstract@*/ /*@mutable@*/ void *jmp_buf;
422 int setjmp (/*@out@*/ jmp_buf env) /*@modifies env;@*/ ;
423 /*@mayexit@*/ void longjmp (jmp_buf env, int val) /*@*/ ;
429 /*@constant int SIGABRT; @*/
430 /*@constant int SIGFPE; @*/
431 /*@constant int SIGILL; @*/
432 /*@constant int SIGINT; @*/
433 /*@constant int SIGSEGV; @*/
434 /*@constant int SIGTERM; @*/
436 typedef /*@integraltype@*/ sig_atomic_t;
438 /*@constant void (*SIG_DFL)(int); @*/
439 /*@constant void (*SIG_ERR)(int); @*/
440 /*@constant void (*SIG_IGN)(int); @*/
443 ** signal takes an int, and a function takes int returns void, and
444 ** returns the function (or NULL if unsuccessful).
447 /*@null@*/ void (*signal (int sig, /*@null@*/ void (*func)(int))) (int)
448 /*@modifies internalState, errno;@*/ ;
450 /*@mayexit@*/ int raise (int sig) ;
456 typedef /*@abstract@*/ /*@mutable@*/ void *va_list;
458 void va_start (/*@out@*/ va_list ap, ...) /*@modifies ap;@*/ ;
459 void va_end (va_list va) /*@modifies va;@*/ ;
469 typedef /*@abstract@*/ /*@mutable@*/ void *FILE;
470 typedef /*@abstract@*/ /*@mutable@*/ void *fpos_t;
472 /*@constant size_t _IOFBF; @*/
473 /*@constant size_t _IOLBF; @*/
474 /*@constant size_t _IONBF; @*/
476 /*@constant size_t BUFSIZ; @*/ /* evans 2002-02-27 change suggested by Walter Briscoe */
478 /*@constant int EOF; @*/
480 /*@constant int FOPEN_MAX; @*/
481 /*@constant int FILENAME_MAX; @*/
483 /*@constant int L_tmpnam; @*/
485 /*@constant int SEEK_CUR; @*/
486 /*@constant int SEEK_END; @*/
487 /*@constant int SEEK_SET; @*/
489 /*@constant int TMP_MAX; @*/
492 /*@checked@*/ FILE *stderr;
493 /*@checked@*/ FILE *stdin;
494 /*@checked@*/ FILE *stdout;
496 /*@unchecked@*/ FILE *stderr;
497 /*@unchecked@*/ FILE *stdin;
498 /*@unchecked@*/ FILE *stdout;
501 int remove (char *filename) /*@modifies fileSystem, errno@*/ ;
502 int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ;
504 /*@dependent@*/ /*@null@*/ FILE *tmpfile (void)
505 /*@modifies fileSystem, errno@*/ ;
507 /*@observer@*/ char *
508 tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s)
509 /*@modifies *s, internalState@*/ ;
511 int fclose (FILE *stream)
512 /*@modifies *stream, errno, fileSystem;@*/ ;
514 int fflush (/*@null@*/ FILE *stream)
515 /*@modifies *stream, errno, fileSystem;@*/ ;
517 /*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode)
518 /*@modifies fileSystem@*/ ;
520 /*@dependent@*/ /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream)
521 /*@modifies *stream, fileSystem, errno@*/ ;
523 extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf)
524 /*@modifies fileSystem, *stream, *buf@*/ ;
526 extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf,
527 int mode, size_t size)
528 /*@modifies fileSystem, *stream, *buf@*/ ;
532 int fprintf (FILE *stream, char *format, ...)
533 /*@modifies fileSystem, *stream@*/ ;
536 int /*@alt void@*/ fprintf (FILE *stream, char *format, ...)
537 /*@modifies fileSystem, *stream@*/ ;
541 int fscanf (FILE *stream, char *format, ...)
542 /*@modifies fileSystem, *stream@*/ ;
546 int printf (char *format, ...)
548 /*@modifies fileSystem, *stdout@*/ ;
551 int /*@alt void@*/ printf (char *format, ...)
553 /*@modifies fileSystem, *stdout@*/ ;
557 int scanf(char *format, ...)
559 /*@modifies fileSystem, *stdin@*/ ;
563 int sprintf (/*@out@*/ char *s, char *format, ...)
567 int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...)
572 int sscanf (/*@out@*/ char *s, char *format, ...) /*@*/ ;
573 /* modifies extra arguments */
575 int vprintf (const char *format, va_list arg)
577 /*@modifies fileSystem, *stdout@*/ ;
579 int vfprintf (FILE *stream, char *format, va_list arg)
580 /*@modifies fileSystem, *stream, arg, errno@*/ ;
582 int vsprintf (/*@out@*/ char *str, const char *format, va_list ap)
583 /*@warn bufferoverflowhigh "Use vsnprintf instead"@*/
586 int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap)
587 /*@requires maxSet(str) >= size@*/
590 int fgetc (FILE *stream)
591 /*@modifies fileSystem, *stream, errno@*/ ;
594 fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream)
595 /*@modifies fileSystem, *s, *stream, errno@*/
596 /*@requires maxSet(s) >= (n -1); @*/
597 /*@ensures maxRead(s) <= (n -1) /\ maxRead(s) >= 0; @*/
600 int fputc (int /*@alt char@*/ c, FILE *stream)
602 /*@modifies fileSystem, *stream, errno@*/ ;
604 int fputs (char *s, FILE *stream)
605 /*@modifies fileSystem, *stream@*/ ;
607 /* note use of sef --- stream may be evaluated more than once */
608 int getc (/*@sef@*/ FILE *stream)
609 /*@modifies fileSystem, *stream@*/ ;
611 int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/ ;
613 /*@null@*/ char *gets (/*@out@*/ char *s)
614 /*@warn bufferoverflowhigh
615 "Use of gets leads to a buffer overflow vulnerability. Use fgets instead"@*/
616 /*@globals stdin@*/ /*@modifies fileSystem, *s, *stdin, errno@*/ ;
618 int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
620 /*@modifies fileSystem, *stream;@*/ ;
622 int putchar (int /*@alt char@*/ c)
624 /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ;
626 int puts (const char *s)
629 /*@modifies fileSystem, *stdout@*/ ;
631 int ungetc (int /*@alt char@*/ c, FILE *stream)
632 /*@modifies fileSystem, *stream, errno@*/ ;
635 fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream)
636 /*@modifies fileSystem, *ptr, *stream, errno@*/ ;
638 size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream)
639 /*@modifies fileSystem, *stream, errno@*/ ;
641 int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos)
642 /*@modifies *pos, errno@*/ ;
644 int fseek (FILE *stream, long int offset, int whence)
646 /*@modifies fileSystem, *stream, errno@*/ ;
648 int fsetpos (FILE *stream, fpos_t *pos)
649 /*@modifies fileSystem, *stream, errno@*/ ;
651 long int ftell(FILE *stream)
652 /*:errorcode -1:*/ /*@modifies errno*/ ;
654 void rewind (FILE *stream) /*@modifies *stream@*/ ;
655 void clearerr (FILE *stream) /*@modifies *stream@*/ ;
657 int feof (FILE *stream) /*@modifies errno@*/ ;
659 int ferror (FILE *stream) /*@modifies errno@*/ ;
661 void perror (/*@null@*/ char *s)
662 /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ;
668 double atof (char *s) /*@*/ ;
669 int atoi (char *s) /*@*/ ;
670 long int atol (char *s) /*@*/ ;
672 double strtod (char *s, /*@null@*/ /*@out@*/ char **endp)
673 /*@modifies *endp, errno@*/ ;
675 long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
676 /*@modifies *endp, errno@*/ ;
679 strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
680 /*@modifies *endp, errno@*/ ;
682 /*@constant int RAND_MAX; @*/
683 int rand (void) /*@modifies internalState@*/ ;
684 void srand (unsigned int seed) /*@modifies internalState@*/ ;
691 /*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/
692 /*@ensures maxSet(result) == (nobj - 1); @*/ ;
693 /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@*/
694 /*@ensures maxSet(result) == (size - 1); @*/ ;
698 /* 11 June 1997: removed out on return value */
701 /*@null@*/ /*@only@*/ void *
702 realloc (/*@null@*/ /*@only@*/ /*@special@*/ void *p,
703 size_t size) /*@releases p@*/ /*@modifies *p@*/
704 /*@ensures maxSet(result) == (size - 1) @*/;
708 ** LCLint annotations cannot fully describe realloc. The semantics we
710 ** realloc returns null: ownership of parameter is not changed
711 ** realloc returns non-null: ownership of parameter is transferred to return value
713 ** Otherwise, storage is in the same state before and after the call.
716 /*@null@*/ /*@only@*/ void *
717 realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size)
718 /*@modifies *p@*/ /*@ensures maxSet(result) >= (size - 1) @*/;
720 void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies p@*/ ;
722 /*@constant int EXIT_FAILURE; @*/
723 /*@constant int EXIT_SUCCESS; @*/
725 /*@exits@*/ void abort (void) /*@*/ ;
726 /*@exits@*/ void exit (int status) /*@*/ ;
727 int atexit (void (*func)(void)) /*@modifies internalState@*/ ;
729 /*@observer@*/ /*@null@*/ char *getenv (char *name) /*@*/ ;
731 int system (/*@null@*/ char *s) /*@modifies fileSystem@*/ ;
733 /*@null@*/ /*@dependent@*/ void *
734 bsearch (void *key, void *base,
735 size_t n, size_t size,
736 int (*compar)(void *, void *)) /*@*/ ;
738 void qsort (void *base, size_t n, size_t size,
739 int (*compar)(void *, void *))
740 /*@modifies *base, errno@*/ ;
742 int abs (int n) /*@*/ ;
744 typedef /*@concrete@*/ struct
750 div_t div (int num, int denom) /*@*/ ;
752 long int labs (long int n) /*@*/ ;
754 typedef /*@concrete@*/ struct
760 ldiv_t ldiv (long num, long denom) /*@*/ ;
762 /*@constant size_t MB_CUR_MAX; @*/
765 ** wchar_t and wint_t functions added by Amendment 1 to ISO.
768 /*@constant int WCHAR_MAX@*/
769 /*@constant int WCHAR_MIN@*/
770 /*@constant wint_t WEOF@*/
772 wint_t btowc (int c) /*@*/ ;
774 wint_t fgetwc (FILE *fp) /*@modifies fileSystem, *fp*/ ;
776 /*@null@*/ wchar_t *fgetws (/*@returned@*/ wchar_t *s, int n, FILE *stream)
777 /*@modifies fileSystem, *s, *stream@*/;
779 wint_t fputwc (wchar_t c, FILE *stream)
780 /*@modifies fileSystem, *stream@*/;
782 int fputws (const wchar_t *s, FILE *stream)
783 /*@modifies fileSystem, *stream@*/ ;
785 int fwide (FILE *stream, int mode) /*@*/ ;
786 /* does not modify the stream */
788 /*@printflike@*/ int fwprintf (FILE *stream, const wchar_t *format, ...)
789 /*@modifies *stream, fileSystem@*/ ;
791 /*@scanflike@*/ int fwscanf (FILE *stream, const wchar_t *format, ...)
792 /*@modifies *stream, fileSystem@*/ ;
794 /* note use of sef --- stream may be evaluated more than once */
795 wint_t getwc (/*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ;
797 wint_t getwchar (void) /*@modifies fileSystem, *stdin@*/;
799 size_t mbrlen (const char *s, size_t n, /*@null@*/ mbstate_t *ps) /*@*/ ;
801 size_t mbrtowc (/*@null@*/ wchar_t *pwc, const char *s, size_t n,
802 /*@null@*/ mbstate_t *ps)
803 /*@modifies *pwc@*/ ;
805 int mbsinit (/*@null@*/ const mbstate_t *ps) /*@*/ ;
807 size_t mbsrtowcs (/*@null@*/ wchar_t *dst, const char **src, size_t len,
808 /*@null@*/ mbstate_t *ps)
809 /*@modifies *dst@*/ ;
811 /* note use of sef --- stream may be evaluated more than once */
812 wint_t putwc (wchar_t c, /*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ;
814 wint_t putwchar (wchar_t c) /*@modifies fileSystem, *stdout@*/ ;
816 /*@printflike@*/ int swprintf (wchar_t *s, size_t n, const wchar_t *format, ...)
819 /*@scanflike@*/ int swscanf (const wchar_t *s, const wchar_t *format, ...)
820 /*@modifies *stdin@*/ ;
822 wint_t ungetwc (wint_t c, FILE *stream) /*@modifies fileSystem, *stream@*/ ;
824 int vfwprintf (FILE *stream, const wchar_t *format, va_list arg)
825 /*@modifies fileSystem, *stream@*/ ;
827 int vswprintf (wchar_t *s, size_t n, const wchar_t *format, va_list arg)
830 int vwprintf (const wchar_t *format, va_list arg)
831 /*@modifies fileSystem, *stdout@*/ ;
833 size_t wcrtomb (/*@null@*/ /*@out@*/ char *s, wchar_t wc, /*@null@*/ mbstate_t *ps)
836 void /*@alt wchar_t *@*/
837 wcscat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2)
840 /*@exposed@*/ /*@null@*/ wchar_t *
841 wcschr (/*@returned@*/ const wchar_t *s, wchar_t c)
844 int wcscmp (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
846 int wcscoll (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
848 void /*@alt wchar_t *@*/
849 wcscpy (/*@unique@*/ /*@out@*/ /*@returned@*/ wchar_t *s1, const wchar_t *s2)
852 size_t wcscspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
854 size_t wcsftime (/*@out@*/ wchar_t *s, size_t maxsize, const wchar_t *format,
855 const struct tm *timeptr)
858 size_t wcslen (const wchar_t *s) /*@*/ ;
860 void /*@alt wchar_t *@*/
861 wcsncat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
865 int wcsncmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
867 void /*@alt wchar_t *@*/
868 wcsncpy (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
873 wcspbrk (/*@returned@*/ const wchar_t *s1, const wchar_t *s2)
877 wcsrchr (/*@returned@*/ const wchar_t *s, wchar_t c)
881 wcsrtombs (/*@null@*/ char *dst, const wchar_t **src, size_t len,
882 /*@null@*/ mbstate_t *ps)
883 /*@modifies *src@*/ ;
885 size_t wcsspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
887 /*@null@*/ wchar_t *wcsstr (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
889 double wcstod (const wchar_t *nptr, /*@null@*/ wchar_t **endptr)
890 /*@modifies *endptr@*/ ;
893 wcstok (/*@null@*/ wchar_t *s1, const wchar_t *s2, wchar_t **ptr)
896 long wcstol (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
897 /*@modifies *endptr@*/;
900 wcstoul (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
901 /*@modifies *endptr@*/;
904 wcsxfrm (/*@null@*/ wchar_t *s1, const wchar_t *s2, size_t n)
907 int wctob (wint_t c) /*@*/;
909 /*@null@*/ wchar_t *wmemchr (const wchar_t *s, wchar_t c, size_t n) /*@*/ ;
911 int wmemcmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
913 wchar_t *wmemcpy (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
916 wchar_t *wmemmove (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
919 wchar_t *wmemset (/*@returned@*/ wchar_t *s, wchar_t c, size_t n)
922 /*@printflike@*/ int wprintf (const wchar_t *format, ...)
923 /*@globals stdout@*/ /*@modifies errno, *stdout@*/;
926 wscanf (const wchar_t *format, ...)
927 /*@globals stdin@*/ /*@modifies errno, *stdin@*/;
930 ** wctype.h (added by Amendment 1)
933 /* Warning: not sure about these (maybe abstract?): */
934 typedef /*@integraltype@*/ wctype_t;
935 typedef /*@integraltype@*/ wctrans_t;
938 lltX_bool iswalnum (wint_t c) /*@*/ ;
939 lltX_bool iswalpha (wint_t c) /*@*/ ;
940 lltX_bool iswcntrl (wint_t c) /*@*/ ;
941 lltX_bool iswctype (wint_t c, wctype_t ctg) /*@*/ ;
942 lltX_bool iswdigit (wint_t c) /*@*/ ;
943 lltX_bool iswgraph (wint_t c) /*@*/ ;
944 lltX_bool iswlower (wint_t c) /*@*/ ;
945 lltX_bool iswprint (wint_t c) /*@*/ ;
946 lltX_bool iswpunct (wint_t c) /*@*/ ;
947 lltX_bool iswspace (wint_t c) /*@*/ ;
948 lltX_bool iswupper (wint_t c) /*@*/ ;
949 lltX_bool iswxdigit (wint_t c) /*@*/ ;
951 wint_t towctrans (wint_t c, wctrans_t ctg) /*@*/ ;
952 wint_t towlower (wint_t c) /*@*/ ;
953 wint_t towupper (wint_t c) /*@*/ ;
955 lltX_bool /*@alt int@*/ iswalnum (wint_t c) /*@*/ ;
956 lltX_bool /*@alt int@*/ iswalpha (wint_t c) /*@*/ ;
957 lltX_bool /*@alt int@*/ iswcntrl (wint_t c) /*@*/ ;
958 lltX_bool /*@alt int@*/ iswctype (wint_t c, wctype_t ctg) /*@*/ ;
959 lltX_bool /*@alt int@*/ iswdigit (wint_t c) /*@*/ ;
960 lltX_bool /*@alt int@*/ iswgraph (wint_t c) /*@*/ ;
961 lltX_bool /*@alt int@*/ iswlower (wint_t c) /*@*/ ;
962 lltX_bool /*@alt int@*/ iswprint (wint_t c) /*@*/ ;
963 lltX_bool /*@alt int@*/ iswpunct (wint_t c) /*@*/ ;
964 lltX_bool /*@alt int@*/ iswspace (wint_t c) /*@*/ ;
965 lltX_bool /*@alt int@*/ iswupper (wint_t c) /*@*/ ;
966 lltX_bool /*@alt int@*/ iswxdigit (wint_t c) /*@*/ ;
968 wint_t /*@alt int@*/ towctrans (wint_t c, wctrans_t ctg) /*@*/ ;
969 wint_t /*@alt int@*/ towlower (wint_t c) /*@*/ ;
970 wint_t /*@alt int@*/ towupper (wint_t c) /*@*/ ;
973 wctrans_t wctrans (const char *property) /*@*/ ;
974 wctype_t wctype (const char *property) /*@*/ ;
976 int mblen (char *s, size_t n) /*@*/ ;
977 int mbtowc (/*@null@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n)
978 /*@modifies *pwc@*/ ;
979 int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar)
981 size_t mbstowcs (/*@out@*/ wchar_t *pwcs, char *s, size_t n)
982 /*@modifies *pwcs@*/ ;
983 size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n)
990 void /*@alt void * @*/
991 memcpy (/*@unique@*/ /*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
993 /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
996 void /*@alt void * @*/
997 memmove (/*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
999 /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
1007 void /*@alt char * @*/
1008 strcpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2)
1010 /*@requires maxSet(s1) >= maxRead(s2) @*/
1011 /*@ensures maxRead(s1) == maxRead (s2) /\ maxRead(result) == maxRead(s2) /\ maxSet(result) == maxSet(s1); @*/;
1013 void /*@alt char * @*/
1014 strncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2, size_t n)
1016 /*@requires maxSet(s1) >= ( n - 1 ); @*/
1017 /*@ensures maxRead (s2) >= maxRead(s1) /\ maxRead (s1) <= n; @*/ ;
1019 void /*@alt char * @*/
1020 strcat (/*@unique@*/ /*@returned@*/ char *s1, char *s2)
1021 /*@modifies *s1@*/ /*@requires maxSet(s1) >= (maxRead(s1) + maxRead(s2) );@*/
1022 /*@ensures maxRead(result) == (maxRead(s1) + maxRead(s2) );@*/;
1024 void /*@alt char * @*/
1025 strncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, size_t n)
1027 /*@requires maxSet(s1) >= ( maxRead(s1) + n); @*/
1028 /*@ensures maxRead(s1) >= (maxRead(s1) + n); @*/;
1032 int memcmp (void *s1, void *s2, size_t n) /*@*/ ;
1033 int strcmp (char *s1, char *s2) /*@*/ ;
1034 int strcoll (char *s1, char *s2) /*@*/ ;
1035 int strncmp (char *s1, char *s2, size_t n) /*@*/ ;
1036 size_t strxfrm (/*@out@*/ /*@null@*/ char *s1, char *s2, size_t n)
1037 /*@modifies *s1@*/ ; /* s1 may be null only if n == 0 */
1039 /*@null@*/ void *memchr (void *s, int c, size_t n) /*@*/ ;
1042 /*@exposed@*/ /*@null@*/ char *
1043 strchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
1045 /*@exposed@*/ /*@null@*/ char *
1046 strchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0; @*/ ;
1049 size_t strcspn (char *s1, char *s2) /*@*/ ;
1050 /*@null@*/ /*@exposed@*/ char *
1051 strpbrk (/*@returned@*/ char *s, char *t) /*@*/ ;
1054 /*@null@*/ /*@exposed@*/ char *
1055 strrchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
1057 /*@null@*/ /*@exposed@*/ char *
1058 strrchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
1061 size_t strspn (char *s, char *t) /*@*/ ;
1063 /*@null@*/ /*@exposed@*/ char *
1064 strstr (/*@returned@*/ const char *s, const char *t) /*@*/
1065 /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 /\ maxRead(result) >= maxRead(t) /\ maxSet(result) >= maxRead(t)@*/ ;
1067 /*@null@*/ /*@exposed@*/ char *
1068 strtok (/*@returned@*/ /*@null@*/ char *s, char *t)
1069 /*@modifies *s, internalState, errno@*/ ;
1071 void /*@alt void *@*/ memset (/*@out@*/ /*@returned@*/ void *s,
1073 /*@modifies *s@*/ /*@requires maxSet(s) >= (n - 1) @*/ /*@ensures maxRead(s) >= (n - 1) @*/ ;
1075 /*@observer@*/ char *strerror (int errnum) /*@*/ ;
1078 size_t strlen (char *s) /*@*/ /*@ensures result == maxRead(s); @*/;
1084 /*@constant int CLOCKS_PER_SEC;@*/
1086 typedef /*@integraltype@*/ clock_t;
1087 typedef /*@integraltype@*/ time_t;
1102 clock_t clock (void) /*@modifies internalState@*/ ;
1103 double difftime (time_t time1, time_t time0) /*@*/ ;
1104 time_t mktime (struct tm *timeptr) /*@*/ ;
1106 time_t time (/*@null@*/ /*@out@*/ time_t *tp)
1107 /*@modifies *tp@*/ ;
1109 /*@observer@*/ char *asctime (struct tm *timeptr)
1110 /*@modifies errno*/ /*@ensures maxSet(result) == 25 /\ maxRead(result) == 25; @*/ ;
1112 /*@observer@*/ char *ctime (time_t *tp) /*@*/
1113 /*@ensures maxSet(result) == 25 /\ maxRead(result) == 25; @*/;
1115 /*@null@*/ /*@observer@*/ struct tm *gmtime (time_t *tp) /*@*/ ;
1117 /*@null@*/ /*@observer@*/ struct tm *localtime (time_t *tp)
1118 /*@modifies errno@*/ ;
1120 size_t strftime (/*@out@*/ char *s, size_t smax,
1121 char *fmt, struct tm *timeptr)
1125 ** ISO c99: 7.18 Integer types <stdint.h>
1129 ** These types are OPTIONAL. Provide warnings on use.
1132 typedef /*@integraltype@*/ int8_t
1133 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least8_t instead."@*/ ;
1135 typedef /*@integraltype@*/ int16_t
1136 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least16_t instead."@*/ ;
1138 typedef /*@integraltype@*/ int32_t
1139 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least32_t instead."@*/ ;
1141 typedef /*@integraltype@*/ int64_t
1142 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least64_t instead."@*/ ;
1144 typedef /*@unsignedintegraltype@*/ uint8_t
1145 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least8_t instead."@*/ ;
1147 typedef /*@unsignedintegraltype@*/ uint16_t
1148 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least16_t instead."@*/ ;
1150 typedef /*@unsignedintegraltype@*/ uint32_t
1151 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least32_t instead."@*/ ;
1153 typedef /*@unsignedintegraltype@*/ uint64_t
1154 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least64_t instead."@*/ ;
1156 typedef /*@integraltype@*/ int_least8_t;
1157 typedef /*@integraltype@*/ int_least16_t;
1158 typedef /*@integraltype@*/ int_least32_t;
1159 typedef /*@integraltype@*/ int_least64_t;
1161 typedef /*@unsignedintegraltype@*/ uint_least8_t;
1162 typedef /*@unsignedintegraltype@*/ uint_least16_t;
1163 typedef /*@unsignedintegraltype@*/ uint_least32_t;
1164 typedef /*@unsignedintegraltype@*/ uint_least64_t;
1166 typedef /*@integraltype@*/ int_fast8_t;
1167 typedef /*@integraltype@*/ int_fast16_t;
1168 typedef /*@integraltype@*/ int_fast32_t;
1169 typedef /*@integraltype@*/ int_fast64_t;
1171 typedef /*@unsignedintegraltype@*/ uint_fast8_t;
1172 typedef /*@unsignedintegraltype@*/ uint_fast16_t;
1173 typedef /*@unsignedintegraltype@*/ uint_fast32_t;
1174 typedef /*@unsignedintegraltype@*/ uint_fast64_t;
1176 typedef int *intptr_t
1177 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;
1179 typedef unsigned int *uintptr_t
1180 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;
1182 typedef /*@signedintegraltype@*/ intmax_t;
1183 typedef /*@unsignedintegraltype@*/ uintmax_t;
1186 ** What should the types be here?
1189 /*@constant int INT8_MIN@*/
1190 /*@constant int INT16_MIN@*/
1191 /*@constant int INT32_MIN@*/
1192 /*@constant int INT64_MIN@*/
1194 /*@constant int INT8_MAX@*/
1195 /*@constant int INT16_MAX@*/
1196 /*@constant int INT32_MAX@*/
1197 /*@constant int INT64_MAX@*/
1199 /*@constant int UINT8_MIN@*/
1200 /*@constant int UINT16_MIN@*/
1201 /*@constant int UINT32_MIN@*/
1202 /*@constant int UINT64_MIN@*/
1204 /*@constant int INT_LEAST8_MIN@*/
1205 /*@constant int INT_LEAST16_MIN@*/
1206 /*@constant int INT_LEAST32_MIN@*/
1207 /*@constant int INT_LEAST64_MIN@*/
1209 /*@constant int INT_LEAST8_MAX@*/
1210 /*@constant int INT_LEAST16_MAX@*/
1211 /*@constant int INT_LEAST32_MAX@*/
1212 /*@constant int INT_LEAST64_MAX@*/
1214 /*@constant int UINT_LEAST8_MAX@*/
1215 /*@constant int UINT_LEAST16_MAX@*/
1216 /*@constant int UINT_LEAST32_MAX@*/
1217 /*@constant int UINT_LEAST64_MAX@*/
1219 /*@constant int INT_FAST8_MIN@*/
1220 /*@constant int INT_FAST16_MIN@*/
1221 /*@constant int INT_FAST32_MIN@*/
1222 /*@constant int INT_FAST64_MIN@*/
1224 /*@constant int INT_FAST8_MAX@*/
1225 /*@constant int INT_FAST16_MAX@*/
1226 /*@constant int INT_FAST32_MAX@*/
1227 /*@constant int INT_FAST64_MAX@*/
1229 /*@constant int UINT_FAST8_MAX@*/
1230 /*@constant int UINT_FAST16_MAX@*/
1231 /*@constant int UINT_FAST32_MAX@*/
1232 /*@constant int UINT_FAST64_MAX@*/
1234 /*@constant size_t INTPTR_MIN@*/
1235 /*@constant size_t INTPTR_MAX@*/