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
|
function {:existential true} {:absdomain "ImplicationDomain"} b1(x1: bool, x2: bool) : bool;
function {:existential true} {:absdomain "ImplicationDomain"} b2(x1: bool, x2: bool) : bool;
function {:existential true} {:absdomain "PowDomain"} b3(x1: int) : bool;
function {:existential true} {:absdomain "PowDomain"} b4(x1: bv32) : bool;
function {:existential true} {:absdomain "EqualitiesDomain"} b5(x: int, y: int, z: int, w:int) : bool;
function {:builtin "bvslt"} BV_SLT(x: bv32, y: bv32) : bool;
var x: int;
var flag: bool;
// Test implication domain
procedure foo ()
modifies x, flag;
{
flag := true;
x := 0;
assert b1(flag, x == 0);
flag := false;
assert b2(flag, x == 0);
}
// Test for PowDomain(int)
procedure bar1 ()
modifies x, flag;
{
x := 2;
if(*) { x := 16; }
assert b3(x);
}
// Test for PowDomain(bv32)
procedure bar2 ()
modifies x, flag;
{
var s: bv32;
s := 2bv32;
if(*) { s := 16bv32; }
assert b4(s);
}
// Test for EqualitiesDomain
procedure baz ()
modifies x, flag;
{
var y: int;
var z: int;
var w: int;
assume x == y;
assume x == z;
if(*) {
x := x + 1;
y := y + 1;
} else {
x := x + 2;
y := y + 2;
}
assume x == w;
assert b5(x,y,z,w);
}
|
