test/null3.c

   1 # include "bool.h"
   2
   3 typedef /*@null@*/ int *nip;
   4 /*@only@*/ nip gnip;
   5 /*@only@*/ int *gip;
   6
   7 void g(int *y);
   8
   9 /*@truenull@*/ bool ptrpred (nip x)
  10 {
  11   return (x == NULL);
  12 }
  13
  14 void f3 (/*@only@*/ nip x)
  15 {
  16   *gnip = 3; /* 1. Possible dereference of null pointer: *gnip */
  17   *gip = 3;  /* okay */
  18
  19   if (x) free (x);
  20 }
  21
  22 /*@only@*/ int *f (nip arg0, nip arg1, nip arg2, /*@only@*/ int *aip)
  23 {
  24   int *y = (int *) malloc (sizeof (int));
  25   int *z = (int *) malloc (sizeof (int));
  26
  27   *arg0 = 3; /* 2. Possible dereference of null pointer: *arg0 */
  28
  29   if (arg1)
  30     {
  31       *arg1 = 7; /* okay */
  32     }
  33   else
  34     {
  35       free (y); /* 3. Possibly null storage passed as non-null param: y */
  36
  37       *z = 3;   /* 4. Possible dereference of null pointer: *z */
  38       return z; /* 5. Only storage not released before return: aip */
  39     }
  40
  41   /* arg1 is guarded */
  42
  43   *arg1 = 3; /* okay */
  44   *arg2 = 5; /* 6. Possible dereference of null pointer: *arg2 */
  45   *gip = 6;  /* okay */
  46
  47   if (z) { *z = 3; }
  48
  49   if (gnip) { free (gnip); } else { ; } /* okay */
  50
  51   gnip = z;  /* okay */
  52   *gnip = 3; /* 7. Possible dereference of null pointer: *gnip */
  53   gip = z;   /* 8, 9. uses z after release, only z not released */
  54              /* Note: gip is possibly null now  +++ kept*/
  55   gnip = aip; /* 10. Only storage gnip not released before assignment: gnip = aip */
  56   *gnip = 3; /* okay */
  57
  58   if (y)
  59     {
  60       return y; /* 11, 12. Returned storage y not completely defined,
  61                    Function returns with non-null global gip referencing null */
  62     }
  63   else
  64     {
  65       return y; /* 13, 14, 15. Possibly null storage returned as non-null: y,
  66                    Returned storage y not completely defined,
  67                    Function returns with non-null global gip referencing null */
  68     }
  69 }
  70
  71 void f2 (void)
  72 {
  73   *gnip = 3; /* 16. Possible dereference of null pointer: *gnip */
  74   *gip = 3;  /* okay */
  75 }
  76
  77
  78
  79