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
32
33

// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

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