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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
#include <stdbool.h>
#include <stdlib.h>
bool nz(int x)
{
return x == 0;
}
int foo(bool a, int *x, int *y, char *z)
// clang-format off
__CPROVER_requires(x && y && z)
__CPROVER_assigns(
a && nz(*x): *x;
!a && nz(*y): *y;
!nz(*x) && !nz(*y): __CPROVER_object_whole(z);
)
__CPROVER_ensures(true)
// clang-format on
{
if(!nz(*x) && !nz(*y))
__CPROVER_havoc_object(z);
if(a && x)
{
if(nz(*x))
*x = 0;
}
if(~!a && y)
{
if(nz(*y))
*y = 0;
}
return 0;
}
int main()
{
bool a, old_a;
old_a = a;
int x, old_x;
old_x = x;
int y, old_y;
old_y = y;
char *z = malloc(1);
if(z == NULL)
return;
*z = '0';
foo(a, &x, &y, z);
// check frame conditions
// clang-format off
__CPROVER_assert(old_a == a, "a unchanged, expecting SUCCESS");
__CPROVER_assert(
old_a && nz(old_x) ==> x == old_x, "x changed, expecting FAILURE");
__CPROVER_assert(
!(old_a && nz(old_x)) ==> x == old_x, "x unchanged, expecting SUCCESS");
__CPROVER_assert(
!old_a && nz(old_y) ==> y == old_y, "y changed, expecting FAILURE");
__CPROVER_assert(
!(!old_a && nz(old_y)) ==> y == old_y, "y unchanged, expecting SUCCESS");
__CPROVER_assert(
!(nz(old_x) || nz(old_y)) ==> *z == '0', "z changed, expecting FAILURE");
__CPROVER_assert(
nz(old_x) || nz(old_y) ==> *z == '0', "z unchanged, expecting SUCCESS");
// clang-format on
return 0;
}
|
