[splint.git] / test / postnotnull.c

typedef struct {
  char *x;
} T;

static void foo(/*@special@*/ T* x)
     /*@defines x->x@*/
     /*@post:notnull x->x@*/ ;
     
static void bar (/*@out@*/ T* x)
     /*@post:notnull x->x@*/
{
  foo(x);
}

void test()
{
  T a;
  foo(&a);
  bar(&a);
}
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	}