lib/tainted.xh

   1 /*
   2 ** tainted.xh
   3 */
   4
   5 /* Library functions annotated for tainted.mts */
   6
   7 extern int printf (/*@untainted@*/ char *format, ...) ;
   8 extern int fprintf (FILE *stream, /*@untainted@*/ char *format, ...) ;
   9 extern int sprintf (/*@out@*/ char *s, /*@untainted@*/ char *format, ...)
  10    /*@ensures s:taintedness = ...:taintedness@*/ ;
  11
  12 extern int snprintf (/*@out@*/ char *s, size_t n, /*@untainted@*/ const char *format, ...)
  13    /*@ensures s:taintedness = ...:taintedness@*/ ;
  14
  15 extern int vprintf (/*@untainted@*/ const char *format, va_list ap);
  16 extern int vfprintf(FILE *stream, /*@untainted@*/ const char *format, va_list ap);
  17 extern int vsprintf (/*@out@*/ char *str, /*@untainted@*/ const char *format, va_list ap)
  18   /*@ensures tainted str@*/ ;
  19 extern int vsnprintf (/*@out@*/ char *str, size_t size, /*@untainted@*/ const char *format, va_list ap)
  20   /*@ensures tainted str@*/ ;
  21
  22 # if 0
  23 extern int vfwprintf (FILE *stream, /*@untainted@*/ const wchar_t *format, va_list arg);
  24 extern int vswprintf (wchar_t *s, size_t n, /*@untainted@*/ const wchar_t *format, va_list arg);
  25 extern int vwprintf (/*@untainted@*/ const wchar_t *format, va_list arg);
  26 # endif
  27
  28 # if 0
  29 extern int remove (/*@untainted@*/ char *filename) /*@modifies fileSystem, errno@*/ ;
  30 extern int rename (/*@untainted@*/ char *old, /*@untainted@*/ char *new) ;
  31 extern /*@observer@*/ char *tmpnam (/*@untainted@*/ char *s) ;
  32 extern FILE *fopen (/*@untainted@*/ char *filename, char *mode) ;
  33 extern /*@null@*/ FILE *freopen (/*@untainted@*/ char *filename, char *mode, FILE *stream) ;
  34 # endif
  35
  36 extern /*@null@*/ /*@tainted@*/ char *
  37   fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream)
  38   /*@ensures tainted s@*/
  39   /*@modifies *s@*/ ;
  40
  41 extern int system (/*@untainted@*/ /*@null@*/ char *s) /*@modifies fileSystem@*/ ;
  42
  43 extern void /*@printflike@*/ syslog (int priority, /*@untainted@*/ const char *message, ...)
  44    /*@modifies fileSystem@*/ ;
  45
  46 extern char *strcpy (/*@returned@*/ /*@anytainted@*/ char *s1, /*@anytainted@*/ char *s2)
  47   /*@ensures s1:taintedness = s2:taintedness@*/ ;
  48
  49 extern char *strcat (/*@returned@*/ /*@anytainted@*/ char *s1, /*@anytainted@*/ char *s2)
  50   /*@ensures s1:taintedness = s1:taintedness | s2:taintedness@*/
  51   /*@ensures result:taintedness = s1:taintedness | s2:taintedness@*/ ;
  52
  53
  54
  55