Test/inline/test5.bpl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

// 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;
}