test/modtest.lcl

   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