summaryrefslogtreecommitdiff
path: root/Test/AbsHoudini/multi.bpl
blob: a33817ac90fd1911fca7ceb4b46e9addc435db17 (plain)
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);
}