blob: 463cecf0728c15f0a8bf4bf3488a88ff6559be5c (
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
|
// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -deterministicExtractLoops -recursionBound:4 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
var g:int;
var h:int; //not modified
var k:int; //modified in a procedure call
procedure {:entrypoint} Foo(a:int)
modifies g;
modifies h;
modifies k;
//ensures g == old(g);
{
var b: int;
b := 0;
g := a;
h := 5;
LH: //assert (b + g == a);
if (g == 0) {
goto LE;
}
//assume (b + g == a); // to help the loop extraction figure out the loop invariant
b := b + 1;
call Bar();
g := g - 1;
if (b > 100) {
goto L2;
}
goto LH;
LE:
L2: //g := old(g);
//assert (b == a);
assume (b != a);
return;
}
procedure Bar()
modifies k;
{
k := 0;
return;
}
|
