source: CIVL/mods/dev.civl.com/examples/mem/mem_tests/mem_union.cvl@ e49edeb

1.23 2.0 main test-branch
Last change on this file since e49edeb was aad342c, checked in by Stephen Siegel <siegel@…>, 3 years ago

Performing huge refactor to incorporate ABC, GMC, and SARL into CIVL repo and use Java modules.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5664 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 746 bytes
Line 
1#include<mem.cvh>
2
3$input int N;
4$assume(N > 10);
5int a[N][N];
6
7int main() {
8 $mem m = &a[0 .. N-4][0 .. N-1];
9
10 m = $mem_union(m, &a[0 .. N-1][0 .. N-1]);
11 $assert($mem_contains(m, &a));
12
13 m = &a[0 .. 3][0 .. 4];
14 m = $mem_union(m, &a[1 .. 4][1 .. 5]);
15 $assert(!$mem_contains(m, &a[0 .. 4][0 .. 5]));
16
17 m = &a[0 .. 3][0 .. 4];
18 m = $mem_union(m, &a[1 .. 4][0 .. 4]);
19 $assert($mem_contains(m, &a[0 .. 4][0 .. 4]));
20 $assert(!$mem_contains(m, &a[0 .. 4][0 .. 5]));
21
22 m = &a[3][4];
23 m = $mem_union(m, &a[4][5]);
24 $assert(!$mem_contains(m, &a[3 .. 4][4 .. 5]));
25
26 m = &a[3][4];
27 m = $mem_union(m, &a[5][4]);
28 $assert(!$mem_contains(m, &a[3 .. 5][4]));
29 m = $mem_union(m, &a[4][4]);
30 $assert($mem_contains(m, &a[3 .. 5][4]));
31}
Note: See TracBrowser for help on using the repository browser.