]> 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 line numbering when multi-line macro parameters are used.
[splint.git] / lib / standard.h
CommitLineData
155af98d 1/*
2** satndard.h --- ISO C99 Standard Library for Splint.
3**
4** Process with -DSTRICT to get strict library.
5*/
6
7/*@-nextlinemacros@*/
8/*@+allimponly@*/
9/*@+globsimpmodifiesnothing@*/
10
11/*
12** errno.h
13*/
14
15/*@constant int EDOM;@*/
16/*@constant int ERANGE;@*/
17/*@constant int EILSEQ;@*/
18
19# ifdef STRICT
20/*@checkedstrict@*/ int errno;
21# else
22/*@unchecked@*/ int errno;
23# endif
24
25/*
26** types
27*/
28
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
378/*@null@*/ FILE *tmpfile (void) /*@modifies fileSystem@*/ ;
379/*@observer@*/ char *
380 tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s)
381 /*@modifies *s, internalState@*/ ;
382
383int fclose (FILE *stream) /*@modifies *stream, errno, fileSystem;@*/ ;
384int fflush (/*@null@*/ FILE *stream)
385 /*@modifies *stream, errno, fileSystem;@*/ ;
386
387/*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode)
388 /*@modifies fileSystem@*/ ;
389
390/*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream)
391 /*@modifies *stream, fileSystem, errno@*/ ;
392
393 extern void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf)
394 /*@modifies fileSystem, *stream, *buf@*/ ;
395
396 extern int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf,
397 int mode, size_t size)
398 /*@modifies fileSystem, *stream, *buf@*/ ;
399
400# ifdef STRICT
401/*@printflike@*/
402int fprintf (FILE *stream, char *format, ...)
403 /*@modifies fileSystem, *stream@*/ ;
404# else
405/*@printflike@*/
406int /*@alt void@*/ fprintf (FILE *stream, char *format, ...)
407 /*@modifies fileSystem, *stream@*/ ;
408# endif
409
410/*@scanflike@*/
411int fscanf (FILE *stream, char *format, ...)
412 /*@modifies fileSystem, *stream@*/ ;
413
414# ifdef STRICT
415/*@printflike@*/
416int printf (char *format, ...)
417 /*@globals stdout@*/
418 /*@modifies fileSystem, *stdout@*/ ;
419# else
420/*@printflike@*/
421int /*@alt void@*/ printf (char *format, ...)
422 /*@globals stdout@*/
423 /*@modifies fileSystem, *stdout@*/ ;
424# endif
425
426/*@scanflike@*/
427int scanf(char *format, ...)
428 /*@globals stdin@*/
429 /*@modifies fileSystem, *stdin@*/ ;
430
431# ifdef STRICT
432/*@printflike@*/
433int sprintf (/*@out@*/ char *s, char *format, ...)
434 /*@modifies *s@*/ ;
435# else
436/*@printflike@*/
437int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...)
438 /*@modifies *s@*/ ;
439# endif
440
441/*@scanflike@*/
442int sscanf (/*@out@*/ char *s, char *format, ...) /*@*/ ;
443 /* modifies extra arguments */
444
445int vprintf (const char *format, va_list arg)
446 /*@globals stdout@*/
447 /*@modifies fileSystem, *stdout@*/ ;
448
449int vfprintf (FILE *stream, char *format, va_list arg)
450 /*@modifies fileSystem, *stream, arg, errno@*/ ;
451
452int vsprintf (/*@out@*/ char *str, const char *format, va_list ap)
453 /*@warn bufferoverflowhigh "Use vsnprintf instead"@*/
454 /*@modifies str@*/ ;
455
456int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap)
457 /*@requires maxSet(str) >= size@*/
458 /*@modifies str@*/ ;
459
460int fgetc (FILE *stream)
461 /*@modifies fileSystem, *stream, errno@*/ ;
462
463/*@null@*/ char *
464 fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream)
465 /*@modifies fileSystem, *s, *stream, errno@*/
466 /*@requires maxSet(s) >= (n -1); @*/
467 /*@ensures maxRead(s) <= (n -1) /\ maxRead(s) >= 0; @*/
468 ;
469
470int fputc (int /*@alt char@*/ c, FILE *stream)
471 /*:errorcode EOF:*/
472 /*@modifies fileSystem, *stream, errno@*/ ;
473
474int fputs (char *s, FILE *stream)
475 /*@modifies fileSystem, *stream@*/ ;
476
477/* note use of sef --- stream may be evaluated more than once */
478int getc (/*@sef@*/ FILE *stream)
479 /*@modifies fileSystem, *stream@*/ ;
480
481int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin@*/ ;
482
483/*@null@*/ char *gets (/*@out@*/ char *s)
484 /*@warn bufferoverflowhigh
485 "Use of gets leads to a buffer overflow vulnerability. Use fgets instead"@*/
486 /*@globals stdin@*/ /*@modifies fileSystem, *s, *stdin, errno@*/ ;
487
488int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream)
489 /*:errorcode EOF:*/
490 /*@modifies fileSystem, *stream;@*/ ;
491
492int putchar (int /*@alt char@*/ c)
493 /*:errorcode EOF:*/
494 /*@globals stdout@*/ /*@modifies fileSystem, *stdout@*/ ;
495
496int puts (const char *s)
497 /*:errorcode EOF:*/
498 /*@globals stdout@*/
499 /*@modifies fileSystem, *stdout@*/ ;
500
501int ungetc (int /*@alt char@*/ c, FILE *stream)
502 /*@modifies fileSystem, *stream, errno@*/ ;
503
504size_t
505 fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream)
506 /*@modifies fileSystem, *ptr, *stream, errno@*/ ;
507
508size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream)
509 /*@modifies fileSystem, *stream, errno@*/ ;
510
511int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos)
512 /*@modifies *pos, errno@*/ ;
513
514int fseek (FILE *stream, long int offset, int whence)
515 /*:errorcode -1:*/
516 /*@modifies fileSystem, *stream, errno@*/ ;
517
518int fsetpos (FILE *stream, fpos_t *pos)
519 /*@modifies fileSystem, *stream, errno@*/ ;
520
521long int ftell(FILE *stream)
522 /*:errorcode -1:*/ /*@modifies errno*/ ;
523
524void rewind (FILE *stream) /*@modifies *stream@*/ ;
525void clearerr (FILE *stream) /*@modifies *stream@*/ ;
526
527int feof (FILE *stream) /*@modifies errno@*/ ;
528int ferror (FILE *stream) /*@modifies errno@*/ ;
529
530void perror (/*@null@*/ char *s)
531 /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ;
532
533/*
534** stdlib.h
535*/
536
537double atof (char *s) /*@*/ ;
538int atoi (char *s) /*@*/ ;
539long int atol (char *s) /*@*/ ;
540
541double strtod (char *s, /*@null@*/ /*@out@*/ char **endp)
542 /*@modifies *endp, errno@*/ ;
543
544long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
545 /*@modifies *endp, errno@*/ ;
546
547unsigned long
548 strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base)
549 /*@modifies *endp, errno@*/ ;
550
551/*@constant int RAND_MAX; @*/
552int rand (void) /*@modifies internalState@*/ ;
553void srand (unsigned int seed) /*@modifies internalState@*/ ;
554
555/*
556 drl
557 changed 12/29/2000
558*/
559
560/*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/
561 /*@ensures maxSet(result) == (nobj - 1); @*/ ;
562/*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@*/
563 /*@ensures maxSet(result) == (size - 1); @*/ ;
564
565/*end drl changed */
566
567/* 11 June 1997: removed out on return value */
568
569# if 0
570/*@null@*/ /*@only@*/ void *
571 realloc (/*@null@*/ /*@only@*/ /*@special@*/ void *p,
572 size_t size) /*@releases p@*/ /*@modifies *p@*/
573 /*@ensures maxSet(result) == (size - 1) @*/;
574# endif
575
576/*
577** LCLint annotations cannot fully describe realloc. The semantics we
578** want are:
579** realloc returns null: ownership of parameter is not changed
580** realloc returns non-null: ownership of parameter is transferred to return value
581**
582** Otherwise, storage is in the same state before and after the call.
583*/
584
585/*@null@*/ /*@only@*/ void *
586 realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size)
587 /*@modifies *p@*/ /*@ensures maxSet(result) >= (size - 1) @*/;
588
589void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies p@*/ ;
590
591/*@constant int EXIT_FAILURE; @*/
592/*@constant int EXIT_SUCCESS; @*/
593
594/*@exits@*/ void abort (void) /*@*/ ;
595/*@exits@*/ void exit (int status) /*@*/ ;
596int atexit (void (*func)(void)) /*@modifies internalState@*/ ;
597
598/*@observer@*/ /*@null@*/ char *getenv (char *name) /*@*/ ;
599
600int system (/*@null@*/ char *s) /*@modifies fileSystem@*/ ;
601
602/*@null@*/ /*@dependent@*/ void *
603 bsearch (void *key, void *base,
604 size_t n, size_t size,
605 int (*compar)(void *, void *)) /*@*/ ;
606
607void qsort (void *base, size_t n, size_t size,
608 int (*compar)(void *, void *))
609 /*@modifies *base, errno@*/ ;
610
611int abs (int n) /*@*/ ;
612
613typedef /*@concrete@*/ struct
614{
615 int quot;
616 int rem;
617} div_t ;
618
619div_t div (int num, int denom) /*@*/ ;
620
621long int labs (long int n) /*@*/ ;
622
623typedef /*@concrete@*/ struct
624{
625 long int quot;
626 long int rem;
627} ldiv_t ;
628
629ldiv_t ldiv (long num, long denom) /*@*/ ;
630
631/*@constant size_t MB_CUR_MAX; @*/
632
633/*
634** wchar_t and wint_t functions added by Amendment 1 to ISO.
635*/
636
637/*@constant int WCHAR_MAX@*/
638/*@constant int WCHAR_MIN@*/
639/*@constant wint_t WEOF@*/
640
641wint_t btowc (int c) /*@*/ ;
642
643wint_t fgetwc (FILE *fp) /*@modifies fileSystem, *fp*/ ;
644
645/*@null@*/ wchar_t *fgetws (/*@returned@*/ wchar_t *s, int n, FILE *stream)
646 /*@modifies fileSystem, *s, *stream@*/;
647
648wint_t fputwc (wchar_t c, FILE *stream)
649 /*@modifies fileSystem, *stream@*/;
650
651int fputws (const wchar_t *s, FILE *stream)
652 /*@modifies fileSystem, *stream@*/ ;
653
654int fwide (FILE *stream, int mode) /*@*/ ;
655 /* does not modify the stream */
656
657/*@printflike@*/ int fwprintf (FILE *stream, const wchar_t *format, ...)
658 /*@modifies *stream, fileSystem@*/ ;
659
660/*@scanflike@*/ int fwscanf (FILE *stream, const wchar_t *format, ...)
661 /*@modifies *stream, fileSystem@*/ ;
662
663/* note use of sef --- stream may be evaluated more than once */
664wint_t getwc (/*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ;
665
666wint_t getwchar (void) /*@modifies fileSystem, *stdin@*/;
667
668size_t mbrlen (const char *s, size_t n, /*@null@*/ mbstate_t *ps) /*@*/ ;
669
670size_t mbrtowc (/*@null@*/ wchar_t *pwc, const char *s, size_t n,
671 /*@null@*/ mbstate_t *ps)
672 /*@modifies *pwc@*/ ;
673
674int mbsinit (/*@null@*/ const mbstate_t *ps) /*@*/ ;
675
676size_t mbsrtowcs (/*@null@*/ wchar_t *dst, const char **src, size_t len,
677 /*@null@*/ mbstate_t *ps)
678 /*@modifies *dst@*/ ;
679
680/* note use of sef --- stream may be evaluated more than once */
681wint_t putwc (wchar_t c, /*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ;
682
683wint_t putwchar (wchar_t c) /*@modifies fileSystem, *stdout@*/ ;
684
685/*@printflike@*/ int swprintf (wchar_t *s, size_t n, const wchar_t *format, ...)
686 /*@modifies *s@*/ ;
687
688/*@scanflike@*/ int swscanf (const wchar_t *s, const wchar_t *format, ...)
689 /*@modifies *stdin@*/ ;
690
691wint_t ungetwc (wint_t c, FILE *stream) /*@modifies fileSystem, *stream@*/ ;
692
693int vfwprintf (FILE *stream, const wchar_t *format, va_list arg)
694 /*@modifies fileSystem, *stream@*/ ;
695
696int vswprintf (wchar_t *s, size_t n, const wchar_t *format, va_list arg)
697 /*@modifies *s@*/ ;
698
699int vwprintf (const wchar_t *format, va_list arg)
700 /*@modifies fileSystem, *stdout@*/ ;
701
702size_t wcrtomb (/*@null@*/ /*@out@*/ char *s, wchar_t wc, /*@null@*/ mbstate_t *ps)
703 /*@modifies *s@*/;
704
705void /*@alt wchar_t *@*/
706 wcscat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2)
707 /*@modifies *s1@*/ ;
708
709/*@exposed@*/ /*@null@*/ wchar_t *
710 wcschr (/*@returned@*/ const wchar_t *s, wchar_t c)
711 /*@*/ ;
712
713int wcscmp (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
714
715int wcscoll (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
716
717void /*@alt wchar_t *@*/
718 wcscpy (/*@unique@*/ /*@out@*/ /*@returned@*/ wchar_t *s1, const wchar_t *s2)
719 /*@modifies *s1@*/ ;
720
721size_t wcscspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
722
723size_t wcsftime (/*@out@*/ wchar_t *s, size_t maxsize, const wchar_t *format,
724 const struct tm *timeptr)
725 /*@modifies *s@*/ ;
726
727size_t wcslen (const wchar_t *s) /*@*/ ;
728
729void /*@alt wchar_t *@*/
730 wcsncat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
731 size_t n)
732 /*@modifies *s1@*/ ;
733
734int wcsncmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
735
736void /*@alt wchar_t *@*/
737 wcsncpy (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2,
738 size_t n)
739 /*@modifies *s1@*/ ;
740
741/*@null@*/ wchar_t *
742 wcspbrk (/*@returned@*/ const wchar_t *s1, const wchar_t *s2)
743 /*@*/ ;
744
745/*@null@*/ wchar_t *
746 wcsrchr (/*@returned@*/ const wchar_t *s, wchar_t c)
747 /*@*/ ;
748
749size_t
750 wcsrtombs (/*@null@*/ char *dst, const wchar_t **src, size_t len,
751 /*@null@*/ mbstate_t *ps)
752 /*@modifies *src@*/ ;
753
754size_t wcsspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
755
756/*@null@*/ wchar_t *wcsstr (const wchar_t *s1, const wchar_t *s2) /*@*/ ;
757
758double wcstod (const wchar_t *nptr, /*@null@*/ wchar_t **endptr)
759 /*@modifies *endptr@*/ ;
760
761/*@null@*/ wchar_t *
762 wcstok (/*@null@*/ wchar_t *s1, const wchar_t *s2, wchar_t **ptr)
763 /*@modifies *ptr@*/;
764
765long wcstol (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
766 /*@modifies *endptr@*/;
767
768unsigned long
769 wcstoul (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base)
770 /*@modifies *endptr@*/;
771
772size_t
773 wcsxfrm (/*@null@*/ wchar_t *s1, const wchar_t *s2, size_t n)
774 /*@modifies *s1@*/;
775
776int wctob (wint_t c) /*@*/;
777
778/*@null@*/ wchar_t *wmemchr (const wchar_t *s, wchar_t c, size_t n) /*@*/ ;
779
780int wmemcmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ;
781
782wchar_t *wmemcpy (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
783 /*@modifies *s1@*/;
784
785wchar_t *wmemmove (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n)
786 /*@modifies *s1@*/;
787
788wchar_t *wmemset (/*@returned@*/ wchar_t *s, wchar_t c, size_t n)
789 /*@modifies *s@*/;
790
791/*@printflike@*/ int wprintf (const wchar_t *format, ...)
792 /*@globals stdout@*/ /*@modifies errno, *stdout@*/;
793
794/*@scanflike@*/ int
795 wscanf (const wchar_t *format, ...)
796 /*@globals stdin@*/ /*@modifies errno, *stdin@*/;
797
798/*
799** wctype.h (added by Amendment 1)
800*/
801
802/* Warning: not sure about these (maybe abstract?): */
803typedef /*@integraltype@*/ wctype_t;
804typedef /*@integraltype@*/ wctrans_t;
805
806# ifdef STRICT
807lltX_bool iswalnum (wint_t c) /*@*/ ;
808lltX_bool iswalpha (wint_t c) /*@*/ ;
809lltX_bool iswcntrl (wint_t c) /*@*/ ;
810lltX_bool iswctype (wint_t c, wctype_t ctg) /*@*/ ;
811lltX_bool iswdigit (wint_t c) /*@*/ ;
812lltX_bool iswgraph (wint_t c) /*@*/ ;
813lltX_bool iswlower (wint_t c) /*@*/ ;
814lltX_bool iswprint (wint_t c) /*@*/ ;
815lltX_bool iswpunct (wint_t c) /*@*/ ;
816lltX_bool iswspace (wint_t c) /*@*/ ;
817lltX_bool iswupper (wint_t c) /*@*/ ;
818lltX_bool iswxdigit (wint_t c) /*@*/ ;
819
820wint_t towctrans (wint_t c, wctrans_t ctg) /*@*/ ;
821wint_t towlower (wint_t c) /*@*/ ;
822wint_t towupper (wint_t c) /*@*/ ;
823# else
824lltX_bool /*@alt int@*/ iswalnum (wint_t c) /*@*/ ;
825lltX_bool /*@alt int@*/ iswalpha (wint_t c) /*@*/ ;
826lltX_bool /*@alt int@*/ iswcntrl (wint_t c) /*@*/ ;
827lltX_bool /*@alt int@*/ iswctype (wint_t c, wctype_t ctg) /*@*/ ;
828lltX_bool /*@alt int@*/ iswdigit (wint_t c) /*@*/ ;
829lltX_bool /*@alt int@*/ iswgraph (wint_t c) /*@*/ ;
830lltX_bool /*@alt int@*/ iswlower (wint_t c) /*@*/ ;
831lltX_bool /*@alt int@*/ iswprint (wint_t c) /*@*/ ;
832lltX_bool /*@alt int@*/ iswpunct (wint_t c) /*@*/ ;
833lltX_bool /*@alt int@*/ iswspace (wint_t c) /*@*/ ;
834lltX_bool /*@alt int@*/ iswupper (wint_t c) /*@*/ ;
835lltX_bool /*@alt int@*/ iswxdigit (wint_t c) /*@*/ ;
836
837wint_t /*@alt int@*/ towctrans (wint_t c, wctrans_t ctg) /*@*/ ;
838wint_t /*@alt int@*/ towlower (wint_t c) /*@*/ ;
839wint_t /*@alt int@*/ towupper (wint_t c) /*@*/ ;
840# endif
841
842wctrans_t wctrans (const char *property) /*@*/ ;
843wctype_t wctype (const char *property) /*@*/ ;
844
845int mblen (char *s, size_t n) /*@*/ ;
846int mbtowc (/*@null@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n)
847 /*@modifies *pwc@*/ ;
848int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar)
849 /*@modifies *s@*/ ;
850size_t mbstowcs (/*@out@*/ wchar_t *pwcs, char *s, size_t n)
851 /*@modifies *pwcs@*/ ;
852size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n)
853 /*@modifies *s@*/ ;
854
855/*
856** string.h
857*/
858
859void /*@alt void * @*/
860 memcpy (/*@unique@*/ /*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
861 /*@modifies *s1@*/
862 /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
863 ;
864
865void /*@alt void * @*/
866 memmove (/*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
867 /*@modifies *s1@*/
868 /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/
869 ;
870
871
872 /* drl
873 modifed 12/29/2000
874 */
875
876void /*@alt char * @*/
877 strcpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2)
878 /*@modifies *s1@*/
879 /*@requires maxSet(s1) >= maxRead(s2) @*/
880 /*@ensures maxRead(s1) == maxRead (s2) /\ maxRead(result) == maxRead(s2) /\ maxSet(result) == maxSet(s1); @*/;
881
882void /*@alt char * @*/
883 strncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2, size_t n)
884 /*@modifies *s1@*/ /*@requires maxSet(s1) >= ( n - 1 ); @*/ /*@ensures maxRead (s2) >= maxRead(s1) /\ maxRead (s1) <= n; @*/;
885
886void /*@alt char * @*/
887 strcat (/*@unique@*/ /*@returned@*/ char *s1, char *s2)
888 /*@modifies *s1@*/ /*@requires maxSet(s1) >= (maxRead(s1) + maxRead(s2) );@*/
889 /*@ensures maxRead(result) == (maxRead(s1) + maxRead(s2) );@*/;
890
891void /*@alt char * @*/
892 strncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, size_t n)
893 /*@modifies *s1@*/
894 /*@requires maxSet(s1) >= ( maxRead(s1) + n); @*/
895 /*@ensures maxRead(s1) >= (maxRead(s1) + n); @*/;
896
897 /*drl end*/
898
899int memcmp (void *s1, void *s2, size_t n) /*@*/ ;
900int strcmp (char *s1, char *s2) /*@*/ ;
901int strcoll (char *s1, char *s2) /*@*/ ;
902int strncmp (char *s1, char *s2, size_t n) /*@*/ ;
903size_t strxfrm (/*@out@*/ /*@null@*/ char *s1, char *s2, size_t n)
904 /*@modifies *s1@*/ ; /* s1 may be null only if n == 0 */
905
906/*@null@*/ void *memchr (void *s, int c, size_t n) /*@*/ ;
907
908# ifdef STRICT
909/*@exposed@*/ /*@null@*/ char *
910strchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
911# else
912/*@exposed@*/ /*@null@*/ char *
913 strchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0; @*/ ;
914# endif
915
916size_t strcspn (char *s1, char *s2) /*@*/ ;
917/*@null@*/ /*@exposed@*/ char *
918 strpbrk (/*@returned@*/ char *s, char *t) /*@*/ ;
919
920# ifdef STRICT
921/*@null@*/ /*@exposed@*/ char *
922 strrchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
923# else
924/*@null@*/ /*@exposed@*/ char *
925 strrchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ;
926# endif
927
928size_t strspn (char *s, char *t) /*@*/ ;
929
930/*@null@*/ /*@exposed@*/ char *
931 strstr (/*@returned@*/ /*@unique@*/ char *s, char *t) /*@*/
932 /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 /\ maxRead(result) >= maxRead(t) /\ maxSet(result) >= maxRead(t)@*/ ;
933
934/*@null@*/ /*@exposed@*/ char *
935 strtok (/*@returned@*/ /*@null@*/ char *s, char *t)
936 /*@modifies *s, internalState, errno@*/ ;
937
938void /*@alt void *@*/ memset (/*@out@*/ /*@returned@*/ void *s,
939 int c, size_t n)
940 /*@modifies *s@*/ /*@requires maxSet(s) >= (n - 1) @*/ /*@ensures maxRead(s) >= (n - 1) @*/ ;
941
942/*@observer@*/ char *strerror (int errnum) /*@*/ ;
943
944/*drl */
945size_t strlen (char *s) /*@*/ /*@ensures result == maxRead(s); @*/;
946
947/*
948** time.h
949*/
950
951/*@constant int CLOCKS_PER_SEC;@*/
952
953typedef /*@integraltype@*/ clock_t;
954typedef /*@integraltype@*/ time_t;
955
956struct tm
957 {
958 int tm_sec;
959 int tm_min;
960 int tm_hour;
961 int tm_mday;
962 int tm_mon;
963 int tm_year;
964 int tm_wday;
965 int tm_yday;
966 int tm_isdst;
967 } ;
968
969clock_t clock (void) /*@modifies internalState@*/ ;
970double difftime (time_t time1, time_t time0) /*@*/ ;
971time_t mktime (struct tm *timeptr) /*@*/ ;
972
973time_t time (/*@null@*/ /*@out@*/ time_t *tp)
974 /*@modifies *tp@*/ ;
975
976/*@observer@*/ char *asctime (struct tm *timeptr)
977 /*@modifies errno*/ /*@ensures maxSet(result) == 25 /\ maxRead(result) == 25; @*/ ;
978
979/*@observer@*/ char *ctime (time_t *tp) /*@*/
980 /*@ensures maxSet(result) == 25 /\ maxRead(result) == 25; @*/;
981
982/*@null@*/ /*@observer@*/ struct tm *gmtime (time_t *tp) /*@*/ ;
983
984/*@null@*/ /*@observer@*/ struct tm *localtime (time_t *tp)
985 /*@modifies errno@*/ ;
986
987size_t strftime (/*@out@*/ char *s, size_t smax,
988 char *fmt, struct tm *timeptr)
989 /*@modifies *s@*/ ;
990
991/*
992** ISO c99: 7.18 Integer types <stdint.h>
993*/
994
995/*
996** These types are OPTIONAL. Provide warnings on use.
997*/
998
999typedef /*@integraltype@*/ int8_t
1000 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least8_t instead."@*/ ;
1001
1002typedef /*@integraltype@*/ int16_t
1003 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least16_t instead."@*/ ;
1004
1005typedef /*@integraltype@*/ int32_t
1006 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least32_t instead."@*/ ;
1007
1008typedef /*@integraltype@*/ int64_t
1009 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least64_t instead."@*/ ;
1010
1011typedef /*@unsignedintegraltype@*/ uint8_t
1012 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least8_t instead."@*/ ;
1013
1014typedef /*@unsignedintegraltype@*/ uint16_t
1015 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least16_t instead."@*/ ;
1016
1017typedef /*@unsignedintegraltype@*/ uint32_t
1018 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least32_t instead."@*/ ;
1019
1020typedef /*@unsignedintegraltype@*/ uint64_t
1021 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least64_t instead."@*/ ;
1022
1023typedef /*@integraltype@*/ int_least8_t;
1024typedef /*@integraltype@*/ int_least16_t;
1025typedef /*@integraltype@*/ int_least32_t;
1026typedef /*@integraltype@*/ int_least64_t;
1027
1028typedef /*@unsignedintegraltype@*/ uint_least8_t;
1029typedef /*@unsignedintegraltype@*/ uint_least16_t;
1030typedef /*@unsignedintegraltype@*/ uint_least32_t;
1031typedef /*@unsignedintegraltype@*/ uint_least64_t;
1032
1033typedef /*@integraltype@*/ int_fast8_t;
1034typedef /*@integraltype@*/ int_fast16_t;
1035typedef /*@integraltype@*/ int_fast32_t;
1036typedef /*@integraltype@*/ int_fast64_t;
1037
1038typedef /*@unsignedintegraltype@*/ uint_fast8_t;
1039typedef /*@unsignedintegraltype@*/ uint_fast16_t;
1040typedef /*@unsignedintegraltype@*/ uint_fast32_t;
1041typedef /*@unsignedintegraltype@*/ uint_fast64_t;
1042
1043typedef int *intptr_t
1044 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;
1045
1046typedef unsigned int *uintptr_t
1047 /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ;
1048
1049typedef /*@signedintegraltype@*/ intmax_t;
1050typedef /*@unsignedintegraltype@*/ uintmax_t;
1051
1052/*
1053** What should the types be here?
1054*/ /*#*/
1055
1056/*@constant int INT8_MIN@*/
1057/*@constant int INT16_MIN@*/
1058/*@constant int INT32_MIN@*/
1059/*@constant int INT64_MIN@*/
1060
1061/*@constant int INT8_MAX@*/
1062/*@constant int INT16_MAX@*/
1063/*@constant int INT32_MAX@*/
1064/*@constant int INT64_MAX@*/
1065
1066/*@constant int UINT8_MIN@*/
1067/*@constant int UINT16_MIN@*/
1068/*@constant int UINT32_MIN@*/
1069/*@constant int UINT64_MIN@*/
1070
1071/*@constant int INT_LEAST8_MIN@*/
1072/*@constant int INT_LEAST16_MIN@*/
1073/*@constant int INT_LEAST32_MIN@*/
1074/*@constant int INT_LEAST64_MIN@*/
1075
1076/*@constant int INT_LEAST8_MAX@*/
1077/*@constant int INT_LEAST16_MAX@*/
1078/*@constant int INT_LEAST32_MAX@*/
1079/*@constant int INT_LEAST64_MAX@*/
1080
1081/*@constant int UINT_LEAST8_MAX@*/
1082/*@constant int UINT_LEAST16_MAX@*/
1083/*@constant int UINT_LEAST32_MAX@*/
1084/*@constant int UINT_LEAST64_MAX@*/
1085
1086/*@constant int INT_FAST8_MIN@*/
1087/*@constant int INT_FAST16_MIN@*/
1088/*@constant int INT_FAST32_MIN@*/
1089/*@constant int INT_FAST64_MIN@*/
1090
1091/*@constant int INT_FAST8_MAX@*/
1092/*@constant int INT_FAST16_MAX@*/
1093/*@constant int INT_FAST32_MAX@*/
1094/*@constant int INT_FAST64_MAX@*/
1095
1096/*@constant int UINT_FAST8_MAX@*/
1097/*@constant int UINT_FAST16_MAX@*/
1098/*@constant int UINT_FAST32_MAX@*/
1099/*@constant int UINT_FAST64_MAX@*/
1100
1101/*@constant size_t INTPTR_MIN@*/
1102/*@constant size_t INTPTR_MAX@*/
git-cvsimport mirror of splint
This page took 0.186755 seconds and 5 git commands to generate.