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
|
// RUN: %boogie -noVerify "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
var g0: int;
var g1: int;
var h0: [ref, name]int;
var h1: [ref, name]int;
const X: name;
procedure P(a: ref, hh: [ref, name]int) returns (b: int, hout: [ref, name]any);
modifies h1, g0;
implementation P(a: ref, hh: [ref, name]int)
returns (b: int, hout: [ref, name]any) {
start:
g0 := 5;
g1 := 6; // error: g1 is not in modifies clause
a := null; // error: in-parameters are not mutable
b := 12;
goto next;
next:
havoc g0;
havoc g1; // error: g1 is not in modifies clause
havoc a; // error: in-parameters are not mutable
havoc b;
goto more;
more:
hh[a,X] := 101; // error: in-parameter (hh) is not mutable
h0[a,X] := 102; // error: h0 is not in modifies clause
h1[a,X] := 103;
hh := h0; // error: in-parameter is not mutable
h0 := h1; // error: h0 is not in modifies clause
h1 := hh;
havoc hh; // error: in-parameter is not mutable
havoc h0; // error: h0 is not in modifies clause
havoc h1;
return;
}
procedure PX();
modifies h1, g0;
procedure PY()
modifies h1, g0;
{
start:
call PX();
call PY();
return;
}
procedure PZ()
modifies h1;
{
start:
call PX(); // error: PX has larger frame than PZ
return;
}
procedure Q() returns (x: int, y: int, h: [ref, name]int)
{
start:
return;
}
procedure QCallerBad()
{
start:
call g0, g1, h0 := Q();
return;
}
procedure QCallerGood()
modifies g0, h0;
{
var t: int;
start:
call t, g0, h0 := Q();
return;
}
procedure MismatchedTypes(x: int);
implementation MismatchedTypes(x: bool) // error
{
start:
return;
}
implementation MismatchedTypes(y: bool) // error (this time with a different name for the formal)
{
start:
return;
}
type ref, name, any;
const null : ref;
|
