blob: 8965f93ebac16e0568bdefac8ef5ec9c3ba59c17 (
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
|
var g:int;
var h:int; //not modified
var k:int; //modified in a procedure call
procedure 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: assert (b == a);
L2: g := old(g);
return;
}
procedure Bar()
modifies k;
{
k := 0;
return;
}
|