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