blob: 3146147e7372c31115dd8686f49b675b2c9c984d (
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
|
copredicate P(b: bool)
{
!b && Q(null)
}
copredicate Q(a: array<int>)
{
a == null && P(true)
}
//copredicate A() { B() }
//predicate B() { A() } // error: SCC of a copredicate must include only copredicates
copredicate D()
reads this; // error: copredicates are not allowed to have a reads clause -- WHY NOT?
{
true
}
copredicate S(d: set<int>)
{
this.Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
this.S#[5](d) &&
S#[5](d) &&
S#[_k](d) // error: _k is not an identifier in scope
}
comethod CM(d: set<int>)
{
var b;
b := this.S#[5](d);
b := S#[5](d);
this.CM#[5](d);
CM#[5](d);
}
module GhostCheck0 {
codatatype Stream<G> = Cons(head: G, tail: Stream);
method UseStream0(s: Stream)
{
var x := 3;
if (s == s.tail) { // error: this operation is allowed only in ghost contexts
x := x + 2;
}
}
}
module GhostCheck1 {
codatatype Stream<G> = Cons(head: G, tail: Stream);
method UseStream1(s: Stream)
{
var x := 3;
if (s ==#[20] s.tail) { // this seems innocent enough, but it's currently not supported by the compiler, so...
x := x + 7; // error: therefore, this is an error
}
}
}
module GhostCheck2 {
codatatype Stream<G> = Cons(head: G, tail: Stream);
ghost method UseStreamGhost(s: Stream)
{
var x := 3;
if (s == s.tail) { // fine
x := x + 2;
}
}
}
|
