1/*
2** tainted.xh
3*/
4
5/* Library functions annotated for tainted.mts */
6
7extern int remove (/*@untainted@*/ char *filename) /*@modifies fileSystem, errno@*/ ;
8extern int rename (/*@untainted@*/ char *old, /*@untainted@*/ char *new) ;
9
10extern /*@observer@*/ char *tmpnam (/*@untainted@*/ char *s) ;
11
12extern FILE *fopen (/*@untainted@*/ char *filename, char *mode) ;
13
14extern int sprintf (/*@out@*/ char *s, /*@untainted@*/ char *format, ...)
15   /*@ensures s:taintedness = ...:taintedness@*/ ;
16
17extern int printf (/*@untainted@*/ char *format, ...) ;
18
19extern /*@null@*/ FILE *freopen (/*@untainted@*/ char *filename, char *mode, FILE *stream) ;
20
21extern /*@null@*/ /*@tainted@*/ char *
22  fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream)
23  /*@ensures tainted s@*/
24  /*@modifies *s@*/ ;
25
26extern int system (/*@untainted@*/ /*@null@*/ char *s) /*@modifies fileSystem@*/ ;
27
28extern char *strcpy (/*@returned@*/ char *s1, char *s2)
29  /*@ensures s1:taintedness = s2:taintedness@*/ ;
30
31extern char *strcat (/*@returned@*/ char *s1, char *s2)
32  /*@ensures s1:taintedness = s1:taintedness | s2:taintedness@*/
33  /*:ensures result:tainted = s1:tainted, s2:tainted)@*/ ;
34
35