]>
Commit | Line | Data |
---|---|---|
8fe44445 | 1 | /* |
2 | ** tainted.xh | |
3 | */ | |
4 | ||
5 | /* Library functions annotated for tainted.mts */ | |
6 | ||
7 | extern int printf (/*@untainted@*/ char *format, ...) ; | |
8 | extern int fprintf (FILE *stream, /*@untainted@*/ char *format, ...) ; | |
9 | extern int sprintf (/*@out@*/ char *s, /*@untainted@*/ char *format, ...) | |
10 | /*@ensures s:taintedness = ...:taintedness@*/ ; | |
11 | ||
d5047b91 | 12 | extern int snprintf (/*@out@*/ char *s, size_t n, /*@untainted@*/ const char *format, ...) |
13 | /*@ensures s:taintedness = ...:taintedness@*/ ; | |
14 | ||
8fe44445 | 15 | extern int vprintf (/*@untainted@*/ const char *format, va_list ap); |
16 | extern int vfprintf(FILE *stream, /*@untainted@*/ const char *format, va_list ap); | |
17 | extern int vsprintf (/*@out@*/ char *str, /*@untainted@*/ const char *format, va_list ap) | |
18 | /*@ensures tainted str@*/ ; | |
19 | extern int vsnprintf (/*@out@*/ char *str, size_t size, /*@untainted@*/ const char *format, va_list ap) | |
20 | /*@ensures tainted str@*/ ; | |
21 | ||
22 | # if 0 | |
23 | extern int vfwprintf (FILE *stream, /*@untainted@*/ const wchar_t *format, va_list arg); | |
24 | extern int vswprintf (wchar_t *s, size_t n, /*@untainted@*/ const wchar_t *format, va_list arg); | |
25 | extern int vwprintf (/*@untainted@*/ const wchar_t *format, va_list arg); | |
26 | # endif | |
27 | ||
28 | # if 0 | |
29 | extern int remove (/*@untainted@*/ char *filename) /*@modifies fileSystem, errno@*/ ; | |
30 | extern int rename (/*@untainted@*/ char *old, /*@untainted@*/ char *new) ; | |
31 | extern /*@observer@*/ char *tmpnam (/*@untainted@*/ char *s) ; | |
32 | extern FILE *fopen (/*@untainted@*/ char *filename, char *mode) ; | |
33 | extern /*@null@*/ FILE *freopen (/*@untainted@*/ char *filename, char *mode, FILE *stream) ; | |
34 | # endif | |
35 | ||
36 | extern /*@null@*/ /*@tainted@*/ char * | |
37 | fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream) | |
38 | /*@ensures tainted s@*/ | |
39 | /*@modifies *s@*/ ; | |
40 | ||
41 | extern int system (/*@untainted@*/ /*@null@*/ char *s) /*@modifies fileSystem@*/ ; | |
42 | ||
43 | extern void /*@printflike@*/ syslog (int priority, /*@untainted@*/ const char *message, ...) | |
44 | /*@modifies fileSystem@*/ ; | |
45 | ||
46 | extern char *strcpy (/*@returned@*/ /*@anytainted@*/ char *s1, /*@anytainted@*/ char *s2) | |
47 | /*@ensures s1:taintedness = s2:taintedness@*/ ; | |
48 | ||
49 | extern char *strcat (/*@returned@*/ /*@anytainted@*/ char *s1, /*@anytainted@*/ char *s2) | |
50 | /*@ensures s1:taintedness = s1:taintedness | s2:taintedness@*/ | |
51 | /*@ensures result:taintedness = s1:taintedness | s2:taintedness@*/ ; | |
52 | ||
53 | ||
54 | ||
55 |