2 ** ansi.h --- LCLint Standard C Library
4 ** Process with -DSTRICT to get strict library.
9 /*@+globsimpmodifiesnothing@*/
15 /*@constant int EDOM;@*/
16 /*@constant int ERANGE;@*/
17 /*@constant int EILSEQ;@*/
20 /*@checkedstrict@*/ extern int errno;
22 /*@unchecked@*/ extern 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 extern /*@falseexit@*/ void assert (/*@sef@*/ lltX_bool e)
53 extern /*@falseexit@*/ void assert (/*@sef@*/ lltX_bool /*@alt int@*/ e)
63 extern lltX_bool isalnum (int c) /*@*/ ;
64 extern lltX_bool isalpha (int c) /*@*/ ;
65 extern lltX_bool iscntrl (int c) /*@*/ ;
66 extern lltX_bool isdigit (int c) /*@*/ ;
67 extern lltX_bool isgraph (int c) /*@*/ ;
68 extern lltX_bool islower (int c) /*@*/ ;
69 extern lltX_bool isprint (int c) /*@*/ ;
70 extern lltX_bool ispunct (int c) /*@*/ ;
71 extern lltX_bool isspace (int c) /*@*/ ;
72 extern lltX_bool isupper (int c) /*@*/ ;
73 extern lltX_bool isxdigit (int c) /*@*/ ;
74 extern char tolower (int c) /*@*/ ;
75 extern char toupper (int c) /*@*/ ;
77 extern lltX_bool /*@alt int@*/ isalnum (int /*@alt unsigned char@*/ c) /*@*/ ;
78 extern lltX_bool /*@alt int@*/ isalpha (int /*@alt unsigned char@*/ c) /*@*/ ;
79 extern lltX_bool /*@alt int@*/ iscntrl (int /*@alt unsigned char@*/ c) /*@*/ ;
80 extern lltX_bool /*@alt int@*/ isdigit (int /*@alt unsigned char@*/ c) /*@*/ ;
81 extern lltX_bool /*@alt int@*/ isgraph (int /*@alt unsigned char@*/ c) /*@*/ ;
82 extern lltX_bool /*@alt int@*/ islower (int /*@alt unsigned char@*/ c) /*@*/ ;
83 extern lltX_bool /*@alt int@*/ isprint (int /*@alt unsigned char@*/ c) /*@*/ ;
84 extern lltX_bool /*@alt int@*/ ispunct (int /*@alt unsigned char@*/ c) /*@*/ ;
85 extern lltX_bool /*@alt int@*/ isspace (int /*@alt unsigned char@*/ c) /*@*/ ;
86 extern lltX_bool /*@alt int@*/ isupper (int /*@alt unsigned char@*/ c) /*@*/ ;
87 extern lltX_bool /*@alt int@*/ isxdigit (int /*@alt unsigned char@*/ c) /*@*/ ;
88 extern char /*@alt int@*/ tolower (int /*@alt unsigned char@*/ c) /*@*/ ;
89 extern char /*@alt int@*/ toupper (int /*@alt unsigned char@*/ c) /*@*/ ;
101 char *int_curr_symbol;
102 char *currency_symbol;
103 char *mon_decimal_point;
104 char *mon_thousands_sep;
108 char int_frac_digits;
118 /*@constant int LC_ALL;@*/
119 /*@constant int LC_COLLATE;@*/
120 /*@constant int LC_CTYPE;@*/
121 /*@constant int LC_MONETARY;@*/
122 /*@constant int LC_NUMERIC;@*/
123 /*@constant int LC_TIME;@*/
125 extern /*@observer@*/ /*@null@*/ char *setlocale (int category, /*@null@*/ char *locale)
126 /*@modifies internalState, errno@*/ ;
128 extern struct lconv *localeconv (void) /*@*/ ;
135 ** Note, these are defined by macros, but NOT necessarily
136 ** constants. They may be used as lvalues.
139 /*@unchecked@*/ extern int DBL_DIG;
140 /*@unchecked@*/ extern double DBL_EPSILON;
141 /*@unchecked@*/ extern int DBL_MANT_DIG;
142 /*@unchecked@*/ extern double DBL_MAX;
143 /*@unchecked@*/ extern int DBL_MAX_10_EXP;
144 /*@unchecked@*/ extern int DBL_MAX_EXP;
145 /*@unchecked@*/ extern double DBL_MIN;
146 /*@unchecked@*/ extern int DBL_MIN_10_EXP;
147 /*@unchecked@*/ extern int DBL_MIN_EXP;
149 /*@unchecked@*/ extern int FLT_DIG;
150 /*@unchecked@*/ extern float FLT_EPSILON;
151 /*@unchecked@*/ extern int FLT_MANT_DIG;
152 /*@unchecked@*/ extern float FLT_MAX;
153 /*@unchecked@*/ extern int FLT_MAX_10_EXP;
154 /*@unchecked@*/ extern int FLT_MAX_EXP;
155 /*@unchecked@*/ extern float FLT_MIN;
156 /*@unchecked@*/ extern int FLT_MIN_10_EXP;
157 /*@unchecked@*/ extern int FLT_MIN_EXP;
158 /*@constant int FLT_RADIX@*/
159 /*@unchecked@*/ extern int FLT_ROUNDS;
161 /*@unchecked@*/ extern int LDBL_DIG;
162 /*@unchecked@*/ extern long double LDBL_EPSILON;
163 /*@unchecked@*/ extern int LDBL_MANT_DIG;
164 /*@unchecked@*/ extern long double LDBL_MAX;
165 /*@unchecked@*/ extern int LDBL_MAX_10_EXP;
166 /*@unchecked@*/ extern int LDBL_MAX_EXP;
167 /*@unchecked@*/ extern long double LDBL_MIN;
168 /*@unchecked@*/ extern int LDBL_MIN_10_EXP;
169 /*@unchecked@*/ extern int LDBL_MIN_EXP;
175 /*@constant int CHAR_BIT; @*/
176 /*@constant char CHAR_MAX; @*/
177 /*@constant char CHAR_MIN; @*/
178 /*@constant int INT_MAX; @*/
179 /*@constant int INT_MIN; @*/
180 /*@constant long int LONG_MAX; @*/
181 /*@constant long int LONG_MIN; @*/
182 /*@constant long int MB_LEN_MAX@*/
183 /*@constant signed char SCHAR_MAX; @*/
184 /*@constant signed char SCHAR_MIN; @*/
185 /*@constant short SHRT_MAX; @*/
186 /*@constant short SHRT_MIN; @*/
187 /*@constant unsigned char UCHAR_MAX; @*/
188 /*@constant unsigned char UCHAR_MIN; @*/
189 /*@constant unsigned int UINT_MAX; @*/
190 /*@constant unsigned long ULONG_MAX; @*/
191 /*@constant unsigned short USHRT_MAX; @*/
197 /*@constant double HUGE_VAL; @*/
200 ** math functions that may have a range error modify errno
203 extern double sin (double x) /*@*/ ;
204 extern double cos (double x) /*@*/ ;
205 extern double tan (double x) /*@*/ ;
206 extern double asin (double x) /*@modifies errno@*/ ;
207 extern double acos (double x) /*@modifies errno@*/ ;
208 extern double atan (double x) /*@*/ ;
209 extern double atan2 (double y, double x) /*@*/ ;
210 extern double sinh (double x) /*@*/ ;
211 extern double cosh (double x) /*@modifies errno@*/ ;
212 extern double tanh (double x) /*@*/ ;
214 extern double exp (double x) /*@modifies errno@*/ ;
215 extern double ldexp (double x, int n) /*@modifies errno@*/ ;
216 extern double frexp (double x, /*@out@*/ int *xp) /*@modifies *xp;@*/ ;
218 extern double log (double x) /*@modifies errno@*/ ;
219 extern double log10 (double x) /*@modifies errno@*/ ;
221 extern double pow (double x, double y) /*@modifies errno@*/ ;
222 extern double sqrt (double x) /*@modifies errno@*/ ;
224 extern double ceil (double x) /*@*/ ;
225 extern double floor (double x) /*@*/ ;
226 extern double fabs (double x) /*@*/ ;
228 double modf (double x, /*@out@*/ double *ip) /*@modifies *ip;@*/ ;
229 double fmod (double x, double y) /*@*/ ;
232 ** These functions are optional in iso C. An implementation does not
233 ** have to provide them. They are included in comments here, but
234 ** are not required to be part of the standard library.
237 # ifdef OPTIONAL_MATH
239 extern float acosf (float x) /*@modifies errno@*/ ;
240 extern long double acosl (long double x) /*@modifies errno@*/ ;
241 extern float asinf (float x) /*@modifies errno@*/ ;
242 extern long double asinl (long double x) /*@modifies errno@*/ ;
243 extern float atanf (float x) /*@*/ ;
244 extern long double atanl (long double x) /*@*/ ;
245 extern float atan2f (float y, float x) /*@*/ ;
246 extern long double atan2l (long double y, long double x) /*@*/ ;
247 extern float ceilf (float x) /*@*/ ;
248 extern long double ceill (long double x) /*@*/ ;
249 extern float cosf (float x) /*@*/ ;
250 extern long double cosl (long double x) /*@*/ ;
251 extern float coshf (float x) /*@modifies errno@*/ ;
252 extern long double coshl (long double x) /*@modifies errno@*/ ;
253 extern float expf (float x) /*@modifies errno@*/ ;
254 extern long double expl (long double x) /*@modifies errno@*/;
255 extern float fabsf (float x) /*@*/ ;
256 extern long double fabsl (long double x) /*@*/ ;
257 extern float floorf (float x) /*@*/ ;
258 extern long double floorl (long double x) /*@*/ ;
259 extern float fmodf (float x, float y) /*@*/ ;
260 extern long double fmodl (long double x, long double y) /*@*/ ;
261 extern float frexpf (float x, /*@out@*/ int *xp) /*@modifies *xp@*/;
262 extern long double frexpl (long double x, /*@out@*/ int *xp) /*@modifies *xp@*/;
263 extern float ldexpf (float x, int n) /*@modifies errno@*/ ;
264 extern long double ldexpl (long double x, int n) /*@modifies errno@*/ ;
265 extern float logf (float x) /*@modifies errno@*/ ;
266 extern long double logl (long double x) /*@modifies errno@*/ ;
267 extern float log10f (float x) /*@modifies errno@*/;
268 extern long double log10l (long double x) /*@modifies errno@*/;
269 extern float modff (float x, /*@out@*/ float *xp) /*@modifies *xp@*/ ;
270 extern long double modfl (long double x, /*@out@*/ long double *xp) /*@modifies *xp@*/ ;
271 extern float powf (float x, float y) /*@modifies errno@*/ ;
272 extern long double powl (long double x, long double y) /*@modifies errno@*/ ;
273 extern float sinf (float x) /*@*/ ;
274 extern long double sinl (long double x) /*@*/ ;
275 extern float sinhf (float x) /*@*/ ;
276 extern long double sinhl (long double x) /*@*/ ;
277 extern float sqrtf (float x) /*@modifies errno@*/ ;
278 extern long double sqrtl (long double x) /*@modifies errno@*/ ;
279 extern float tanf (float x) /*@*/ ;
280 extern long double tanl (long double x) /*@*/ ;
281 extern float tanhf (float x) /*@*/ ;
282 extern long double tanhl (long double x) /*@*/ ;
290 typedef /*@abstract@*/ /*@mutable@*/ void *jmp_buf;
292 extern int setjmp (/*@out@*/ jmp_buf env) /*@modifies env;@*/ ;
293 extern /*@mayexit@*/ void longjmp (jmp_buf env, int val) /*@*/ ;
299 /*@constant int SIGABRT; @*/
300 /*@constant int SIGFPE; @*/
301 /*@constant int SIGILL; @*/
302 /*@constant int SIGINT; @*/
303 /*@constant int SIGSEGV; @*/
304 /*@constant int SIGTERM; @*/
306 typedef /*@integraltype@*/ sig_atomic_t;
308 /*@constant void (*SIG_DFL)(int); @*/
309 /*@constant void (*SIG_ERR)(int); @*/
310 /*@constant void (*SIG_IGN)(int); @*/
313 ** signal takes an int, and a function takes int returns void, and
314 ** returns the function (or NULL if unsuccessful).
317 extern /*@null@*/ void (*signal (int sig, /*@null@*/ void (*func)(int))) (int)
318 /*@modifies internalState, errno;@*/ ;
320 extern /*@mayexit@*/ int raise (int sig) ;
326 typedef /*@abstract@*/ /*@mutable@*/ void *va_list;
328 extern void va_start (/*@out@*/ va_list ap, ...) /*@modifies ap;@*/ ;
329 extern void va_end (va_list va) /*@modifies va;@*/ ;
339 typedef /*@abstract@*/ /*@mutable@*/ void *FILE;
340 typedef /*@abstract@*/ /*@mutable@*/ void *fpos_t;
342 /*@constant int _IOFBF; @*/
343 /*@constant int _IOLBF; @*/
344 /*@constant int _IONBF; @*/
346 /*@constant int BUFSIZ; @*/
347 /*@constant int EOF; @*/
349 /*@constant int FOPEN_MAX; @*/
350 /*@constant int FILENAME_MAX; @*/
352 /*@constant int L_tmpnam; @*/
354 /*@constant int SEEK_CUR; @*/
355 /*@constant int SEEK_END; @*/
356 /*@constant int SEEK_SET; @*/
358 /*@constant int TMP_MAX; @*/
361 /*@checked@*/ FILE *stderr;
362 /*@checked@*/ FILE *stdin;
363 /*@checked@*/ FILE *stdout;
365 /*@unchecked@*/ FILE *stderr;
366 /*@unchecked@*/ FILE *stdin;
367 /*@unchecked@*/ FILE *stdout;
370 extern int remove (char *filename) /*@modifies fileSystem, errno@*/ ;
371 extern int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ;
373 extern /*@null@*/ FILE *tmpfile (void) /*@modifies fileSystem@*/ ;
374 extern /*@observer@*/ char *
375 tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s)
376 /*@modifies *s, internalState@*/ ;
378 extern int fclose (FILE *stream) /*@modifies *stream, errno, fileSystem;@*/ ;
379 extern int fflush (/*@null@*/ FILE *stream)
380 /*@modifies *stream, errno, fileSystem;@*/ ;
382 extern /*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode)
383 /*@modifies fileSystem@*/ ;
385 extern /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream)
386 /*@modifies *stream, fileSystem, errno@*/ ;
388 extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf)
389 /*@modifies fileSystem, *stream, *buf@*/ ;
391 extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ char *buf,
392 int mode, size_t size)
393 /*@modifies fileSystem, *stream, *buf@*/ ;
397 extern int fprintf (FILE *stream, char *format, ...)
398 /*@modifies fileSystem, *stream@*/ ;
401 extern int /*@alt void@*/ fprintf (FILE *stream, char *format, ...)
402 /*@modifies fileSystem, *stream@*/ ;
406 extern int fscanf (FILE *stream, char *format, ...)
407 /*@modifies fileSystem, *stream@*/ ;
411 extern int printf (char *format, ...)
413 /*@modifies fileSystem, *stdout@*/ ;
416 extern int /*@alt void@*/ printf (char *format, ...)
418 /*@modifies fileSystem, *stdout@*/ ;
422 extern int scanf(char *format, ...)
424 /*@modifies fileSystem, *stdin@*/ ;
428 extern int sprintf (/*@out@*/ char *s, char *format, ...)
432 extern int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...)
437 int sscanf (/*@out@*/ char *s, char *format, ...) /*@*/ ;
438 /* modifies extra arguments */
440 int vprintf (const char *format, va_list arg)
442 /*@modifies fileSystem, *stdout@*/ ;
444 int vfprintf (FILE *stream, char *format, va_list arg)
445 /*@modifies fileSystem, *stream, arg, errno@*/ ;
447 int vsprintf (/*@out@*/ char *str, const char *format, va_list ap)
448 /*@warn bufferoverflowhigh "Use vsnprintf instead"@*/
451 int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap)
452 /*@requires maxSet(str) >= size@*/
455 extern int fgetc (FILE *stream)
456 /*@modifies fileSystem, *stream, errno@*/ ;
458 extern /*@null@*/ char *
459 fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream)
460 /*@modifies fileSystem, *s, *stream, errno@*/
461 /*@requires MaxSet(s) >= (n -1); @*/
462 /*@ensures MaxRead(s) <= (n -1) /\ MaxRead(s) >= 0; @*/
465 extern int fputc (int /*@alt char@*/ c, FILE *stream)
466 /*@modifies fileSystem, *stream, errno@*/ ;
468 extern int fputs (char *s, FILE *stream)
469 /*@modifies fileSystem, *stream@*/ ;
471 /* note use of sef --- stream may be evaluated more than once */
472 extern int getc (/*@sef@*/ FILE *stream)
473 /*@modifies fileSystem, *stream@*/ ;
475 extern int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/ ;
477 extern /*@null@*/ char *gets (/*@out@*/ char *s)
478 /*@warn bufferoverflowhigh
479 "Use of gets leads to a buffer overflow vulnerability. Use fgets instead"@*/
480 /*@globals stdin@*/ /*@modifies fileSystem, *s, *stdin, errno@*/ ;
482 extern int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
483 /*@modifies fileSystem, *stream;@*/ ;
485 extern int putchar (int /*@alt char@*/ c)
486 /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ;
488 extern int puts (const char *s)
489 /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ;
491 extern int ungetc (int /*@alt char@*/ c, FILE *stream)
492 /*@modifies fileSystem, *stream, errno@*/ ;
495 fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream)
496 /*@modifies fileSystem, *ptr, *stream, errno@*/ ;
498 extern size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream)
499 /*@modifies fileSystem, *stream, errno@*/ ;
501 extern int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos)
502 /*@modifies *pos, errno@*/ ;
504 extern int fseek (FILE *stream, long int offset, int whence)
505 /*@modifies fileSystem, *stream, errno@*/ ;
507 extern int fsetpos (FILE *stream, fpos_t *pos)
508 /*@modifies fileSystem, *stream, errno@*/ ;
510 extern long int ftell(FILE *stream) /*@modifies errno@*/ ;
512 extern void rewind (FILE *stream) /*@modifies *stream@*/ ;
513 extern void clearerr (FILE *stream) /*@modifies *stream@*/ ;
515 extern int feof (FILE *stream) /*@modifies errno@*/ ;
516 extern int ferror (FILE *stream) /*@modifies errno@*/ ;
518 extern void perror (/*@null@*/ char *s)
519 /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ;
525 extern double atof (char *s) /*@*/ ;
526 extern int atoi (char *s) /*@*/ ;
527 extern long int atol (char *s) /*@*/ ;
529 extern double strtod (char *s, /*@null@*/ /*@out@*/ char **endp)
530 /*@modifies *endp, errno@*/ ;
532 extern long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
533 /*@modifies *endp, errno@*/ ;
536 strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
537 /*@modifies *endp, errno@*/ ;
539 /*@constant int RAND_MAX; @*/
540 extern int rand (void) /*@modifies internalState@*/ ;
541 extern void srand (unsigned int seed) /*@modifies internalState@*/ ;
548 extern /*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/
549 /*@ensures MaxSet(result) == (nobj - 1); @*/ ;
550 extern /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@*/
551 /*@ensures MaxSet(result) == (size - 1); @*/ ;
555 /* 11 June 1997: removed out on return value */
558 extern /*@null@*/ /*@only@*/ void *
559 realloc (/*@null@*/ /*@only@*/ /*@special@*/ void *p,
560 size_t size) /*@releases p@*/ /*@modifies *p@*/
561 /*@ensures MaxSet(result) == (size - 1) @*/;
565 ** LCLint annotations cannot fully describe realloc. The semantics we
567 ** realloc returns null: ownership of parameter is not changed
568 ** realloc returns non-null: ownership of parameter is transferred to return value
570 ** Otherwise, storage is in the same state before and after the call.
573 extern /*@null@*/ /*@only@*/ void *
574 realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size)
575 /*@modifies *p@*/ /*@ensures MaxSet(result) >= (size - 1) @*/;
577 extern void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies p@*/ ;
579 /*@constant int EXIT_FAILURE; @*/
580 /*@constant int EXIT_SUCCESS; @*/
582 extern /*@exits@*/ void abort (void) /*@*/ ;
583 extern /*@exits@*/ void exit (int status) /*@*/ ;
584 extern int atexit (void (*func)(void)) /*@modifies internalState@*/ ;
586 extern /*@observer@*/ /*@null@*/ char *getenv (char *name) /*@*/ ;
588 extern int system (/*@null@*/ char *s) /*@modifies fileSystem@*/ ;
590 extern /*@null@*/ /*@dependent@*/ void *
591 bsearch (void *key, void *base,
592 size_t n, size_t size,
593 int (*compar)(void *, void *)) /*@*/ ;
595 extern void qsort (void *base, size_t n, size_t size,
596 int (*compar)(void *, void *))
597 /*@modifies *base, errno@*/ ;
599 extern int abs (int n) /*@*/ ;
601 typedef /*@concrete@*/ struct
607 extern div_t div (int num, int denom) /*@*/ ;
609 extern long int labs (long int n) /*@*/ ;
611 typedef /*@concrete@*/ struct
617 extern ldiv_t ldiv (long num, long denom) /*@*/ ;
619 /*@constant size_t MB_CUR_MAX; @*/
622 ** wchar_t and wint_t functions added by Amendment 1 to ISO.
625 /*@constant int WCHAR_MAX@*/
626 /*@constant int WCHAR_MIN@*/
627 /*@constant wint_t WEOF@*/
629 extern wint_t btowc (int c) /*@*/ ;
631 extern wint_t fgetwc (FILE *fp) /*@modifies fileSystem, *fp*/ ;
633 extern /*@null@*/ wchar_t *fgetws (/*@returned@*/ wchar_t *s, int n, FILE *stream)
634 /*@modifies fileSystem, *s, *stream@*/;
636 extern wint_t fputwc (wchar_t c, FILE *stream)
637 /*@modifies fileSystem, *stream@*/;
639 extern int fputws (const wchar_t *s, FILE *stream)
640 /*@modifies fileSystem, *stream@*/ ;
642 extern int fwide (FILE *stream, int mode) /*@*/ ;
643 /* does not modify the stream */
645 /*@printflike@*/ extern int fwprintf (FILE *stream, const wchar_t *format, ...)
646 /*@modifies *stream, fileSystem@*/ ;
648 /*@scanflike@*/ extern int fwscanf (FILE *stream, const wchar_t *format, ...)
649 /*@modifies *stream, fileSystem@*/ ;
651 /* note use of sef --- stream may be evaluated more than once */
652 extern wint_t getwc (/*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ;
654 extern wint_t getwchar (void) /*@modifies fileSystem, *stdin@*/;
656 extern size_t mbrlen (const char *s, size_t n, /*@null@*/ mbstate_t *ps) /*@*/ ;
658 extern size_t mbrtowc (/*@null@*/ wchar_t *pwc, const char *s, size_t n,
659 /*@null@*/ mbstate_t *ps)
660 /*@modifies *pwc@*/ ;
662 extern int mbsinit (/*@null@*/ const mbstate_t *ps) /*@*/ ;
664 extern size_t mbsrtowcs (/*@null@*/ wchar_t *dst, const char **src, size_t len,
665 /*@null@*/ mbstate_t *ps)
666 /*@modifies *dst@*/ ;
668 /* note use of sef --- stream may be evaluated more than once */
669 extern wint_t putwc (wchar_t c, /*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ;
671 extern wint_t putwchar (wchar_t c) /*@modifies fileSystem, *stdout@*/ ;
673 /*@printflike@*/ extern int swprintf (wchar_t *s, size_t n, const wchar_t *format, ...)
676 /*@scanflike@*/ extern int swscanf (const wchar_t *s, const wchar_t *format, ...)
677 /*@modifies *stdin@*/ ;
679 extern wint_t ungetwc (wint_t c, FILE *stream) /*@modifies fileSystem, *stream@*/ ;
681 extern int vfwprintf (FILE *stream, const wchar_t *format, va_list arg)
682 /*@modifies fileSystem, *stream@*/ ;
684 extern int vswprintf (wchar_t *s, size_t n, const wchar_t *format, va_list arg)
687 extern int vwprintf (const wchar_t *format, va_list arg)
688 /*@modifies fileSystem, *stdout@*/ ;
690 extern size_t wcrtomb (/*@null@*/ /*@out@*/ char *s, wchar_t wc, /*@null@*/ mbstate_t *ps)
693 extern void /*@alt wchar_t *@*/
694 wcscat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2)
697 extern /*@exposed@*/ /*@null@*/ wchar_t *
698 wcschr (/*@returned@*/ const wchar_t *s, wchar_t c)
701 extern int wcscmp (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
703 extern int wcscoll (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
705 extern void /*@alt wchar_t *@*/
706 wcscpy (/*@unique@*/ /*@out@*/ /*@returned@*/ wchar_t *s1, const wchar_t *s2)
709 extern size_t wcscspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
711 extern size_t wcsftime (/*@out@*/ wchar_t *s, size_t maxsize, const wchar_t *format,
712 const struct tm *timeptr)
715 extern size_t wcslen (const wchar_t *s) /*@*/ ;
717 extern void /*@alt wchar_t *@*/
718 wcsncat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
722 extern int wcsncmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
724 extern void /*@alt wchar_t *@*/
725 wcsncpy (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
729 extern /*@null@*/ wchar_t *
730 wcspbrk (/*@returned@*/ const wchar_t *s1, const wchar_t *s2)
733 extern /*@null@*/ wchar_t *
734 wcsrchr (/*@returned@*/ const wchar_t *s, wchar_t c)
738 wcsrtombs (/*@null@*/ char *dst, const wchar_t **src, size_t len,
739 /*@null@*/ mbstate_t *ps)
740 /*@modifies *src@*/ ;
742 extern size_t wcsspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
744 extern /*@null@*/ wchar_t *wcsstr (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
746 extern double wcstod (const wchar_t *nptr, /*@null@*/ wchar_t **endptr)
747 /*@modifies *endptr@*/ ;
749 extern /*@null@*/ wchar_t *
750 wcstok (/*@null@*/ wchar_t *s1, const wchar_t *s2, wchar_t **ptr)
753 extern long wcstol (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
754 /*@modifies *endptr@*/;
757 wcstoul (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
758 /*@modifies *endptr@*/;
761 wcsxfrm (/*@null@*/ wchar_t *s1, const wchar_t *s2, size_t n)
764 extern int wctob (wint_t c) /*@*/;
766 extern /*@null@*/ wchar_t *wmemchr (const wchar_t *s, wchar_t c, size_t n) /*@*/ ;
768 extern int wmemcmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
770 extern wchar_t *wmemcpy (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
773 extern wchar_t *wmemmove (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
776 extern wchar_t *wmemset (/*@returned@*/ wchar_t *s, wchar_t c, size_t n)
779 /*@printflike@*/ extern int wprintf (const wchar_t *format, ...)
780 /*@globals stdout@*/ /*@modifies errno, *stdout@*/;
782 /*@scanflike@*/ extern int
783 wscanf (const wchar_t *format, ...)
784 /*@globals stdin@*/ /*@modifies errno, *stdin@*/;
787 ** wctype.h (added by Amendment 1)
790 /* Warning: not sure about these (maybe abstract?): */
791 typedef /*@integraltype@*/ wctype_t;
792 typedef /*@integraltype@*/ wctrans_t;
795 extern lltX_bool iswalnum (wint_t c) /*@*/ ;
796 extern lltX_bool iswalpha (wint_t c) /*@*/ ;
797 extern lltX_bool iswcntrl (wint_t c) /*@*/ ;
798 extern lltX_bool iswctype (wint_t c, wctype_t ctg) /*@*/ ;
799 extern lltX_bool iswdigit (wint_t c) /*@*/ ;
800 extern lltX_bool iswgraph (wint_t c) /*@*/ ;
801 extern lltX_bool iswlower (wint_t c) /*@*/ ;
802 extern lltX_bool iswprint (wint_t c) /*@*/ ;
803 extern lltX_bool iswpunct (wint_t c) /*@*/ ;
804 extern lltX_bool iswspace (wint_t c) /*@*/ ;
805 extern lltX_bool iswupper (wint_t c) /*@*/ ;
806 extern lltX_bool iswxdigit (wint_t c) /*@*/ ;
808 extern wint_t towctrans (wint_t c, wctrans_t ctg) /*@*/ ;
809 extern wint_t towlower (wint_t c) /*@*/ ;
810 extern wint_t towupper (wint_t c) /*@*/ ;
812 extern lltX_bool /*@alt int@*/ iswalnum (wint_t c) /*@*/ ;
813 extern lltX_bool /*@alt int@*/ iswalpha (wint_t c) /*@*/ ;
814 extern lltX_bool /*@alt int@*/ iswcntrl (wint_t c) /*@*/ ;
815 extern lltX_bool /*@alt int@*/ iswctype (wint_t c, wctype_t ctg) /*@*/ ;
816 extern lltX_bool /*@alt int@*/ iswdigit (wint_t c) /*@*/ ;
817 extern lltX_bool /*@alt int@*/ iswgraph (wint_t c) /*@*/ ;
818 extern lltX_bool /*@alt int@*/ iswlower (wint_t c) /*@*/ ;
819 extern lltX_bool /*@alt int@*/ iswprint (wint_t c) /*@*/ ;
820 extern lltX_bool /*@alt int@*/ iswpunct (wint_t c) /*@*/ ;
821 extern lltX_bool /*@alt int@*/ iswspace (wint_t c) /*@*/ ;
822 extern lltX_bool /*@alt int@*/ iswupper (wint_t c) /*@*/ ;
823 extern lltX_bool /*@alt int@*/ iswxdigit (wint_t c) /*@*/ ;
825 extern wint_t /*@alt int@*/ towctrans (wint_t c, wctrans_t ctg) /*@*/ ;
826 extern wint_t /*@alt int@*/ towlower (wint_t c) /*@*/ ;
827 extern wint_t /*@alt int@*/ towupper (wint_t c) /*@*/ ;
830 extern wctrans_t wctrans (const char *property) /*@*/ ;
831 extern wctype_t wctype (const char *property) /*@*/ ;
833 extern int mblen (char *s, size_t n) /*@*/ ;
834 extern int mbtowc (/*@null@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n)
835 /*@modifies *pwc@*/ ;
836 extern int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar)
838 extern size_t mbstowcs (/*@out@*/ wchar_t *pwcs, char *s, size_t n)
839 /*@modifies *pwcs@*/ ;
840 extern size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n)
847 extern void /*@alt void * @*/
848 memcpy (/*@unique@*/ /*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
850 /*@requires MaxRead(s2) >= (n - 1) /\ MaxSet(s1) >= (n - 1); @*/
853 extern void /*@alt void * @*/
854 memmove (/*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
856 /*@requires MaxRead(s2) >= (n - 1) /\ MaxSet(s1) >= (n - 1); @*/
864 extern void /*@alt char * @*/
865 strcpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2)
867 /*@requires maxSet(s1) >= maxRead(s2) @*/
868 /*@ensures MaxRead(s1) == MaxRead (s2) /\ MaxRead(result) == MaxRead(s2) /\ MaxSet(result) == MaxSet(s1); @*/;
870 extern void /*@alt char * @*/
871 strncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2, size_t n)
872 /*@modifies *s1@*/ /*@requires MaxSet(s1) >= ( n - 1 ); @*/ /*@ensures MaxRead (s2) >= MaxRead(s1) /\ MaxRead (s1) <= n; @*/;
874 extern void /*@alt char * @*/
875 strcat (/*@unique@*/ /*@returned@*/ char *s1, char *s2)
876 /*@modifies *s1@*/ /*@requires MaxSet(s1) >= (MaxRead(s1) + MaxRead(s2) );@*/
877 /*@ensures MaxRead(result) == (MaxRead(s1) + MaxRead(s2) );@*/;
879 extern void /*@alt char * @*/
880 strncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, size_t n)
882 /*@requires MaxSet(s1) >= ( MaxRead(s1) + n); @*/
883 /*@ensures MaxRead(s1) >= (MaxRead(s1) + n); @*/;
887 extern int memcmp (void *s1, void *s2, size_t n) /*@*/ ;
888 extern int strcmp (char *s1, char *s2) /*@*/ ;
889 extern int strcoll (char *s1, char *s2) /*@*/ ;
890 extern int strncmp (char *s1, char *s2, size_t n) /*@*/ ;
891 extern size_t strxfrm (/*@out@*/ /*@null@*/ char *s1, char *s2, size_t n)
892 /*@modifies *s1@*/ ; /* s1 may be null only if n == 0 */
894 extern /*@null@*/ void *memchr (void *s, int c, size_t n) /*@*/ ;
897 extern /*@exposed@*/ /*@null@*/ char *
898 strchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0 @*/ ;
900 extern /*@exposed@*/ /*@null@*/ char *
901 strchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0; @*/ ;
904 extern size_t strcspn (char *s1, char *s2) /*@*/ ;
905 extern /*@null@*/ /*@exposed@*/ char *
906 strpbrk (/*@returned@*/ char *s, char *t) /*@*/ ;
909 extern /*@null@*/ /*@exposed@*/ char *
910 strrchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0 @*/ ;
912 extern /*@null@*/ /*@exposed@*/ char *
913 strrchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0 @*/ ;
916 extern size_t strspn (char *s, char *t) /*@*/ ;
918 extern /*@null@*/ /*@exposed@*/ char *
919 strstr (/*@returned@*/ /*@unique@*/ char *s, char *t) /*@*/
920 /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0 @*/ ;
922 extern /*@null@*/ /*@exposed@*/ char *
923 strtok (/*@returned@*/ /*@null@*/ char *s, char *t)
924 /*@modifies *s, internalState, errno@*/ ;
926 extern void /*@alt void *@*/ memset (/*@out@*/ /*@returned@*/ void *s,
928 /*@modifies *s@*/ /*@requires MaxSet(s) >= (n - 1) @*/ /*@ensures MaxRead(s) >= (n - 1) @*/ ;
930 extern /*@observer@*/ char *strerror (int errnum) /*@*/ ;
933 extern size_t strlen (char *s) /*@*/ /*@ensures result == MaxRead(s); @*/;
939 /*@constant int CLOCKS_PER_SEC;@*/
941 typedef /*@integraltype@*/ clock_t;
942 typedef /*@integraltype@*/ time_t;
957 extern clock_t clock (void) /*@modifies internalState@*/ ;
958 extern double difftime (time_t time1, time_t time0) /*@*/ ;
959 extern time_t mktime (struct tm *timeptr) /*@*/ ;
961 extern time_t time (/*@null@*/ /*@out@*/ time_t *tp)
964 extern /*@observer@*/ char *asctime (struct tm *timeptr)
965 /*@modifies errno*/ /*@ensures MaxSet(result) == 25 /\ MaxRead(result) == 25; @*/ ;
967 extern /*@observer@*/ char *ctime (time_t *tp) /*@*/
968 /*@ensures MaxSet(result) == 25 /\ MaxRead(result) == 25; @*/;
970 extern /*@null@*/ /*@observer@*/ struct tm *gmtime (time_t *tp) /*@*/ ;
972 extern /*@null@*/ /*@observer@*/ struct tm *localtime (time_t *tp)
973 /*@modifies errno@*/ ;
975 extern size_t strftime (/*@out@*/ char *s, size_t smax,
976 char *fmt, struct tm *timeptr)
980 ** ISO c99: 7.18 Integer types <stdint.h>
984 ** These types are OPTIONAL. Provide warnings on use.
987 typedef /*@integraltype@*/ int8_t
988 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least8_t instead."@*/ ;
990 typedef /*@integraltype@*/ int16_t
991 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least16_t instead."@*/ ;
993 typedef /*@integraltype@*/ int32_t
994 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least32_t instead."@*/ ;
996 typedef /*@integraltype@*/ int64_t
997 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least64_t instead."@*/ ;
999 typedef /*@unsignedintegraltype@*/ uint8_t
1000 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least8_t instead."@*/ ;
1002 typedef /*@unsignedintegraltype@*/ uint16_t
1003 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least16_t instead."@*/ ;
1005 typedef /*@unsignedintegraltype@*/ uint32_t
1006 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least32_t instead."@*/ ;
1008 typedef /*@unsignedintegraltype@*/ uint64_t
1009 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least64_t instead."@*/ ;
1011 typedef /*@integraltype@*/ int_least8_t;
1012 typedef /*@integraltype@*/ int_least16_t;
1013 typedef /*@integraltype@*/ int_least32_t;
1014 typedef /*@integraltype@*/ int_least64_t;
1016 typedef /*@unsignedintegraltype@*/ uint_least8_t;
1017 typedef /*@unsignedintegraltype@*/ uint_least16_t;
1018 typedef /*@unsignedintegraltype@*/ uint_least32_t;
1019 typedef /*@unsignedintegraltype@*/ uint_least64_t;
1021 typedef /*@integraltype@*/ int_fast8_t;
1022 typedef /*@integraltype@*/ int_fast16_t;
1023 typedef /*@integraltype@*/ int_fast32_t;
1024 typedef /*@integraltype@*/ int_fast64_t;
1026 typedef /*@unsignedintegraltype@*/ uint_fast8_t;
1027 typedef /*@unsignedintegraltype@*/ uint_fast16_t;
1028 typedef /*@unsignedintegraltype@*/ uint_fast32_t;
1029 typedef /*@unsignedintegraltype@*/ uint_fast64_t;
1031 typedef int *intptr_t
1032 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;
1034 typedef unsigned int *uintptr_t
1035 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;
1037 typedef /*@signedintegraltype@*/ intmax_t;
1038 typedef /*@unsignedintegraltype@*/ uintmax_t;
1041 ** What should the types be here?
1044 /*@constant int INT8_MIN@*/
1045 /*@constant int INT16_MIN@*/
1046 /*@constant int INT32_MIN@*/
1047 /*@constant int INT64_MIN@*/
1049 /*@constant int INT8_MAX@*/
1050 /*@constant int INT16_MAX@*/
1051 /*@constant int INT32_MAX@*/
1052 /*@constant int INT64_MAX@*/
1054 /*@constant int UINT8_MIN@*/
1055 /*@constant int UINT16_MIN@*/
1056 /*@constant int UINT32_MIN@*/
1057 /*@constant int UINT64_MIN@*/
1059 /*@constant int INT_LEAST8_MIN@*/
1060 /*@constant int INT_LEAST16_MIN@*/
1061 /*@constant int INT_LEAST32_MIN@*/
1062 /*@constant int INT_LEAST64_MIN@*/
1064 /*@constant int INT_LEAST8_MAX@*/
1065 /*@constant int INT_LEAST16_MAX@*/
1066 /*@constant int INT_LEAST32_MAX@*/
1067 /*@constant int INT_LEAST64_MAX@*/
1069 /*@constant int UINT_LEAST8_MAX@*/
1070 /*@constant int UINT_LEAST16_MAX@*/
1071 /*@constant int UINT_LEAST32_MAX@*/
1072 /*@constant int UINT_LEAST64_MAX@*/
1074 /*@constant int INT_FAST8_MIN@*/
1075 /*@constant int INT_FAST16_MIN@*/
1076 /*@constant int INT_FAST32_MIN@*/
1077 /*@constant int INT_FAST64_MIN@*/
1079 /*@constant int INT_FAST8_MAX@*/
1080 /*@constant int INT_FAST16_MAX@*/
1081 /*@constant int INT_FAST32_MAX@*/
1082 /*@constant int INT_FAST64_MAX@*/
1084 /*@constant int UINT_FAST8_MAX@*/
1085 /*@constant int UINT_FAST16_MAX@*/
1086 /*@constant int UINT_FAST32_MAX@*/
1087 /*@constant int UINT_FAST64_MAX@*/
1089 /*@constant size_t INTPTR_MIN@*/
1090 /*@constant size_t INTPTR_MAX@*/