blob: e48a7a0c9a106bcf6e1d0f9537ecb02c8c842de8 (
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
|
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;
}
|
