test/specclauses4.c

   1 /*@-paramuse@*/
   2
   3 typedef struct
   4 {
   5   int id;
   6   char *name;
   7 } *record;
   8
   9 void usename (/*@special@*/ char **name)
  10    /*@uses *name@*/
  11    /*@pre:isnull *name@*/
  12 {
  13   **name = 'a'; /* 1. Dereference of null pointer *name: **name */
  14 }
  15
  16 void callname (void)
  17 {
  18   char **s;
  19
  20   s = (char **) malloc (sizeof (char *));
  21   assert (s != NULL);
  22   *s = (char *) malloc (sizeof (char));
  23   assert (*s != NULL);
  24
  25   **s = 'a';
  26
  27   usename (s); /* 2. Non-null storage *s corresponds to storage listed in ... */
  28   free (*s);
  29   free (s);
  30 }
  31
  32 void nullname (/*@special@*/ char **name)
  33    /*@post:isnull *name@*/
  34 {
  35   *name = NULL;
  36 }
  37
  38 void nullname2 (/*@special@*/ char **name)
  39    /*@post:isnull *name@*/
  40 {
  41   ;
  42 } /* 3. Non-null storage *name corresponds to storage listed in ... */
  43
  44
  45
  46
  47