diff options
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
|