test/tainted/taintedimplicit.c

   1 char *taintme (char *s)
   2      /*@ensures result:taintedness = s:taintedness@*/
   3 {
   4   char *res = (char *) malloc (sizeof (*res) * strlen (s));
   5   assert (res != NULL);
   6   strcpy (res, s);
   7   return res;
   8 }
   9
  10 void safecall (/*@untainted@*/ char *s)
  11 {
  12   (void) system (taintme (s)); /* okay */
  13 }
  14
  15 void dangerouscall (/*@tainted@*/ char *s)
  16 {
  17   (void) system (taintme (s)); /* error */
  18 }