blob: 5e01f01999c8a10905a5e581225d1e01582a2d15 (
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
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class C {
var data: int;
ghost var gdata: int;
ghost method Init_ModifyNothing() { }
ghost method Init_ModifyThis() modifies this;
{
data := 6; // error: assignment to a non-ghost field
gdata := 7;
}
ghost method Init_ModifyStuff(c: C) modifies this, c; { }
method NonGhostMethod() { print "hello\n"; }
ghost method GhostMethodWithModifies(x: int) modifies this; { gdata := gdata + x; }
}
method M0(IS: set<int>)
{
forall (i | 0 <= i < 20) {
i := i + 1; // error: not allowed to assign to bound variable
}
var k := 0;
forall (i | 0 <= i < 20) {
k := k + i; // error: not allowed to assign to local k, since k is not declared inside forall block
}
forall (i | 0 <= i < 20)
ensures true;
{
var x := i;
x := x + 1;
}
ghost var y;
var z;
forall (i | 0 <= i)
ensures true;
{
var x := i;
x := x + 1;
y := 18; // (this statement is not allowed, since y is declared outside the forall, but that check happens only if the first resolution pass of the forall statement passes, which it doesn't in this case because of the next line)
z := 20; // error: assigning to a non-ghost variable inside a ghost forall block
}
forall (i | 0 <= i)
ensures true;
{
ghost var x := i;
x := x + 1; // cool
}
var ca := new C[20];
forall (i | 0 <= i < 20) {
ca[i] := new C; // error: new allocation not allowed
}
forall (i | 0 <= i < 20)
ensures true;
{
var c := new C; // error: 'new' not allowed in ghost context
var d := new C.Init_ModifyNothing(); // error: 'new' not allowed in ghost context
var e := new C.Init_ModifyThis(); // error: 'new' not allowed in ghost context
var f := new C.Init_ModifyStuff(e); // error: 'new' not allowed in ghost context
c.Init_ModifyStuff(d); // error: not allowed to call method with modifies clause in ghost context
c.NonGhostMethod(); // error: only allowed to call ghost methods (because of possible 'print' statements, sigh)
}
}
method M1() {
forall (i | 0 <= i < 20) {
assert i < 100;
if (i == 17) { break; } // error: nothing to break out of
}
forall (i | 0 <= i < 20) ensures true; {
if (i == 8) { return; } // error: return not allowed inside forall block
}
var m := 0;
label OutsideLoop:
while (m < 20) {
forall (i | 0 <= i < 20) {
if (i == 17) { break; } // error: not allowed to break out of loop that sits outside forall
if (i == 8) { break break; } // error: ditto (also: attempt to break too far)
if (i == 9) { break OutsideLoop; } // error: ditto
}
m := m + 1;
}
forall (i | 0 <= i < 20) {
var j := 0;
while (j < i) {
if (j == 6) { break; } // fine
if (j % 7 == 4) { break break; } // error: attempt to break out too far
if (j % 7 == 4) { break OutsideLoop; } // error: attempt to break to place not in enclosing scope
j := j + 1;
}
}
}
method M2() {
var a := new int[100];
forall (x | 0 <= x < 100)
ensures true;
{
a[x] :| assume a[x] > 0; // error: not allowed to update heap location in a proof-forall statement
}
}
method M3(c: C)
requires c != null;
{
forall x {
c.GhostMethodWithModifies(x); // error: not allowed to call method with nonempty modifies clause
}
forall x
ensures true;
{
c.GhostMethodWithModifies(x); // error: not allowed to call method with nonempty modifies clause
}
}
|
