]>
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 |