blob: 72bf0d8c4f246829854b7a268004b9b5f40e1be4 (
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
|
// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
procedure foo () returns ()
{
var i: int;
var j: int;
var n: int;
entry:
assume n >= 4;
i := 0;
j := i + 1;
// n >= 4 AND i = 0 AND j = i+1
goto exit, loop0;
loop0:
// n >= 4 AND i >= 0 AND j = i+1
assume j <= n;
goto loop1;
loop1:
// n >= 4 AND i >= 0 AND j = i+1 AND j <= n
i := i + 1;
goto loop2;
loop2:
j := j + 1;
// n >= 4 AND i >= 1 AND j = i+1 AND j <= n+1
goto loop0, exit;
exit:
// n >= 4 AND i >= 0 AND j = i+1 AND j <= n+1
return;
}
|
