test/ensures.c

   1 typedef /*@null@*/ char *ncp;
   2
   3 void notnullname (ncp *name)
   4    /*@ensures notnull *name@*/
   5 {
   6   **name = 'a';  /* ensures.c:6:4: Dereference of possibly null pointer *name: **name */
   7 } /* Possibly null storage *name corresponds to storage listed in */
   8
   9 void nullname (/*@unused@*/ char **name)
  10    /*@ensures isnull *name@*/
  11 {
  12   ;
  13 } /* ensures.c:13:2: Non-null storage *name corresponds to storage listed in ensures */
  14
  15 void nullname2 (char **name)
  16    /*@ensures isnull *name@*/
  17 {
  18   *name = NULL;
  19 }
  20
  21 void callname (void)
  22 {
  23   char **s;
  24
  25   s = (char **) malloc (sizeof (char *));
  26   assert (s != NULL);
  27   *s = NULL;
  28
  29   notnullname (s);
  30   **s = 'a'; /* okay! */
  31
  32   nullname (s);
  33   **s = 'a'; /* ensures.c:33:4: Dereference of null pointer *s: **s */
  34
  35   free (*s);
  36   free (s);
  37 }
  38