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
|
int nondet_int();
void foo(
int *in,
int *in1,
int *in2,
int *in3,
int *in4,
int *in5,
int *in6,
int **out1,
int **out2,
int **out3,
int **out4,
int **out5,
int **out6)
// clang-format off
__CPROVER_requires(__CPROVER_is_fresh(in, sizeof(int)))
__CPROVER_requires(__CPROVER_is_fresh(in1, sizeof(int)) || __CPROVER_pointer_in_range_dfcc(in, in1, in))
__CPROVER_requires(__CPROVER_pointer_in_range_dfcc(in, in2, in) || __CPROVER_is_fresh(in2, sizeof(int)))
__CPROVER_requires(__CPROVER_is_fresh(in3, sizeof(int)) || __CPROVER_pointer_equals(in3, in))
__CPROVER_requires(__CPROVER_pointer_equals(in4, in) || __CPROVER_is_fresh(in4, sizeof(int)))
__CPROVER_requires(__CPROVER_pointer_in_range_dfcc(in, in5, in) || __CPROVER_pointer_equals(in5, in))
__CPROVER_requires(__CPROVER_pointer_equals(in6, in) || __CPROVER_pointer_in_range_dfcc(in, in6, in))
__CPROVER_requires(__CPROVER_is_fresh(out1, sizeof(int *)))
__CPROVER_requires(__CPROVER_is_fresh(out2, sizeof(int *)))
__CPROVER_requires(__CPROVER_is_fresh(out3, sizeof(int *)))
__CPROVER_requires(__CPROVER_is_fresh(out4, sizeof(int *)))
__CPROVER_requires(__CPROVER_is_fresh(out5, sizeof(int *)))
__CPROVER_requires(__CPROVER_is_fresh(out6, sizeof(int *)))
__CPROVER_assigns(*out1, *out2, *out3, *out4, *out5, *out6)
__CPROVER_ensures(__CPROVER_is_fresh(*out1, sizeof(int)) || __CPROVER_pointer_in_range_dfcc(in, *out1, in))
__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(in, *out2, in) || __CPROVER_is_fresh(*out2, sizeof(int)))
__CPROVER_ensures(__CPROVER_is_fresh(*out3, sizeof(int)) || __CPROVER_pointer_equals(*out3, in))
__CPROVER_ensures(__CPROVER_pointer_equals(*out4, in) || __CPROVER_is_fresh(*out4, sizeof(int)))
__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(in, *out5, in) || __CPROVER_pointer_equals(*out5, in))
__CPROVER_ensures(__CPROVER_pointer_equals(*out6, in) || __CPROVER_pointer_in_range_dfcc(in, *out6, in))
// clang-format on
{
int *tmp1 = malloc(sizeof(int));
__CPROVER_assume(tmp1);
*out1 = nondet_int() ? tmp1 : in;
int *tmp2 = malloc(sizeof(int));
__CPROVER_assume(tmp2);
*out2 = nondet_int() ? tmp2 : in;
int *tmp3 = malloc(sizeof(int));
__CPROVER_assume(tmp3);
*out3 = nondet_int() ? tmp3 : in;
int *tmp4 = malloc(sizeof(int));
__CPROVER_assume(tmp4);
*out4 = nondet_int() ? tmp4 : in;
*out5 = in;
*out6 = in;
}
int main()
{
int *in, *in1, *in2, *in3, *in4, *in5, *in6;
int **out1, **out2, **out3, **out4, **out5, **out6;
foo(in, in1, in2, in3, in4, in5, in6, out1, out2, out3, out4, out5, out6);
return 0;
}
|
