test/postnotnull.c

   1 typedef struct {
   2   char *x;
   3 } T;
   4
   5 static void foo(/*@special@*/ T* x)
   6      /*@defines x->x@*/
   7      /*@post:notnull x->x@*/ ;
   8
   9 static void bar (/*@out@*/ T* x)
  10      /*@post:notnull x->x@*/
  11 {
  12   foo(x);
  13 }
  14
  15 void test()
  16 {
  17   T a;
  18   foo(&a);
  19   bar(&a);
  20 }