Test/inline/test5.bpl


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
79

// test a case, where the inlined proc comes before the caller

procedure {:inline 2} foo()
  modifies x;
{
  x := x + 1;
}

var x:int;

procedure  bar()
  modifies x;
{
  x := 3;
  call foo();
  assert x == 4;
  call foo();
  assert x == 5;
}

// -------------------------------------------------

var Mem : [int]int;

procedure {:inline 1} P(x:int)
  modifies Mem;
{
  Mem[x] := 1;
}

procedure mainA()
  modifies Mem;
{
  Mem[1] := 0;
  call P(0);
  call P(1);
  assert Mem[1] == 0;  // error
}

procedure mainB()
  modifies Mem;
{
  Mem[1] := 0;
  call P(0);
  call P(1);
  assert Mem[1] == 1;  // good
}

procedure mainC()
  modifies Mem;
{
  Mem[1] := 0;
  call P(0);
  call P(1);
  assert Mem[1] == 1;  // good
}

// -------------------------------------------------

type ref;
var xyz: ref;

procedure xyzA();
  modifies xyz;
  ensures old(xyz) == xyz;

procedure {:inline 1} xyzB()
  modifies xyz;
{
  call xyzA();
}

procedure xyzMain()
  modifies xyz;
{
  call xyzA();
  assert old(xyz) == xyz;
  call xyzB();
}