test/null4.c

   1 # include "bool.h"
   2
   3 /*@only@*/ /*@null@*/ int *p;
   4
   5 extern /*@truenull@*/ bool isNull (/*@null@*/ int *p);
   6
   7 void f (void)
   8 {
   9   if (p != NULL) return;
  10   else
  11     {
  12       p = malloc (24);
  13       if (p == NULL) exit (EXIT_FAILURE);
  14       *p = 3;
  15     }
  16 }
  17
  18 void f1 (void)
  19 {
  20   if (p != NULL) return;
  21
  22   p = malloc (24);
  23   if (p == NULL) exit (EXIT_FAILURE);
  24   *p = 3;
  25 }
  26
  27 int f2 (void)
  28 {
  29   if (p == NULL) return 0;
  30   return *p;
  31 }
  32
  33 int f3 (void)
  34 {
  35   if (isNull(p)) return 0;
  36   return *p;
  37 }
  38
  39 void g (void)
  40 {
  41   if (p == NULL) return;
  42
  43   p = malloc (24);  /* 1. Only storage p not released before assignment */
  44   if (p == NULL) exit (EXIT_FAILURE);
  45   *p = 3;
  46 }
  47