test/specclauses.c

   1 typedef struct
   2 {
   3   char *name;
   4   char *id;
   5   int year;
   6 } record;
   7
   8 extern void setName (/*@special@*/ record *r, /*@only@*/ char *name)
   9   /*@defines r->name@*/ ;
  10
  11 extern /*@observer@*/ char *getName (/*@special@*/ record r)
  12   /*@uses r.name@*/ ;
  13
  14 extern void freeName (/*@special@*/ record r)
  15   /*@releases r.name@*/ ;
  16
  17 extern /*@observer@*/ char *f (/*@only@*/ char *name, char *id)
  18 {
  19   record r;
  20
  21   if (0 == 1)
  22     {
  23       setName (&r, name);
  24       return (getName (r)); /* r.name not released */
  25     }
  26   else if (1 == 2)
  27     {
  28       return (getName (r)); /* r.name not defined */
  29     }
  30   else if (2 == 3)
  31     {
  32       r.name = malloc (sizeof (char) * 12);
  33       setName (&r, name); /* r.name allocated, memory leak */
  34       return id; /* r.name not released */
  35     }
  36   else
  37     {
  38       setName (&r, name);
  39       freeName (r);
  40       printf ("%s\n", r.name); /* dead! */
  41       freeName (r);
  42       return id;
  43     }
  44 }
  45