ex13-change-orig.c
1 |
|
---|---|
2 |
int nondet_int();
|
3 |
|
4 |
int get_even(int a, int b){ |
5 |
int rnd = 0; |
6 |
if (a > 5 || b < 5){ |
7 |
rnd = a; |
8 |
} else {
|
9 |
rnd = b; |
10 |
} |
11 |
return rnd;
|
12 |
} |
13 |
|
14 |
int test1(int a){ |
15 |
return get_even(a, 5); |
16 |
} |
17 |
|
18 |
int test2(int a){ |
19 |
return get_even(5, a); |
20 |
} |
21 |
|
22 |
void main(void) |
23 |
{ |
24 |
|
25 |
int a = nondet_int();
|
26 |
|
27 |
int a1 = test1(a);
|
28 |
int a2 = test2(a);
|
29 |
|
30 |
assert(a1 == a2); |
31 |
|
32 |
} |