summaryrefslogtreecommitdiff
path: root/Test/inline/test4.bpl
blob: 4a740bbcf7adc50b59434efd2d72b225f350a8db (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

procedure main(x:int)
{
	var A:[int]int;
	var i:int;
	var b:bool;
	var size:int;
	
	call i,b := find(A, size, x);

	if(b) {
		assert(i > 0 && A[i] == x);
	}

	return;
}

procedure {:inline 1} find(A:[int]int, size:int, x:int) returns (ret:int, found:bool)
{
	var i:int;
	var b:bool;

	ret := -1;
	b := false;
	found := b;
	i := 0;

	while(i < size) {
		call b := check(A, i, x);
		if(b) {
		      ret := i;
		      found := b;
		      break;
		}
	
	}

	return;

}


procedure {:inline 3} check (A:[int]int, i:int, c:int) returns (ret:bool)
	  requires i >= 0;
	  ensures (old(A[i]) > c) ==> ret == true;
{
	if(A[i] == c) {
		ret := true;
	} else {
	       ret := false;
	}
	return;
}