[splint.git] / test / modtest.lcl

int x, y;
int ai[];
int bi[];
typedef struct _ts { int a; int b; } tst;
tst ts;
tst *tstp ;

int f (int i[], int *j) int ai[]; int x, y; tst ts; tst* tstp; 
{
  let elt be ai[6];
  modifies elt, x, ai[3], ai[3+6], ai[x'], ts.a, tstp'->a, ts;
  ensures true;
}

int g (int a[], int *p) int x, y;
{
   modifies x, y;
   ensures true;
}
Commit	Line	Data
885824d3	1	int x, y;
	2	int ai[];
	3	int bi[];
	4	typedef struct _ts { int a; int b; } tst;
	5	tst ts;
	6	tst *tstp ;
	7
	8	int f (int i[], int j) int ai[]; int x, y; tst ts; tst tstp;
	9	{
	10	let elt be ai[6];
	11	modifies elt, x, ai[3], ai[3+6], ai[x'], ts.a, tstp'->a, ts;
	12	ensures true;
	13	}
	14
	15	int g (int a[], int *p) int x, y;
	16	{
	17	modifies x, y;
	18	ensures true;
	19	}
	20