File: tainted.xh

package info (click to toggle)
splint 1%3A3.1.2%2Bdfsg-5
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, sid
  • size: 21,004 kB
  • sloc: ansic: 150,869; yacc: 3,465; sh: 3,034; makefile: 2,157; lex: 412
file content (55 lines) | stat: -rw-r--r-- 2,288 bytes parent folder | download | duplicates (7)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
/*
** tainted.xh
*/

/* Library functions annotated for tainted.mts */

extern int printf (/*@untainted@*/ char *format, ...) ;
extern int fprintf (FILE *stream, /*@untainted@*/ char *format, ...) ;
extern int sprintf (/*@out@*/ char *s, /*@untainted@*/ char *format, ...) 
   /*@ensures s:taintedness = ...:taintedness@*/ ;

extern int snprintf (/*@out@*/ char *s, size_t n, /*@untainted@*/ const char *format, ...)
   /*@ensures s:taintedness = ...:taintedness@*/ ;

extern int vprintf (/*@untainted@*/ const char *format, va_list ap);
extern int vfprintf(FILE *stream, /*@untainted@*/ const char *format, va_list ap);
extern int vsprintf (/*@out@*/ char *str, /*@untainted@*/ const char *format, va_list ap)
  /*@ensures tainted str@*/ ;
extern int vsnprintf (/*@out@*/ char *str, size_t size, /*@untainted@*/ const char *format, va_list ap)
  /*@ensures tainted str@*/ ;

# if 0
extern int vfwprintf (FILE *stream, /*@untainted@*/ const wchar_t *format, va_list arg);
extern int vswprintf (wchar_t *s, size_t n, /*@untainted@*/ const wchar_t *format, va_list arg);
extern int vwprintf (/*@untainted@*/ const wchar_t *format, va_list arg);
# endif

# if 0
extern int remove (/*@untainted@*/ char *filename) /*@modifies fileSystem, errno@*/ ;
extern int rename (/*@untainted@*/ char *old, /*@untainted@*/ char *new) ;
extern /*@observer@*/ char *tmpnam (/*@untainted@*/ char *s) ;
extern FILE *fopen (/*@untainted@*/ char *filename, char *mode) ;
extern /*@null@*/ FILE *freopen (/*@untainted@*/ char *filename, char *mode, FILE *stream) ;
# endif

extern /*@null@*/ /*@tainted@*/ char *
  fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream) 
  /*@ensures tainted s@*/ 
  /*@modifies *s@*/ ;

extern int system (/*@untainted@*/ /*@null@*/ char *s) /*@modifies fileSystem@*/ ;

extern void /*@printflike@*/ syslog (int priority, /*@untainted@*/ const char *message, ...)
   /*@modifies fileSystem@*/ ;

extern char *strcpy (/*@returned@*/ /*@anytainted@*/ char *s1, /*@anytainted@*/ char *s2) 
  /*@ensures s1:taintedness = s2:taintedness@*/ ;

extern char *strcat (/*@returned@*/ /*@anytainted@*/ char *s1, /*@anytainted@*/ char *s2) 
  /*@ensures s1:taintedness = s1:taintedness | s2:taintedness@*/ 
  /*@ensures result:taintedness = s1:taintedness | s2:taintedness@*/ ;