Fixed bug #32 dafny.codeplex.com.

1 files changed, 14 insertions, 6 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index cec2f0ec..7f197969 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -476,6 +476,14 @@ ResolutionErrors.dfy(819,6): Error: RHS (of type B) not assignable to LHS (of ty
 ResolutionErrors.dfy(824,6): Error: RHS (of type G) not assignable to LHS (of type object)

 ResolutionErrors.dfy(825,6): Error: RHS (of type Dt) not assignable to LHS (of type object)

 ResolutionErrors.dfy(826,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)

+ResolutionErrors.dfy(888,4): Error: LHS of array assignment must denote an array element (found seq<int>)

+ResolutionErrors.dfy(889,4): Error: LHS of array assignment must denote an array element (found seq<int>)

+ResolutionErrors.dfy(894,10): Error: LHS of assignment must denote a mutable field

+ResolutionErrors.dfy(895,10): Error: LHS of assignment must denote a mutable field

+ResolutionErrors.dfy(896,9): Error: cannot assign to a range of array elements (try the 'forall' statement)

+ResolutionErrors.dfy(897,9): Error: cannot assign to a range of array elements (try the 'forall' statement)

+ResolutionErrors.dfy(898,5): Error: cannot assign to a range of array elements (try the 'forall' statement)

+ResolutionErrors.dfy(899,5): Error: cannot assign to a range of array elements (try the 'forall' statement)

 ResolutionErrors.dfy(427,2): Error: More than one default constructor

 ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts

@@ -555,7 +563,7 @@ ResolutionErrors.dfy(541,20): Error: ghost variables are allowed only in specifi
 ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts

 ResolutionErrors.dfy(544,18): Error: unresolved identifier: w

 ResolutionErrors.dfy(651,11): Error: lemmas are not allowed to have modifies clauses

-126 resolution/type errors detected in ResolutionErrors.dfy

+134 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

@@ -1106,7 +1114,7 @@ Dafny program verifier finished with 27 verified, 6 errors
 

 -------------------- ParallelResolveErrors.dfy --------------------

 ParallelResolveErrors.dfy(7,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(18,6): Error: LHS of assignment must denote a mutable variable or field

+ParallelResolveErrors.dfy(18,4): Error: LHS of assignment must denote a mutable variable

 ParallelResolveErrors.dfy(23,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement

 ParallelResolveErrors.dfy(41,6): 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)

 ParallelResolveErrors.dfy(53,13): Error: new allocation not supported in forall statements

@@ -1930,16 +1938,16 @@ TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive met
 5 resolution/type errors detected in TailCalls.dfy

 

 -------------------- IteratorResolution.dfy --------------------

-IteratorResolution.dfy(59,11): Error: LHS of assignment does not denote a mutable field

+IteratorResolution.dfy(59,9): Error: LHS of assignment must denote a mutable field

 IteratorResolution.dfy(64,18): Error: arguments must have the same type (got _T0 and int)

 IteratorResolution.dfy(76,19): Error: RHS (of type bool) not assignable to LHS (of type int)

 IteratorResolution.dfy(79,13): Error: when allocating an object of type 'GenericIteratorResult', one of its constructor methods must be called

 IteratorResolution.dfy(83,15): Error: logical negation expects a boolean argument (instead got int)

-IteratorResolution.dfy(17,11): Error: LHS of assignment does not denote a mutable field

-IteratorResolution.dfy(19,12): Error: LHS of assignment does not denote a mutable field

+IteratorResolution.dfy(17,9): Error: LHS of assignment must denote a mutable field

+IteratorResolution.dfy(19,9): Error: LHS of assignment must denote a mutable field

 IteratorResolution.dfy(123,9): Error: unresolved identifier: _decreases3

 IteratorResolution.dfy(124,21): Error: arguments must have the same type (got int and ?)

-IteratorResolution.dfy(125,14): Error: LHS of assignment does not denote a mutable field

+IteratorResolution.dfy(125,2): Error: LHS of assignment must denote a mutable field

 IteratorResolution.dfy(132,9): Error: unresolved identifier: _decreases1

 IteratorResolution.dfy(137,9): Error: unresolved identifier: _decreases0

 12 resolution/type errors detected in IteratorResolution.dfy