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 
bar(T * x)9 static void bar (/*@out@*/ T* x)
10      /*@post:notnull x->x@*/
11 {
12   foo(x);
13 }
14 
test()15 void test()
16 {
17   T a;
18   foo(&a);
19   bar(&a);
20 }
21