test/returned.c

   1 extern char *returnme (/*@returned@*/ char *s);
   2
   3 /*@only@*/ char *f (void)
   4 {
   5   char *s = (char *) malloc (sizeof (char));
   6   *s = 'a';
   7
   8   if (3 > 4)
   9     {
  10       return s;
  11     }
  12   else
  13     {
  14       return returnme (s);
  15     }
  16 }