1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
int x, y;
int z[10];
void h(int w) {
x = x + 1;
y = y + 1;
}
_Bool strict_sorted(int a[], int len, int s) {
int i;
for (i = s; i < len-1; i++) {
if (a[i] >= a[i+1])
return 0;
}
return 1;
}
_Bool sorted(int a[], int len, int s) {
int i;
for (i = s; i < len-1; i++) {
if (a[i] > a[i+1])
return 0;
}
return 1;
}
int g (int w) {
int i;
int local_arr[50];
assert(w >= 1);
x = w;
w--;
y = w;
for(i = 0; i < 10; i++)
z[i] = i;
assert(strict_sorted(z,10,0));
assert(x > y);
}
int f (int j, int k) {
int i;
assert(j > k);
assert(j >= 0);
assert((k > 10) && (k < 20));
j -= k;
g(j);
j = k;
y = k;
g(j);
h(j);
assert(sorted(z,10,5));
assert(x >= y);
}
int main () {
int x, y;
__CPROVER_assume (x > y);
__CPROVER_assume (x >= 0);
__CPROVER_assume ((y > 15) && (y < 18));
f(x,y);
}
|
