test/specclauses3.c

   1 typedef struct
   2 {
   3   int id;
   4   char *name;
   5 } *record;
   6
   7 int *badResult (void)
   8   /* 1. Function result is used in defines clause of badResult but ...
   9      2. Special clause accesses field of non-struct or union result */
  10    /*@defines result->name@*/
  11 {
  12   return NULL; /* 3. Null storage returned as non-null: NULL */
  13 }
  14
  15 /*@special@*/ record createName (/*@only@*/ char *name)
  16    /*@defines result->name@*/
  17 {
  18   record res = (record) malloc (sizeof (*res));
  19
  20   assert (res != NULL);
  21   res->name = name;
  22   return res;
  23 }
  24
  25 /*@special@*/ record createName2 (void)
  26    /*@defines result->name@*/
  27 {
  28   record res = (record) malloc (sizeof (*res));
  29   return res; /* 4. Undefined storage res->name corresponds to storage listed ...
  30                  5. Possibly null storage res returned as non-null: res */
  31 }
  32
  33 /*@special@*/ record createName3 (void)
  34    /*@defines result->id@*/
  35    /*@allocates result->name@*/
  36 {
  37   record res = (record) malloc (sizeof (*res));
  38
  39   assert (res != NULL);
  40
  41   res->name = (char *) malloc (sizeof (char) * 23);
  42   res->id = 21;
  43   return res;
  44 }
  45
  46 /*@special@*/ record createName4 (void)
  47    /*@defines result->id@*/
  48    /*@allocates result->name@*/
  49 {
  50   record res = (record) malloc (sizeof (*res));
  51
  52   assert (res != NULL);
  53
  54   res->id = 21;
  55   return res; /* 6. Unallocated storage res->name corresponds to storage ... */
  56 }
  57
  58
  59
  60
  61