]>
Commit | Line | Data |
---|---|---|
68de3f33 | 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 | ||
3e3ec469 | 9 | static void bar (/*@out@*/ T* x) |
68de3f33 | 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 | } |