test/specclauses6.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    /*@requires isnull *name@*/
  12    /*@ensures notnull *name@*/
  13 {
  14   **name = 'a'; /* 1. Dereference of null pointer *name: **name */
  15 }
  16
  17 void callname (void)
  18 {
  19   char **s;
  20
  21   s = (char **) malloc (sizeof (char *));
  22   assert (s != NULL);
  23   *s = (char *) malloc (sizeof (char));
  24   assert (*s != NULL);
  25
  26   **s = 'a';
  27
  28   usename (s); /* 2. Non-null storage *s corresponds to storage listed in ... */
  29   **s = 'a'; /* 3. null! */
  30   free (*s);
  31   free (s);
  32 }
  33
  34 void nullname (/*@special@*/ char **name)
  35    /*@post:isnull *name@*/
  36 {
  37   *name = NULL;
  38 }
  39
  40 void nullname2 (/*@special@*/ char **name)
  41    /*@post:isnull *name@*/
  42 {
  43   ;
  44 } /* 3. Non-null storage *name corresponds to storage listed in ... */
  45
  46
  47
  48
  49