Test/inline/test2.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


var glb:int;

procedure calculate()
modifies glb;
{
	var x:int;
	var y:int;
	
	y := 5;

	call x := increase(y);
	
	return;
}


procedure {:inline 1} increase (i:int) returns (k:int)
modifies glb;
{
	var j:int;
	
	j := i;
	j := j + 1;
	
	glb := glb + j;

	k := j;

	return;
}