blob: 017dcd85a257063b132369f3cc5e3256f26199e6 (
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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
// RUN: %boogie -noinfer "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
var x: int;
var y: int;
procedure P()
modifies x;
ensures x == old(x) + 1;
{
start:
x := 1 + x;
return;
}
procedure Q();
modifies x;
ensures x == old(x) + 1;
implementation Q()
{
start:
x := 1 + x;
return;
}
procedure R()
modifies x;
ensures x == old(x) + 1;
{
start:
return;
} // error: does not establish postcondition
procedure Swap()
modifies x, y;
ensures x == old(y) && y == old(x);
{
var t: int;
start:
goto A, B;
A:
t := x;
x := y;
y := t;
goto end;
B:
x := x - y; // x == old(x) - old(y)
y := y + x; // y == old(y) + (old(x) - old(y)) == old(x)
x := y - x; // x == old(x) - (old(x) - old(y)) == old(y)
goto end;
end:
return;
}
procedure OutParam0(x: int) returns (y: int)
ensures y == x + 1;
{
start:
y := x + 1;
return;
}
// OutParam1 is like OutParam0, except that there's now a separate
// implementation declaration, which means that the specification
// and body use different AST nodes for the formal parameters. This
// may make a difference in the various substitutions going on.
// (Indeed, a previous bug caused OutParam0 to verify but not OutParam1.)
procedure OutParam1(x: int) returns (y: int);
ensures y == x + 1;
implementation OutParam1(x: int) returns (y: int)
{
start:
y := x + 1;
return;
}
var a: [ref]int;
var b: [ref]int;
procedure SwapElems(o: ref) returns (p: ref)
modifies a, b;
ensures a[o] == old(b[p]) && b[o] == old(a[p]);
{
var ta: int, tb: int;
start:
goto A, B, C;
A:
havoc p;
goto B, C;
B:
ta := a[p];
tb := b[p];
a[o] := tb;
b[o] := ta;
return;
C:
assume a[o] == b[o];assume false;
p := o;
return;
}
//-------------------------------------------------------------------------
// Test old in Boogie PL code
//-------------------------------------------------------------------------
var Global0: int;
// Good
procedure OldInCode0()
requires Global0 >= 0;
ensures Global0 <= old(Global0) + 1;
modifies Global0;
{
var local0: int;
start:
goto A,B;
A:
assert Global0 == old(Global0);
return;
B:
local0 := Global0 + 1;
local0 := local0 - 1;
Global0 := old(local0 + 1);
return;
}
type ref;
|
