5 /* Library functions annotated for tainted.mts */
7 extern int remove (/*@untainted@*/ char *filename) /*@modifies fileSystem, errno@*/ ;
8 extern int rename (/*@untainted@*/ char *old, /*@untainted@*/ char *new) ;
10 extern /*@observer@*/ char *tmpnam (/*@untainted@*/ char *s) ;
12 extern FILE *fopen (/*@untainted@*/ char *filename, char *mode) ;
14 extern /*@null@*/ FILE *freopen (/*@untainted@*/ char *filename, char *mode, FILE *stream) ;
16 extern /*@null@*/ /*@tainted@*/ char *
17 fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream)
18 /*@ensures tainted s@*/
21 extern int system (/*@untainted@*/ /*@null@*/ char *s) /*@modifies fileSystem@*/ ;