test/specclauses2.c

   1 /*@-paramuse@*/
   2
   3 typedef struct
   4 {
   5   char *name;
   6   char *id;
   7   int year;
   8 } record;
   9
  10 extern void allocYear (/*@special@*/ record *r)
  11   /*@allocates r->year@*/  /* 1. Allocates clause includes *<parameter 1>.year of ... */
  12 {
  13   r->year = 23;
  14 } /* 2. Unallocated storage r->year corresponds to storage listed ... */
  15
  16 extern void setName (/*@special@*/ record *r, /*@only@*/ char *name)
  17   /*@defines r->name@*/
  18 {
  19   r->name = name;
  20 }
  21
  22 extern void setName1 (/*@special@*/ record *r, /*@only@*/ char *name)
  23   /*@defines r->name@*/
  24 {
  25   free (name);
  26 } /* 3. Storage r->name listed in defines clause not defined at ... */
  27
  28 extern void setName2 (/*@special@*/ record *r, char *name)
  29   /*@sets r->name@*/
  30 {
  31   strcpy (r->name, name);
  32 }
  33
  34 extern void setName3 (/*@special@*/ record *r, char *name)
  35   /*@sets r->name@*/
  36 {
  37 } /* 4. Storage *(r->name) listed in sets clause not defined at ... */
  38
  39 extern void setName4 (/*@special@*/ record *r, /*@only@*/ char *name)
  40   /*@sets r->name@*/
  41 {
  42   r->name = name; /* 5. Implicitly only storage r->name not released before ... */
  43 }
  44
  45 extern void allocName (/*@special@*/ record *r)
  46   /*@allocates r->name@*/
  47 {
  48   r->name = (char *) malloc (sizeof (char) * 20);
  49 }
  50
  51 extern void allocName2 (/*@special@*/ record *r)
  52   /*@allocates r->name@*/
  53 {
  54 } /* 6. Storage r->name listed in allocates clauses is not ... */
  55
  56 extern void freeName (/*@special@*/ record r)
  57   /*@releases r.name@*/
  58 {
  59   free (r.name);
  60 }
  61
  62 extern void freeName2 (/*@special@*/ record r)
  63   /*@releases r.name@*/
  64 {
  65 } /* 7. Storage r.name listed in releases clause not released */
  66
  67 extern void freeName3 (/*@special@*/ record *r)
  68   /*@releases r->name@*/
  69 {
  70   free (r->name);
  71 }
  72
  73 extern void freeName4 (/*@special@*/ record *r)
  74   /*@releases r->name@*/
  75 {
  76 } /* 8. Storage r->name listed in releases clause not released ... */