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