diff options
| author |  leino <unknown> | 2015-09-28 13:16:15 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-09-28 13:16:15 -0700 |
| commit | 0c1ec594e68dab4fcd458a00f9f7a1ac6de2e218 (patch) | |
| tree | cb89d6ef66c96bfa171f954898548f295a3cabc0 /Test/dafny0 | |
| parent | ebaaa36321463925dc9030455e87ae17732b2353 (diff) | |
Changed computation of ghosts until pass 2 of resolution.
Other clean-up in resolution passes, like:
Include everything of type "char" into bounds that are discovered, and likewise for reference types.
Allow more set comprehensions, determining if they are finite based on their argument type.
Changed CalcExpr.SubExpressions to not include computed expressions.
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/AssumptionVariables0.dfy.expect | 4 | ||||
| -rw-r--r-- | Test/dafny0/CallStmtTests.dfy | 34 | ||||
| -rw-r--r-- | Test/dafny0/CallStmtTests.dfy.expect | 4 | ||||
| -rw-r--r-- | Test/dafny0/DiscoverBounds.dfy.expect | 6 | ||||
| -rw-r--r-- | Test/dafny0/NonGhostQuantifiers.dfy | 7 | ||||
| -rw-r--r-- | Test/dafny0/NonGhostQuantifiers.dfy.expect | 22 | ||||
| -rw-r--r-- | Test/dafny0/ParallelResolveErrors.dfy | 13 | ||||
| -rw-r--r-- | Test/dafny0/ParallelResolveErrors.dfy.expect | 36 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 278 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 87 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 50 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy.expect | 14 |
12 files changed, 398 insertions, 157 deletions
diff --git a/Test/dafny0/AssumptionVariables0.dfy.expect b/Test/dafny0/AssumptionVariables0.dfy.expect index 16572961..83eb8a73 100644 --- a/Test/dafny0/AssumptionVariables0.dfy.expect +++ b/Test/dafny0/AssumptionVariables0.dfy.expect @@ -1,13 +1,13 @@ AssumptionVariables0.dfy(6,29): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(7,33): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a2 && <boolean expression>"
-AssumptionVariables0.dfy(9,2): Error: assumption variable must be of type 'bool'
+AssumptionVariables0.dfy(9,26): Error: assumption variable must be of type 'bool'
AssumptionVariables0.dfy(15,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && <boolean expression>"
AssumptionVariables0.dfy(17,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && <boolean expression>"
AssumptionVariables0.dfy(27,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(31,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(53,9): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(61,37): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
-AssumptionVariables0.dfy(61,10): Error: assumption variable must be of type 'bool'
+AssumptionVariables0.dfy(61,34): Error: assumption variable must be of type 'bool'
AssumptionVariables0.dfy(69,15): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(78,20): Error: assumption variable must be ghost
12 resolution/type errors detected in AssumptionVariables0.dfy
diff --git a/Test/dafny0/CallStmtTests.dfy b/Test/dafny0/CallStmtTests.dfy index 67e66b34..46c466ff 100644 --- a/Test/dafny0/CallStmtTests.dfy +++ b/Test/dafny0/CallStmtTests.dfy @@ -1,23 +1,27 @@ // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
-method testing1(t: int)
-{
- t := m(); // error: should be checked at the Dafny level, not fall to Boogie.
-}
+module M0 {
+ method testing1(t: int)
+ {
+ t := m(); // error: should be checked at the Dafny level, not fall to Boogie.
+ }
-method m() returns (r: int)
-{
- return 3;
+ method m() returns (r: int)
+ {
+ return 3;
+ }
}
-method testing2()
-{
- var v;
- v := m2(); // error: v needs to be ghost because r is.
-}
+module M1 {
+ method testing2()
+ {
+ var v;
+ v := m2(); // error: v needs to be ghost because r is.
+ }
-method m2() returns (ghost r: int)
-{
- r := 23;
+ method m2() returns (ghost r: int)
+ {
+ r := 23;
+ }
}
diff --git a/Test/dafny0/CallStmtTests.dfy.expect b/Test/dafny0/CallStmtTests.dfy.expect index 8a334754..246b89f8 100644 --- a/Test/dafny0/CallStmtTests.dfy.expect +++ b/Test/dafny0/CallStmtTests.dfy.expect @@ -1,3 +1,3 @@ -CallStmtTests.dfy(6,3): Error: LHS of assignment must denote a mutable variable
-CallStmtTests.dfy(17,10): Error: actual out-parameter 0 is required to be a ghost variable
+CallStmtTests.dfy(7,4): Error: LHS of assignment must denote a mutable variable
+CallStmtTests.dfy(20,11): Error: actual out-parameter 0 is required to be a ghost variable
2 resolution/type errors detected in CallStmtTests.dfy
diff --git a/Test/dafny0/DiscoverBounds.dfy.expect b/Test/dafny0/DiscoverBounds.dfy.expect index ee816683..34003053 100644 --- a/Test/dafny0/DiscoverBounds.dfy.expect +++ b/Test/dafny0/DiscoverBounds.dfy.expect @@ -1,4 +1,4 @@ -DiscoverBounds.dfy(36,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o''
-DiscoverBounds.dfy(39,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'r'
-DiscoverBounds.dfy(40,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'r''
+DiscoverBounds.dfy(36,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o''
+DiscoverBounds.dfy(39,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'r'
+DiscoverBounds.dfy(40,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'r''
3 resolution/type errors detected in DiscoverBounds.dfy
diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy index bff1d65b..e522d0fc 100644 --- a/Test/dafny0/NonGhostQuantifiers.dfy +++ b/Test/dafny0/NonGhostQuantifiers.dfy @@ -181,6 +181,12 @@ module DependencyOnAllAllocatedObjects { forall c: SomeClass :: true // error: not allowed to dependend on which objects are allocated
}
+ class SomeClass {
+ var f: int;
+ }
+}
+
+module DependencyOnAllAllocatedObjects_More {
method M()
{
var b := forall c: SomeClass :: c != null ==> c.f == 0; // error: non-ghost code requires bounds
@@ -192,3 +198,4 @@ module DependencyOnAllAllocatedObjects { var f: int;
}
}
+
diff --git a/Test/dafny0/NonGhostQuantifiers.dfy.expect b/Test/dafny0/NonGhostQuantifiers.dfy.expect index 1e2fce17..6b737add 100644 --- a/Test/dafny0/NonGhostQuantifiers.dfy.expect +++ b/Test/dafny0/NonGhostQuantifiers.dfy.expect @@ -6,16 +6,16 @@ NonGhostQuantifiers.dfy(167,4): Error: a quantifier involved in a function defin NonGhostQuantifiers.dfy(171,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
NonGhostQuantifiers.dfy(176,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
NonGhostQuantifiers.dfy(181,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
-NonGhostQuantifiers.dfy(186,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'c'
-NonGhostQuantifiers.dfy(16,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
-NonGhostQuantifiers.dfy(45,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
-NonGhostQuantifiers.dfy(49,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd'
-NonGhostQuantifiers.dfy(53,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
-NonGhostQuantifiers.dfy(77,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'
-NonGhostQuantifiers.dfy(81,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(91,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(106,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(114,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'
-NonGhostQuantifiers.dfy(123,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'
+NonGhostQuantifiers.dfy(192,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'c'
+NonGhostQuantifiers.dfy(16,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(45,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(49,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'd'
+NonGhostQuantifiers.dfy(53,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(77,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'i'
+NonGhostQuantifiers.dfy(81,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(91,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(106,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(114,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'y'
+NonGhostQuantifiers.dfy(123,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'x'
NonGhostQuantifiers.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
20 resolution/type errors detected in NonGhostQuantifiers.dfy
diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy index 61956651..8c48487d 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy +++ b/Test/dafny0/ParallelResolveErrors.dfy @@ -7,7 +7,6 @@ class C { 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; { }
@@ -120,3 +119,15 @@ method M3(c: C) c.GhostMethodWithModifies(x); // error: not allowed to call method with nonempty modifies clause
}
}
+
+module AnotherModule {
+ class C {
+ var data: int;
+ ghost var gdata: int;
+ ghost method Init_ModifyThis() modifies this;
+ {
+ data := 6; // error: assignment to a non-ghost field
+ gdata := 7;
+ }
+ }
+}
diff --git a/Test/dafny0/ParallelResolveErrors.dfy.expect b/Test/dafny0/ParallelResolveErrors.dfy.expect index 00030994..4d25ba11 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy.expect +++ b/Test/dafny0/ParallelResolveErrors.dfy.expect @@ -1,23 +1,23 @@ -ParallelResolveErrors.dfy(10,9): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ParallelResolveErrors.dfy(21,4): Error: LHS of assignment must denote a mutable variable
-ParallelResolveErrors.dfy(26,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
+ParallelResolveErrors.dfy(129,11): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ParallelResolveErrors.dfy(20,4): Error: LHS of assignment must denote a mutable variable
+ParallelResolveErrors.dfy(25,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
+ParallelResolveErrors.dfy(42,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
ParallelResolveErrors.dfy(43,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
-ParallelResolveErrors.dfy(44,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
-ParallelResolveErrors.dfy(56,13): Error: new allocation not supported in forall statements
+ParallelResolveErrors.dfy(55,13): Error: new allocation not supported in forall statements
+ParallelResolveErrors.dfy(60,13): Error: new allocation not allowed in ghost context
ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost context
ParallelResolveErrors.dfy(62,13): Error: new allocation not allowed in ghost context
ParallelResolveErrors.dfy(63,13): Error: new allocation not allowed in ghost context
-ParallelResolveErrors.dfy(64,13): Error: new allocation not allowed in ghost context
-ParallelResolveErrors.dfy(65,22): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
-ParallelResolveErrors.dfy(66,20): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods
-ParallelResolveErrors.dfy(73,19): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(77,18): Error: return statement is not allowed inside a forall statement
-ParallelResolveErrors.dfy(84,21): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(85,20): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(86,20): Error: break label is undefined or not in scope: OutsideLoop
-ParallelResolveErrors.dfy(95,24): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(96,24): Error: break label is undefined or not in scope: OutsideLoop
-ParallelResolveErrors.dfy(107,9): Error: the body of the enclosing forall statement is not allowed to update heap locations
-ParallelResolveErrors.dfy(115,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
-ParallelResolveErrors.dfy(120,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
+ParallelResolveErrors.dfy(64,22): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
+ParallelResolveErrors.dfy(65,20): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods
+ParallelResolveErrors.dfy(72,19): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(76,18): Error: return statement is not allowed inside a forall statement
+ParallelResolveErrors.dfy(83,21): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(84,20): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(85,20): Error: break label is undefined or not in scope: OutsideLoop
+ParallelResolveErrors.dfy(94,24): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(95,24): Error: break label is undefined or not in scope: OutsideLoop
+ParallelResolveErrors.dfy(106,9): Error: the body of the enclosing forall statement is not allowed to update heap locations
+ParallelResolveErrors.dfy(114,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
+ParallelResolveErrors.dfy(119,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
22 resolution/type errors detected in ParallelResolveErrors.dfy
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 2fab6bf3..d3514b2b 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -102,7 +102,7 @@ class EE { }
// --------------- ghost tests -------------------------------------
-
+module HereAreMoreGhostTests {
datatype GhostDt =
Nil(ghost extraInfo: int) |
Cons(data: int, tail: GhostDt, ghost moreInfo: int)
@@ -154,7 +154,7 @@ class GhostTests { ensures false;
{
while (true)
- decreases *; // error: not allowed in ghost context
+//KRML-confirmed decreases *; // error: not allowed in ghost context
{
}
}
@@ -228,7 +228,7 @@ class GhostTests { if (p == 67) {
break break; // fine, since this is not a ghost context
} else if (*) {
- break break break; // error: tries to break out of more loop levels than there are
+//KRML-confirmed break break break; // error: tries to break out of more loop levels than there are
}
q := q + 1;
}
@@ -238,7 +238,7 @@ class GhostTests { p := p + 1;
}
}
-method BreakMayNotBeFineHere_Ghost(ghost t: int)
+ method BreakMayNotBeFineHere_Ghost(ghost t: int)
{
var n := 0;
ghost var k := 0;
@@ -297,7 +297,7 @@ method BreakMayNotBeFineHere_Ghost(ghost t: int) }
}
}
-
+} //HereAreMoreGhostTests
method DuplicateLabels(n: int) {
var x;
if (n < 7) {
@@ -364,17 +364,17 @@ method DatatypeDestructors(d: DTD_List) { }
}
method DatatypeDestructors_Ghost(d: DTD_List) {
- var g1 := d.g; // error: cannot use ghost member in non-ghost code
+ var g1 := d.g; // error: cannot use ghost member in non-ghost code//KRML-confirmed
}
// ------------------- print statements ---------------------------------------
-
+module GhostPrintAttempts {
method PrintOnlyNonGhosts(a: int, ghost b: int)
{
print "a: ", a, "\n";
print "b: ", b, "\n"; // error: print statement cannot take ghosts
}
-
+}
// ------------------- auto-added type arguments ------------------------------
class GenericClass<T> { var data: T; }
@@ -439,11 +439,11 @@ method TestCalc_Ghost(m: int, n: int, a: bool, b: bool) {
calc {
n + m;
- { print n + m; } // error: non-ghost statements are not allowed in hints
+ { print n + m; } // error: non-ghost statements are not allowed in hints//KRML-confirmed
m + n;
}
}
-
+module MyOwnModule {
class SideEffectChecks {
ghost var ycalc: int;
@@ -461,11 +461,11 @@ class SideEffectChecks { var x: int;
calc {
0;
- { Mod(0); } // methods with side-effects are not allowed
+ { Mod(0); } // error: methods with side-effects are not allowed
ycalc;
- { ycalc := 1; } // heap updates are not allowed
+ { ycalc := 1; } // error: heap updates are not allowed
1;
- { x := 1; } // updates to locals defined outside of the hint are not allowed
+ { x := 1; } // error: updates to locals defined outside of the hint are not allowed
x;
{
var x: int;
@@ -475,7 +475,7 @@ class SideEffectChecks { }
}
}
-
+}
// ------------------- nameless constructors ------------------------------
class YHWH {
@@ -523,13 +523,13 @@ method AssignSuchThatFromGhost() var x: int;
ghost var g: int;
- x := g; // error: ghost cannot flow into non-ghost
+ x := g; // error: ghost cannot flow into non-ghost//KRML-confirmed
x := *;
assume x == g; // this mix of ghosts and non-ghosts is cool (but, of course,
// the compiler will complain)
- x :| x == g; // error: left-side has non-ghost, so RHS must be non-ghost as well
+ x :| x == g; // error: left-side has non-ghost, so RHS must be non-ghost as well//KRML-confirmed
x :| assume x == g; // this is cool, since it's an assume (but, of course, the
// compiler will complain)
@@ -605,7 +605,7 @@ method LetSuchThat(ghost z: int, n: nat) }
method LetSuchThat_Ghost(ghost z: int, n: nat)
{
- var x := var y :| y < z; y; // error: contraint depend on ghost (z)
+ var x := var y :| y < z; y; // error: contraint depend on ghost (z)//KRML-confirmed
}
// ------------ quantified variables whose types are not inferred ----------
@@ -677,9 +677,9 @@ module GhostAllocationTests { 5;
{ var y := new G; } // error: 'new' not allowed in ghost contexts
2 + 3;
- { if n != 0 { GhostNew4(n-1); } } // error: cannot call non-ghost method in a ghost context
+ { if n != 0 { GhostNew4(n-1); } } // error: cannot call non-ghost method in a ghost context//KRML-confirmed
1 + 4;
- { GhostNew5(g); } // error: cannot call method with nonempty modifies
+ { GhostNew5(g); } // error: cannot call method with nonempty modifies//KRML-confirmed
-5 + 10;
}
}
@@ -735,7 +735,7 @@ module StatementsInExpressions { {
calc {
5;
- { SideEffect(); } // error: cannot call method with side effects
+ { SideEffect(); } // error: cannot call method with side effects//KRML
5;
}
}
@@ -745,7 +745,7 @@ module StatementsInExpressions { calc {
6;
{ assert 6 < 8; }
- { NonGhostMethod(); } // error: cannot call non-ghost method
+ { NonGhostMethod(); } // error: cannot call non-ghost method//KRML-confirmed
{ var x := 8;
while x != 0
decreases *; // error: cannot use 'decreases *' in a ghost context
@@ -759,12 +759,12 @@ module StatementsInExpressions { x := x - 1;
}
}
- { MyField := 12; } // error: cannot assign to a field
- { MyGhostField := 12; } // error: cannot assign to any field
- { SideEffect(); } // error: cannot call (ghost) method with a modifies clause
+ { MyField := 12; } // error: cannot assign to a field//KRML-confirmed
+ { MyGhostField := 12; } // error: cannot assign to any field//KRML-confirmed
+ { SideEffect(); } // error: cannot call (ghost) method with a modifies clause//KRML-confirmed
{ var x := 8;
while x != 0
- modifies this; // error: cannot use a modifies clause on a loop
+ modifies this; // error: cannot use a modifies clause on a loop//KRML-confirmed
{
x := x - 1;
}
@@ -783,7 +783,7 @@ module StatementsInExpressions { calc {
6;
{ assert 6 < 8; }
- { NonGhostMethod(); } // error: cannot call non-ghost method
+ { NonGhostMethod(); } // error: cannot call non-ghost method//KRML-confirmed
{ var x := 8;
while x != 0
decreases *; // error: cannot use 'decreases *' in a ghost context
@@ -791,12 +791,12 @@ module StatementsInExpressions { x := x - 1;
}
}
- { MyField := 12; } // error: cannot assign to a field
- { MyGhostField := 12; } // error: cannot assign to any field
- { M(); } // error: cannot call (ghost) method with a modifies clause
+ { MyField := 12; } // error: cannot assign to a field//KRML-confirmed
+ { MyGhostField := 12; } // error: cannot assign to any field//KRML-confirmed
+ { M(); } // error: cannot call (ghost) method with a modifies clause//KRML-confirmed
{ var x := 8;
while x != 0
- modifies this; // error: cannot use a modifies clause on a loop
+ modifies this; // error: cannot use a modifies clause on a loop//KRML-confirmed
{
x := x - 1;
}
@@ -822,7 +822,7 @@ module StatementsInExpressions { {
MyLemma();
MyGhostMethod(); // error: modifi2es state
- OrdinaryMethod(); // error: not a ghost
+ OrdinaryMethod(); // error: not a ghost//KRML-confirmed
OutParamMethod(); // error: has out-parameters
10
}
@@ -1446,3 +1446,219 @@ module SuchThat { w
}
}
+
+// ---------------------- NEW STUFF ----------------------------------------
+
+module GhostTests {
+ class G { }
+
+ method GhostNew4(n: nat)
+ {
+ var g := new G;
+ calc {
+ 5;
+ 2 + 3;
+ { if n != 0 { GhostNew4(n-1); } } // error: cannot call non-ghost method in a ghost context//ADD:680
+ 1 + 4;
+ { GhostNew5(g); } // error: cannot call method with nonempty modifies//ADD:682
+ -5 + 10;
+ }
+ }
+
+ ghost method GhostNew5(g: G)
+ modifies g;
+ {
+ }
+
+ class MyClass {
+ ghost method SideEffect()
+ modifies this;
+ {
+ }
+
+ method NonGhostMethod()
+ {
+ }
+
+ ghost method M()
+ modifies this;
+ {
+ calc {
+ 5;
+ { SideEffect(); } // error: cannot call method with side effects//ADD:738
+ 5;
+ }
+ }
+ function F(): int
+ {
+ calc {
+ 6;
+ { assert 6 < 8; }
+ { NonGhostMethod(); } // error: cannot call non-ghost method//ADD:748
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ { MyField := 12; } // error: cannot assign to a field, and especially not a non-ghost field//ADD:762
+ { MyGhostField := 12; } // error: cannot assign to any field//ADD:763
+ { SideEffect(); } // error: cannot call (ghost) method with a modifies clause//ADD:764
+ { var x := 8;
+ while x != 0
+ modifies this; // error: cannot use a modifies clause on a loop//ADD:767
+ {
+ x := x - 1;
+ }
+ }
+ 6;
+ }
+ 5
+ }
+ var MyField: int;
+ ghost var MyGhostField: int;
+ method N()
+ {
+ var y :=
+ calc {
+ 6;
+ { assert 6 < 8; }
+ { NonGhostMethod(); } // error: cannot call non-ghost method//ADD:786
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ { MyField := 12; } // error: cannot assign to a field, and especially not a non-ghost field//ADD:794
+ { MyGhostField := 12; } // error: cannot assign to any field//ADD:795
+ { M(); } // error: cannot call (ghost) method with a modifies clause//ADD:796
+ { var x := 8;
+ while x != 0
+ modifies this; // error: cannot use a modifies clause on a loop//ADD:799
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ 6;
+ }
+ 5;
+ }
+ ghost method MyLemma()
+ ghost method MyGhostMethod()
+ modifies this;
+ method OrdinaryMethod()
+ ghost method OutParamMethod() returns (y: int)
+
+ function UseLemma(): int
+ {
+ MyLemma();
+ OrdinaryMethod(); // error: not a ghost//ADD:825
+ 10
+ }
+ }
+}
+
+module EvenMoreGhostTests {
+ ghost method NiceTry()
+ ensures false;
+ {
+ while (true)
+ decreases *; // error: not allowed in ghost context//ADD:157
+ {
+ }
+ }
+ method BreakMayNotBeFineHere()
+ {
+ var n := 0;
+ var p := 0;
+ while (true)
+ {
+ var dontKnow;
+ if (n == 112) {
+ } else if (dontKnow == 708) {
+ while * {
+ label IfNest:
+ if (p == 67) {
+ break break; // fine, since this is not a ghost context
+ } else if (*) {
+ break break break; // error: tries to break out of more loop levels than there are//ADD:231
+ }
+ }
+ }
+ }
+ }
+ ghost method Bad()
+ {
+ var x: int;
+ calc {
+ 1;
+//****** { x := 1; } // error: updates to locals defined outside of the hint are not allowed
+ x;
+ {
+ var x: int;
+ x := 1; // this is OK
+ }
+ 1;
+ }
+ }
+}
+
+module BadGhostTransfer {
+ datatype DTD_List = DTD_Nil | DTD_Cons(Car: int, Cdr: DTD_List, ghost g: int)
+
+ method DatatypeDestructors_Ghost(d: DTD_List) {
+ var g1 := d.g; // error: cannot use ghost member in non-ghost code//ADD:367
+ }
+ method AssignSuchThatFromGhost()
+ {
+ var x: int;
+ ghost var g: int;
+
+ x := g; // error: ghost cannot flow into non-ghost//ADD:526
+
+ x := *;
+ assume x == g; // this mix of ghosts and non-ghosts is cool (but, of course,
+ // the compiler will complain)
+
+ x :| x == g; // error: left-side has non-ghost, so RHS must be non-ghost as well//ADD:532
+
+ x :| assume x == g; // this is cool, since it's an assume (but, of course, the
+ // compiler will complain)
+
+ x :| x == 5;
+ g :| g <= g;
+ g :| assume g < g; // the compiler will complain here, despite the LHS being
+ // ghost -- and rightly so, since an assume is used
+ }
+}
+
+module MoreGhostPrintAttempts {
+ method TestCalc_Ghost(m: int, n: int, a: bool, b: bool)
+ {
+ calc {
+ n + m;
+ { print n + m; } // error: non-ghost statements are not allowed in hints//ADD:442
+ m + n;
+ }
+ }
+}
+
+module MoreLetSuchThatExpr {
+ method LetSuchThat_Ghost(ghost z: int, n: nat)
+ {
+ var x := var y :| y < z; y; // error: contraint depend on ghost (z)//ADD:608
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 0286778b..ee2dd5f7 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -1,3 +1,21 @@ +ResolutionErrors.dfy(113,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(114,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(118,11): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(119,10): Error: actual out-parameter 0 is required to be a ghost variable
+ResolutionErrors.dfy(126,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(130,23): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(137,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(141,21): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(142,35): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(151,10): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(251,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors.dfy(274,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(288,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(293,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
+ResolutionErrors.dfy(375,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(464,11): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(466,14): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(468,10): Error: a hint is not allowed to update a variable declared outside the hint
ResolutionErrors.dfy(558,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
ResolutionErrors.dfy(563,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
ResolutionErrors.dfy(577,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
@@ -13,26 +31,11 @@ ResolutionErrors.dfy(652,11): Error: the body of the enclosing forall statement ResolutionErrors.dfy(652,14): Error: new allocation not allowed in ghost context
ResolutionErrors.dfy(662,23): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(669,15): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(669,15): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(678,17): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(680,29): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(682,17): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(700,21): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(738,20): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(748,24): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(751,22): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(762,18): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(763,23): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(764,20): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(767,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(786,24): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(789,22): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(794,18): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(795,23): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(796,11): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(799,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
ResolutionErrors.dfy(824,19): Error: calls to methods with side-effects are not allowed inside a statement expression
-ResolutionErrors.dfy(825,20): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(826,20): Error: wrong number of method result arguments (got 0, expected 1)
ResolutionErrors.dfy(838,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
ResolutionErrors.dfy(848,4): Error: ghost variables are allowed only in specification contexts
@@ -74,8 +77,8 @@ ResolutionErrors.dfy(1146,6): Error: RHS (of type P<int>) not assignable to LHS ResolutionErrors.dfy(1151,13): Error: arguments must have the same type (got P<int> and P<X>)
ResolutionErrors.dfy(1152,13): Error: arguments must have the same type (got P<bool> and P<X>)
ResolutionErrors.dfy(1153,13): Error: arguments must have the same type (got P<int> and P<bool>)
-ResolutionErrors.dfy(1176,38): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
-ResolutionErrors.dfy(1178,24): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
+ResolutionErrors.dfy(1176,38): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
+ResolutionErrors.dfy(1178,24): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
ResolutionErrors.dfy(1283,26): Error: the type of this variable is underspecified
ResolutionErrors.dfy(1284,31): Error: the type of this variable is underspecified
ResolutionErrors.dfy(1285,29): Error: the type of this variable is underspecified
@@ -106,6 +109,29 @@ ResolutionErrors.dfy(1440,11): Error: type of RHS of assign-such-that statement ResolutionErrors.dfy(1441,9): Error: type of RHS of assign-such-that statement must be boolean (got int)
ResolutionErrors.dfy(1442,13): Error: type of RHS of assign-such-that statement must be boolean (got int)
ResolutionErrors.dfy(1445,15): Error: type of RHS of let-such-that expression must be boolean (got int)
+ResolutionErrors.dfy(1488,20): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1510,18): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1511,23): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1512,20): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1515,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(1497,24): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1510,18): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(1539,18): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1540,23): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1541,11): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1544,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(1532,24): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1539,18): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(1568,20): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1461,29): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1463,17): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1579,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(1597,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(1623,16): Error: ghost fields are allowed only in specification contexts
+ResolutionErrors.dfy(1630,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1636,4): Error: non-ghost variable cannot be assigned a value that depends on a ghost
+ResolutionErrors.dfy(1653,8): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(1662,26): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(488,2): Error: More than one anonymous constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
@@ -113,25 +139,6 @@ ResolutionErrors.dfy(92,14): Error: the name 'David' denotes a datatype construc ResolutionErrors.dfy(93,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(95,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(97,18): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)
-ResolutionErrors.dfy(113,9): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(114,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ResolutionErrors.dfy(118,11): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(119,10): Error: actual out-parameter 0 is required to be a ghost variable
-ResolutionErrors.dfy(126,15): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(130,23): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(137,4): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(141,21): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(142,35): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(151,10): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(157,16): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(231,12): Error: trying to break out of more loop levels than there are enclosing loops
-ResolutionErrors.dfy(251,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
-ResolutionErrors.dfy(274,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(288,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(293,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
-ResolutionErrors.dfy(464,11): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(466,14): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(468,10): Error: a hint is not allowed to update a variable declared outside the hint
ResolutionErrors.dfy(494,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
ResolutionErrors.dfy(499,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
ResolutionErrors.dfy(500,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
@@ -168,8 +175,6 @@ ResolutionErrors.dfy(345,9): Error: a constructor is allowed to be called only w ResolutionErrors.dfy(359,16): Error: arguments must have the same type (got int and DTD_List)
ResolutionErrors.dfy(360,16): Error: arguments must have the same type (got DTD_List and int)
ResolutionErrors.dfy(361,25): Error: arguments must have the same type (got bool and int)
-ResolutionErrors.dfy(367,14): Error: ghost fields are allowed only in specification contexts
-ResolutionErrors.dfy(375,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(400,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
ResolutionErrors.dfy(412,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
ResolutionErrors.dfy(420,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
@@ -180,11 +185,7 @@ ResolutionErrors.dfy(429,10): Error: first argument to ==> must be of type bool ResolutionErrors.dfy(429,10): Error: second argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(434,10): Error: first argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(434,10): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(442,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ResolutionErrors.dfy(526,7): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(532,2): Error: non-ghost variable cannot be assigned a value that depends on a ghost
ResolutionErrors.dfy(603,18): Error: unresolved identifier: w
-ResolutionErrors.dfy(608,24): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(714,11): Error: lemmas are not allowed to have modifies clauses
ResolutionErrors.dfy(976,9): Error: unresolved identifier: s
ResolutionErrors.dfy(987,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
@@ -198,4 +199,4 @@ ResolutionErrors.dfy(1164,8): Error: new cannot be applied to a trait ResolutionErrors.dfy(1185,13): Error: first argument to / must be of numeric type (instead got set<bool>)
ResolutionErrors.dfy(1192,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
ResolutionErrors.dfy(1207,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-200 resolution/type errors detected in ResolutionErrors.dfy
+201 resolution/type errors detected in ResolutionErrors.dfy
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index b44f4d68..a9d473f6 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -39,7 +39,7 @@ datatype ReverseOrder_TheCounterpart<T> = // ---------------------
-class ArrayTests {
+module ArrayTests {
ghost method G(a: array<int>)
requires a != null && 10 <= a.Length;
modifies a;
@@ -167,31 +167,33 @@ module Expl_Module { // --------------------- more ghost tests, for assign-such-that statements
-method M()
-{
- ghost var b: bool;
- ghost var k: int, l: int;
- var m: int;
-
- k :| k < 10;
- k, m :| 0 <= k < m; // error: LHS has non-ghost and RHS has ghost
- m :| m < 10;
-
- // Because of the ghost guard, these 'if' statements are ghost contexts, so only
- // assignments to ghosts are allowed.
- if (b) {
- k :| k < 10; // should be allowed
- k, l :| 0 <= k < l; // ditto
- }
- if (b) {
- m :| m < 10; // error: not allowed in ghost context
- k, m :| 0 <= k < m; // error: not allowed in ghost context
+module MoreGhostTests {
+ method M()
+ {
+ ghost var b: bool;
+ ghost var k: int, l: int;
+ var m: int;
+
+ k :| k < 10;
+ k, m :| 0 <= k < m; // error: LHS has non-ghost and RHS has ghost
+ m :| m < 10;
+
+ // Because of the ghost guard, these 'if' statements are ghost contexts, so only
+ // assignments to ghosts are allowed.
+ if (b) {
+ k :| k < 10; // should be allowed
+ k, l :| 0 <= k < l; // ditto
+ }
+ if (b) {
+ m :| m < 10; // error: not allowed in ghost context
+ k, m :| 0 <= k < m; // error: not allowed in ghost context
+ }
}
-}
-ghost method GhostM() returns (x: int)
-{
- x :| true; // no problem (but there once was a problem with this case, where an error was generated for no reason)
+ ghost method GhostM() returns (x: int)
+ {
+ x :| true; // no problem (but there once was a problem with this case, where an error was generated for no reason)
+ }
}
// ------------------ cycles that could arise from proxy assignments ---------
diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect index 8206fd43..de0bfbed 100644 --- a/Test/dafny0/TypeTests.dfy.expect +++ b/Test/dafny0/TypeTests.dfy.expect @@ -1,6 +1,10 @@ -TypeTests.dfy(205,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
-TypeTests.dfy(211,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
-TypeTests.dfy(218,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)
+TypeTests.dfy(47,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+TypeTests.dfy(178,7): Error: non-ghost variable cannot be assigned a value that depends on a ghost
+TypeTests.dfy(188,6): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(189,9): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(207,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
+TypeTests.dfy(213,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
+TypeTests.dfy(220,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)
TypeTests.dfy(7,17): Error: type mismatch for argument 0 (function expects C, got D)
TypeTests.dfy(7,20): Error: type mismatch for argument 1 (function expects D, got C)
TypeTests.dfy(8,15): Error: type mismatch for argument 0 (function expects C, got int)
@@ -8,7 +12,6 @@ TypeTests.dfy(8,18): Error: type mismatch for argument 1 (function expects D, go TypeTests.dfy(14,16): Error: incorrect type of method in-parameter 0 (expected int, got bool)
TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 0 (expected int, got C)
TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 1 (expected C, got int)
-TypeTests.dfy(47,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
TypeTests.dfy(56,6): Error: Duplicate local-variable name: z
TypeTests.dfy(58,6): Error: Duplicate local-variable name: x
TypeTests.dfy(61,8): Error: Duplicate local-variable name: x
@@ -56,8 +59,5 @@ TypeTests.dfy(151,13): Error: sorry, cannot instantiate type parameter with a su TypeTests.dfy(152,2): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(153,16): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(154,14): Error: sorry, cannot instantiate type parameter with a subrange type
-TypeTests.dfy(177,5): Error: non-ghost variable cannot be assigned a value that depends on a ghost
-TypeTests.dfy(187,4): Error: cannot assign to non-ghost variable in a ghost context
-TypeTests.dfy(188,7): Error: cannot assign to non-ghost variable in a ghost context
TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
62 resolution/type errors detected in TypeTests.dfy
|