1.23
2.0
acw/focus-triggers
main
test-branch
| Rev | Line | |
|---|
| [4501911] | 1 | #include<mem.cvh>
|
|---|
| 2 | struct S {
|
|---|
| 3 | int a[10][10];
|
|---|
| 4 | };
|
|---|
| 5 |
|
|---|
| 6 | int main() {
|
|---|
| 7 | struct T {
|
|---|
| 8 | struct S s[10][10];
|
|---|
| 9 | } t[10][10];
|
|---|
| 10 |
|
|---|
| 11 | $read_set_push();
|
|---|
| 12 | t[0][1].s[2][3].a[4][5] = t[1][2].s[3][4].a[5][6];
|
|---|
| 13 | $mem m = $read_set_pop();
|
|---|
| 14 | $mem oracle = ($mem)&t[0][1].s[2][3].a[4][5];
|
|---|
| 15 |
|
|---|
| 16 | oracle = $mem_union(oracle, ($mem)&t[1][2].s[3][4].a[5][6]);
|
|---|
| 17 | $assert($mem_equals(m, oracle));
|
|---|
| 18 | }
|
|---|
Note:
See
TracBrowser
for help on using the repository browser.
