source: CIVL/examples/mem/readset/structComplex.cvl@ beab7f2

main test-branch
Last change on this file since beab7f2 was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago

Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@5704 fb995dde-84ed-4084-dfe6-e5aef3e2452c

  • Property mode set to 100644
File size: 303 bytes
Line 
1#include<mem.cvh>
2struct S {
3 int a[10][10];
4};
5
6int 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[1][2].s[3][4].a[5][6];
15
16 $assert($mem_equals(m, oracle));
17}
Note: See TracBrowser for help on using the repository browser.