test/tainted/tainted.xh

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