test/sharing5.c

   1 extern void free (/*@out@*/ /*@only@*/ void *s);
   2 extern /*@only@*/ char *string_copy (char *s);
   3
   4 void f(/*@only@*/ char *only1, /*@only@*/ char *only2, /*@only@*/ char *only3,
   5        /*@shared@*/ char *shared)
   6 {
   7   char *local1, *local2, *local4;
   8   char **localp;
   9
  10   local1 = only1;
  11   *only1 = 'c';      /* okay */
  12   free (local1);     /* okay --- kills only1 */
  13   *only1 = 'c';      /* 1. bad --- only1 is dead */
  14
  15   if (3 > 4)
  16     {
  17       local2 = only2;
  18     }
  19   else
  20     {
  21       local2 = shared;
  22     } /* 2. Clauses exit with local2 referencing dependant storage in true */
  23
  24   free (local2);     /* 3. bad --- could free shared2 (may kill only2) */
  25
  26   localp = malloc(sizeof(char *));
  27   *localp = only3; /* 4. possible null deref */
  28
  29   local4 = only3;
  30   local4 = NULL;  /* okay */
  31
  32   localp = &only3;   /* 5. new storage not released */
  33 } /* 6. only3 may not be released [[[ only2 ??? ]]] */
  34
  35
  36
  37
  38
  39
  40
  41