test/keep.c

   1 /*@only@*/ int *oglob;
   2 /*@keep@*/ int *kglob;
   3
   4 void f1 (/*@keep@*/ int *x)
   5 {
   6   kglob = x;
   7   return;
   8 }
   9
  10 void f2 (/*@keep@*/ int *x)
  11 {
  12   free (x); /* 1. Keep storage passed as only param: x */
  13 }
  14
  15 int f3 (/*@keep@*/ int *x)
  16 {
  17   int *y = malloc (sizeof (int));
  18
  19   if (y == NULL) return 3; /* 2. Keep storage not transferred before return: x */
  20
  21   *y = 3;
  22
  23   f1 (x);
  24   f1 (y);
  25
  26   return *x;
  27 }
  28
  29 int f4 (/*@only@*/ int *x)
  30 {
  31   return (f3 (x));
  32 }
  33
  34 void f5 (/*@unused@*/ /*@keep@*/ int *x)
  35 {
  36   return; /* 3. Keep storage not transferred before return: x */
  37 }
  38
  39 void f6 (/*@keep@*/ int *x)
  40 {
  41   if (*x > 3)
  42     {
  43       f2 (x);
  44     } /* 4. Variable x is kept in true branch, but live in continuation. */
  45
  46   f2 (x); /* 5. Kept storage passed as keep: f2 (x) */
  47 }
  48
  49 /*@null@*/ int *f7 (/*@null@*/ /*@keep@*/ int *x)
  50 {
  51   if (x == NULL)
  52     {
  53       ;
  54     }
  55   else
  56     {
  57       f2 (x);
  58     }
  59
  60   return x; /* 6. Kept storage x returned as implicitly only: x */
  61 }
  62
  63
  64
  65
  66