source: CIVL/mods/dev.civl.com/examples/mem/readset/pointer.cvl@ cb4d4f4

main test-branch
Last change on this file since cb4d4f4 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: 359 bytes
RevLine 
[4501911]1#include<mem.cvh>
2int main() {
3 int x,y,z;
4 int * p, * q;
5
6 x = 0, y = 0, z = 0;
7 p = &x; q = &y;
8 $read_set_push();
9 int a = *p + *q;
10
11 $mem m = $read_set_pop();
12 $mem oracle = ($mem)&x;
13
14 oracle = $mem_union(oracle, ($mem)&y);
15 oracle = $mem_union(oracle, ($mem)&p);
16 oracle = $mem_union(oracle, ($mem)&q);
17 $assert($mem_equals(m, oracle));
18}
Note: See TracBrowser for help on using the repository browser.