source: CIVL/examples/mem/readset/simple.cvl

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