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