source: CIVL/examples/mem/readset/call.cvl@ 15298b6

1.23 2.0 acw/focus-triggers main test-branch
Last change on this file since 15298b6 was 4501911, checked in by Ziqing Luo <ziqing@…>, 7 years ago

add new examples to CIVL

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5225 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 324 bytes
Line 
1#include<mem.cvh>
2int f(int x, int y) {
3 return x + y;
4}
5
6int main() {
7 int x,y,z;
8
9 x = 0, y = 0, z = 0;
10 $read_set_push();
11 int a = f(y, z);
12
13 $mem m = $read_set_pop();
14 $mem oracle = ($mem)&y;
15
16 oracle = $mem_union(oracle, ($mem)&z);
17 oracle = $mem_union(oracle, ($mem)&a);
18 $assert($mem_equals(m, oracle));
19}
Note: See TracBrowser for help on using the repository browser.