From e10098cde7bac9a7a1576000fa29d15f1fcd8970 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 2 Jul 2015 16:06:02 -0700 Subject: Type parameters in method/function signatures are no longer auto-declared. Although convenient and concise, the auto-declare behavior has on many occasions caused confusion when a type name has accidentally been mistyped (and Dafny had then accepted and auto-declared the name). Note, the behavior of filling in missing type parameters is still supported. This mode, although unusual (even original?) in languages, is different from the auto- declare behavior. For auto-declare, identifiers could be used in the program without having a declaration. For fill-in parameters, the implicitly declared type parameters remain anonymous. --- Test/hofs/ReadsReads.dfy | 52 ++++++++++++++++++++++++------------------------ 1 file changed, 26 insertions(+), 26 deletions(-) (limited to 'Test/hofs/ReadsReads.dfy') diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy index e11473bd..a6f8d922 100644 --- a/Test/hofs/ReadsReads.dfy +++ b/Test/hofs/ReadsReads.dfy @@ -2,58 +2,58 @@ // RUN: %diff "%s.expect" "%t" module ReadsRequiresReads { - function MyReadsOk(f : A -> B, a : A) : set - reads f.reads(a); + function MyReadsOk(f : A -> B, a : A) : set + reads f.reads(a) { f.reads(a) } - function MyReadsOk2(f : A -> B, a : A) : set - reads f.reads(a); + function MyReadsOk2(f : A -> B, a : A) : set + reads f.reads(a) { (f.reads)(a) } - function MyReadsOk3(f : A -> B, a : A) : set - reads (f.reads)(a); + function MyReadsOk3(f : A -> B, a : A) : set + reads (f.reads)(a) { f.reads(a) } - function MyReadsOk4(f : A -> B, a : A) : set - reads (f.reads)(a); + function MyReadsOk4(f : A -> B, a : A) : set + reads (f.reads)(a) { (f.reads)(a) } - function MyReadsBad(f : A -> B, a : A) : set + function MyReadsBad(f : A -> B, a : A) : set { f.reads(a) // error: MyReadsBad does not have permission to read what f.reads(a) reads } - function MyReadsBad2(f : A -> B, a : A) : set + function MyReadsBad2(f : A -> B, a : A) : set { (f.reads)(a) // error: MyReadsBad2 does not have permission to read what f.reads(a) reads } - function MyReadsOk'(f : A -> B, a : A, o : object) : bool - reads f.reads(a); + function MyReadsOk'(f : A -> B, a : A, o : object) : bool + reads f.reads(a) { o in f.reads(a) } - function MyReadsBad'(f : A -> B, a : A, o : object) : bool + function MyReadsBad'(f : A -> B, a : A, o : object) : bool { o in f.reads(a) // error: MyReadsBad' does not have permission to read what f.reads(a) reads } - function MyRequiresOk(f : A -> B, a : A) : bool - reads f.reads(a); + function MyRequiresOk(f : A -> B, a : A) : bool + reads f.reads(a) { f.requires(a) } - function MyRequiresBad(f : A -> B, a : A) : bool + function MyRequiresBad(f : A -> B, a : A) : bool { f.requires(a) // error: MyRequiresBad does not have permission to read what f.requires(a) reads } @@ -72,11 +72,11 @@ module WhatWeKnowAboutReads { } class S { - var s : S; + var s : S } function ReadsSomething(s : S):() - reads s; + reads s {()} method MaybeSomething() { @@ -105,29 +105,29 @@ module WhatWeKnowAboutReads { module ReadsAll { function A(f: int -> int) : int - reads set o,x | o in f.reads(x) :: o; - requires forall x :: f.requires(x); + reads set o,x | o in f.reads(x) :: o + requires forall x :: f.requires(x) { f(0) + f(1) + f(2) } function method B(f: int -> int) : int - reads set o,x | o in f.reads(x) :: o; - requires forall x :: f.requires(x); + reads set o,x | o in f.reads(x) :: o + requires forall x :: f.requires(x) { f(0) + f(1) + f(2) } function C(f: int -> int) : int - reads f.reads; - requires forall x :: f.requires(x); + reads f.reads + requires forall x :: f.requires(x) { f(0) + f(1) + f(2) } function method D(f: int -> int) : int - reads f.reads; - requires forall x :: f.requires(x); + reads f.reads + requires forall x :: f.requires(x) { f(0) + f(1) + f(2) } -- cgit v1.2.3 From 8a869bcfaeceb6b5a1d01e9b1c0c08b7000a094e Mon Sep 17 00:00:00 2001 From: leino Date: Mon, 28 Sep 2015 22:47:35 -0700 Subject: Removed specContextOnly parameter from ResolveStatement. Moved all bounds discovery to resolution pass 1. --- Source/Dafny/Resolver.cs | 277 ++++++++++++++------------------ Test/dafny0/ResolutionErrors.dfy | 26 +-- Test/dafny0/ResolutionErrors.dfy.expect | 27 +++- Test/dafny4/Regression0.dfy | 6 +- Test/dafny4/Regression0.dfy.expect | 3 +- Test/dafny4/set-compr.dfy | 54 +++++-- Test/dafny4/set-compr.dfy.expect | 15 +- Test/hofs/ReadsReads.dfy | 4 +- 8 files changed, 218 insertions(+), 194 deletions(-) (limited to 'Test/hofs/ReadsReads.dfy') diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 9f2feb14..1c376c49 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1336,11 +1336,6 @@ namespace Microsoft.Dafny // ---------------------------------- Pass 0 ---------------------------------- // This pass resolves names, introduces (and may solve) type constraints, and // builds the module's call graph. - // Some bounds are discovered during this pass [is this necessary? can they be - // moved to pass 1 like the other bounds discovery? --KRML], namely: - // - forall statements - // - quantifier expressions - // - map comprehensions // For 'newtype' declarations, it also checks that all types were fully // determined. // ---------------------------------------------------------------------------- @@ -1375,7 +1370,7 @@ namespace Microsoft.Dafny if (!CheckTypeInference_Visitor.IsDetermined(dd.BaseType.NormalizeExpand())) { reporter.Error(MessageSource.Resolver, dd.tok, "newtype's base type is not fully determined; add an explicit type for '{0}'", dd.Var.Name); } - CheckTypeInference(dd.Constraint); + CheckTypeInference(dd.Constraint, dd); scope.PopMarker(); } } @@ -1408,7 +1403,10 @@ namespace Microsoft.Dafny // * checks that type inference was able to determine all types // * fills in the .ResolvedOp field of binary expressions // * discovers bounds for: + // - forall statements // - set comprehensions + // - map comprehensions + // - quantifier expressions // - assign-such-that statements // - compilable let-such-that expressions // - newtype constraints @@ -1432,7 +1430,7 @@ namespace Microsoft.Dafny iter.SubExpressions.Iter(e => CheckExpression(e, this, iter)); } if (iter.Body != null) { - CheckTypeInference(iter.Body); + CheckTypeInference(iter.Body, iter); if (prevErrCnt == reporter.Count(ErrorLevel.Error)) { ComputeGhostInterest(iter.Body, false, iter); CheckExpression(iter.Body, this, iter); @@ -2047,22 +2045,22 @@ namespace Microsoft.Dafny private void CheckTypeInference_Member(MemberDecl member) { if (member is Method) { var m = (Method)member; - m.Req.Iter(CheckTypeInference_MaybeFreeExpression); - m.Ens.Iter(CheckTypeInference_MaybeFreeExpression); - CheckTypeInference_Specification_FrameExpr(m.Mod); - CheckTypeInference_Specification_Expr(m.Decreases); + m.Req.Iter(mfe => CheckTypeInference_MaybeFreeExpression(mfe, m)); + m.Ens.Iter(mfe => CheckTypeInference_MaybeFreeExpression(mfe, m)); + CheckTypeInference_Specification_FrameExpr(m.Mod, m); + CheckTypeInference_Specification_Expr(m.Decreases, m); if (m.Body != null) { - CheckTypeInference(m.Body); + CheckTypeInference(m.Body, m); } } else if (member is Function) { var f = (Function)member; var errorCount = reporter.Count(ErrorLevel.Error); - f.Req.Iter(CheckTypeInference); - f.Ens.Iter(CheckTypeInference); - f.Reads.Iter(fe => CheckTypeInference(fe.E)); - CheckTypeInference_Specification_Expr(f.Decreases); + f.Req.Iter(e => CheckTypeInference(e, f)); + f.Ens.Iter(e => CheckTypeInference(e, f)); + f.Reads.Iter(fe => CheckTypeInference(fe.E, f)); + CheckTypeInference_Specification_Expr(f.Decreases, f); if (f.Body != null) { - CheckTypeInference(f.Body); + CheckTypeInference(f.Body, f); } if (errorCount == reporter.Count(ErrorLevel.Error) && f is FixpointPredicate) { var cop = (FixpointPredicate)f; @@ -2071,43 +2069,51 @@ namespace Microsoft.Dafny } } - private void CheckTypeInference_MaybeFreeExpression(MaybeFreeExpression mfe) { + private void CheckTypeInference_MaybeFreeExpression(MaybeFreeExpression mfe, ICodeContext codeContext) { Contract.Requires(mfe != null); + Contract.Requires(codeContext != null); foreach (var e in Attributes.SubExpressions(mfe.Attributes)) { - CheckTypeInference(e); + CheckTypeInference(e, codeContext); } - CheckTypeInference(mfe.E); + CheckTypeInference(mfe.E, codeContext); } - private void CheckTypeInference_Specification_Expr(Specification spec) { + private void CheckTypeInference_Specification_Expr(Specification spec, ICodeContext codeContext) { Contract.Requires(spec != null); + Contract.Requires(codeContext != null); foreach (var e in Attributes.SubExpressions(spec.Attributes)) { - CheckTypeInference(e); + CheckTypeInference(e, codeContext); } - spec.Expressions.Iter(CheckTypeInference); + spec.Expressions.Iter(e => CheckTypeInference(e, codeContext)); } - private void CheckTypeInference_Specification_FrameExpr(Specification spec) { + private void CheckTypeInference_Specification_FrameExpr(Specification spec, ICodeContext codeContext) { Contract.Requires(spec != null); + Contract.Requires(codeContext != null); foreach (var e in Attributes.SubExpressions(spec.Attributes)) { - CheckTypeInference(e); + CheckTypeInference(e, codeContext); } - spec.Expressions.Iter(fe => CheckTypeInference(fe.E)); + spec.Expressions.Iter(fe => CheckTypeInference(fe.E, codeContext)); } - void CheckTypeInference(Expression expr) { + void CheckTypeInference(Expression expr, ICodeContext codeContext) { Contract.Requires(expr != null); + Contract.Requires(codeContext != null); PartiallySolveTypeConstraints(); - var c = new CheckTypeInference_Visitor(this); + var c = new CheckTypeInference_Visitor(this, codeContext); c.Visit(expr); } - void CheckTypeInference(Statement stmt) { + void CheckTypeInference(Statement stmt, ICodeContext codeContext) { Contract.Requires(stmt != null); - var c = new CheckTypeInference_Visitor(this); + Contract.Requires(codeContext != null); + var c = new CheckTypeInference_Visitor(this, codeContext); c.Visit(stmt); } class CheckTypeInference_Visitor : ResolverBottomUpVisitor { - public CheckTypeInference_Visitor(Resolver resolver) + readonly ICodeContext codeContext; + public CheckTypeInference_Visitor(Resolver resolver, ICodeContext codeContext) : base(resolver) { Contract.Requires(resolver != null); + Contract.Requires(codeContext != null); + this.codeContext = codeContext; } protected override void VisitOneStmt(Statement stmt) { if (stmt is VarDeclStmt) { @@ -2118,6 +2124,9 @@ namespace Microsoft.Dafny } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable")); + List missingBounds; + s.Bounds = DiscoverBestBounds_MultipleVars(s.BoundVars, s.Range, true, true, out missingBounds); + } else if (stmt is AssignSuchThatStmt) { var s = (AssignSuchThatStmt)stmt; if (s.AssumeToken == null) { @@ -2154,27 +2163,55 @@ namespace Microsoft.Dafny resolver.reporter.Error(MessageSource.Resolver, bv.tok, "type of bound variable '{0}' could not be determined; please specify the type explicitly", bv.Name); } } - if (e is SetComprehension) { - var sc = (SetComprehension)e; - if (sc.Finite) { - // A set must be finite. Discover bounds for the Range expression, but report an error only if the Term is not - // of a finite-individuals type. - List missingBounds; - sc.Bounds = DiscoverBestBounds_MultipleVars(sc.BoundVars, sc.Range, true, true, out missingBounds); - if (missingBounds.Count != 0) { - sc.MissingBounds = missingBounds; - if (sc.Type.HasFinitePossibleValues) { - // This means the set is finite, regardless of if the Range is bounded. So, we don't give any error here. - // However, if this expression is used in a non-ghost context (which is not yet known at this stage of - // resolution), the resolver will generate an error about that later. - } else { - foreach (var bv in sc.MissingBounds) { - resolver.reporter.Error(MessageSource.Resolver, sc, "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 '{0}'", bv.Name); - } + // apply bounds discovery to quantifiers, finite sets, and finite maps + string what = null; + Expression whereToLookForBounds = null; + bool polarity = true; + if (e is QuantifierExpr) { + what = "quantifier"; + whereToLookForBounds = ((QuantifierExpr)e).LogicalBody(); + polarity = e is ExistsExpr; + } else if (e is SetComprehension && ((SetComprehension)e).Finite) { + what = "set comprehension"; + whereToLookForBounds = e.Range; + } else if (e is MapComprehension && ((MapComprehension)e).Finite) { + what = "map comprehension"; + whereToLookForBounds = e.Range; + } + if (whereToLookForBounds != null) { + List missingBounds; + e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, whereToLookForBounds, polarity, true, out missingBounds); + if (missingBounds.Count != 0) { + e.MissingBounds = missingBounds; + + if ((e is SetComprehension && !((SetComprehension)e).Finite) || (e is MapComprehension && !((MapComprehension)e).Finite)) { + // a possibly infinite set/map has no restrictions on its range + } else if (e is QuantifierExpr) { + // don't report any errors at this time (instead, wait to see if the quantifier is used in a non-ghost context) + } else if (e is SetComprehension && e.Type.HasFinitePossibleValues) { + // This means the set is finite, regardless of if the Range is bounded. So, we don't give any error here. + // However, if this expression is used in a non-ghost context (which is not yet known at this stage of + // resolution), the resolver will generate an error about that later. + } else { + // we cannot be sure that the set/map really is finite + foreach (var bv in missingBounds) { + resolver.reporter.Error(MessageSource.Resolver, e, "a {0} must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{1}'", what, bv.Name); + } + } + } + if (codeContext is Function && e.Bounds != null) { + // functions are not allowed to depend on the set of allocated objects + Contract.Assert(e.Bounds.Count == e.BoundVars.Count); + for (int i = 0; i < e.Bounds.Count; i++) { + var bound = e.Bounds[i] as ComprehensionExpr.RefBoundedPool; + if (bound != null) { + var bv = e.BoundVars[i]; + resolver.reporter.Error(MessageSource.Resolver, expr, "a {0} 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 '{1}'", what, bv.Name); } } } } + } else if (expr is MemberSelectExpr) { var e = (MemberSelectExpr)expr; if (e.Member is Function || e.Member is Method) { @@ -4035,7 +4072,7 @@ namespace Microsoft.Dafny int prevErrors = reporter.Count(ErrorLevel.Error); ResolveExpression(arg, opts); if (prevErrors == reporter.Count(ErrorLevel.Error)) { - CheckTypeInference(arg); + CheckTypeInference(arg, opts.codeContext); } } } @@ -4289,7 +4326,7 @@ namespace Microsoft.Dafny scope.Push(k.Name, k); // we expect no name conflict for _k } var prevErrorCount = reporter.Count(ErrorLevel.Error); - ResolveBlockStatement(m.Body, m.IsGhost, m); + ResolveBlockStatement(m.Body, m); SolveAllTypeConstraints(); if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { //KRML ComputeGhostInterest(m.Body, m); @@ -4411,7 +4448,7 @@ namespace Microsoft.Dafny // Resolve body if (iter.Body != null) { - ResolveBlockStatement(iter.Body, false, iter); + ResolveBlockStatement(iter.Body, iter); if (reporter.Count(ErrorLevel.Error) == postSpecErrorCount) { //KRML ComputeGhostInterest(iter.Body, iter); } @@ -5249,11 +5286,7 @@ namespace Microsoft.Dafny return at; } - /// - /// "specContextOnly" means that the statement must be erasable, that is, it should be okay to omit it - /// at run time. That means it must not have any side effects on non-ghost variables, for example. - /// - public void ResolveStatement(Statement stmt, bool specContextOnly, ICodeContext codeContext) { + public void ResolveStatement(Statement stmt, ICodeContext codeContext) { Contract.Requires(stmt != null); Contract.Requires(codeContext != null); if (!(stmt is ForallStmt)) { // forall statements do their own attribute resolution below @@ -5328,13 +5361,13 @@ namespace Microsoft.Dafny } s.hiddenUpdate = new UpdateStmt(s.Tok, s.EndTok, formals, s.rhss, true); // resolving the update statement will check for return/yield statement specifics. - ResolveStatement(s.hiddenUpdate, specContextOnly, codeContext); + ResolveStatement(s.hiddenUpdate, codeContext); } } else {// this is a regular return/yield statement. s.hiddenUpdate = null; } } else if (stmt is ConcreteUpdateStatement) { - ResolveConcreteUpdateStmt((ConcreteUpdateStatement)stmt, specContextOnly, codeContext); + ResolveConcreteUpdateStmt((ConcreteUpdateStatement)stmt, codeContext); } else if (stmt is VarDeclStmt) { var s = (VarDeclStmt)stmt; // We have three cases. @@ -5370,7 +5403,7 @@ namespace Microsoft.Dafny lhs.Type = local.Type; } // resolve the whole thing - ResolveConcreteUpdateStmt(s.Update, specContextOnly, codeContext); + ResolveConcreteUpdateStmt(s.Update, codeContext); } // Add the locals to the scope foreach (var local in s.Locals) { @@ -5382,7 +5415,7 @@ namespace Microsoft.Dafny } // Resolve the AssignSuchThatStmt, if any if (s.Update is AssignSuchThatStmt) { - ResolveConcreteUpdateStmt(s.Update, specContextOnly, codeContext); + ResolveConcreteUpdateStmt(s.Update, codeContext); } // Update the VarDeclStmt's ghost status according to its components foreach (var local in s.Locals) @@ -5481,52 +5514,40 @@ namespace Microsoft.Dafny } else if (stmt is BlockStmt) { var s = (BlockStmt)stmt; scope.PushMarker(); - ResolveBlockStatement(s, specContextOnly, codeContext); + ResolveBlockStatement(s, codeContext); scope.PopMarker(); } else if (stmt is IfStmt) { IfStmt s = (IfStmt)stmt; - bool branchesAreSpecOnly = specContextOnly; if (s.Guard != null) { - int prevErrorCount = reporter.Count(ErrorLevel.Error); ResolveExpression(s.Guard, new ResolveOpts(codeContext, true)); Contract.Assert(s.Guard.Type != null); // follows from postcondition of ResolveExpression - bool successfullyResolved = reporter.Count(ErrorLevel.Error) == prevErrorCount; ConstrainTypes(s.Guard.Type, Type.Bool, s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type); - if (!specContextOnly && successfullyResolved) { - branchesAreSpecOnly = UsesSpecFeatures(s.Guard); - } } - ResolveStatement(s.Thn, branchesAreSpecOnly, codeContext); + ResolveStatement(s.Thn, codeContext); if (s.Els != null) { - ResolveStatement(s.Els, branchesAreSpecOnly, codeContext); + ResolveStatement(s.Els, codeContext); } } else if (stmt is AlternativeStmt) { var s = (AlternativeStmt)stmt; - ResolveAlternatives(s.Alternatives, specContextOnly, null, codeContext); + ResolveAlternatives(s.Alternatives, null, codeContext); } else if (stmt is WhileStmt) { WhileStmt s = (WhileStmt)stmt; - bool bodyMustBeSpecOnly = specContextOnly; var fvs = new HashSet(); if (s.Guard != null) { - int prevErrorCount = reporter.Count(ErrorLevel.Error); ResolveExpression(s.Guard, new ResolveOpts(codeContext, true)); Contract.Assert(s.Guard.Type != null); // follows from postcondition of ResolveExpression - bool successfullyResolved = reporter.Count(ErrorLevel.Error) == prevErrorCount; Translator.ComputeFreeVariables(s.Guard, fvs); ConstrainTypes(s.Guard.Type, Type.Bool, s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type); - if (!specContextOnly && successfullyResolved) { - bodyMustBeSpecOnly = UsesSpecFeatures(s.Guard); - } } ResolveLoopSpecificationComponents(s.Invariants, s.Decreases, s.Mod, codeContext, fvs); if (s.Body != null) { loopStack.Add(s); // push - ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext); + ResolveStatement(s.Body, codeContext); loopStack.RemoveAt(loopStack.Count - 1); // pop } else { string text = "havoc {" + Util.Comma(", ", fvs, fv => fv.Name) + "};"; // always terminate with a semi-colon @@ -5535,7 +5556,7 @@ namespace Microsoft.Dafny } else if (stmt is AlternativeLoopStmt) { var s = (AlternativeLoopStmt)stmt; - ResolveAlternatives(s.Alternatives, specContextOnly, s, codeContext); + ResolveAlternatives(s.Alternatives, s, codeContext); ResolveLoopSpecificationComponents(s.Invariants, s.Decreases, s.Mod, codeContext, null); } else if (stmt is ForallStmt) { @@ -5559,23 +5580,13 @@ namespace Microsoft.Dafny // first (above) and only then resolve the attributes (below). ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, true)); - bool bodyMustBeSpecOnly = specContextOnly || (prevErrorCount == reporter.Count(ErrorLevel.Error) && UsesSpecFeatures(s.Range)); - if (!bodyMustBeSpecOnly && prevErrorCount == reporter.Count(ErrorLevel.Error)) { - CheckTypeInference(s.Range); // we need to resolve operators before the call to DiscoverBounds - List missingBounds; - s.Bounds = DiscoverBestBounds_MultipleVars(s.BoundVars, s.Range, true, true, out missingBounds); - if (missingBounds.Count != 0) { - bodyMustBeSpecOnly = true; - } - } - if (s.Body != null) { // clear the labels for the duration of checking the body, because break statements are not allowed to leave a forall statement var prevLblStmts = labeledStatements; var prevLoopStack = loopStack; labeledStatements = new Scope(); loopStack = new List(); - ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext); + ResolveStatement(s.Body, codeContext); labeledStatements = prevLblStmts; loopStack = prevLoopStack; } @@ -5627,7 +5638,7 @@ namespace Microsoft.Dafny ResolveFrameExpression(fe, false, codeContext); } if (s.Body != null) { - ResolveBlockStatement(s.Body, specContextOnly, codeContext); + ResolveBlockStatement(s.Body, codeContext); } } else if (stmt is CalcStmt) { @@ -5658,7 +5669,7 @@ namespace Microsoft.Dafny labeledStatements = new Scope(); loopStack = new List(); foreach (var h in s.Hints) { - ResolveStatement(h, true, codeContext); + ResolveStatement(h, codeContext); } labeledStatements = prevLblStmts; loopStack = prevLoopStack; @@ -5675,13 +5686,13 @@ namespace Microsoft.Dafny Contract.Assert(prevErrorCount != reporter.Count(ErrorLevel.Error) || s.Steps.Count == s.Hints.Count); } else if (stmt is MatchStmt) { - ResolveMatchStmt(stmt, specContextOnly, codeContext); + ResolveMatchStmt(stmt, codeContext); } else if (stmt is SkeletonStatement) { var s = (SkeletonStatement)stmt; reporter.Error(MessageSource.Resolver, s.Tok, "skeleton statements are allowed only in refining methods"); // nevertheless, resolve the underlying statement; hey, why not if (s.S != null) { - ResolveStatement(s.S, specContextOnly, codeContext); + ResolveStatement(s.S, codeContext); } } else { Contract.Assert(false); throw new cce.UnreachableException(); @@ -5726,18 +5737,12 @@ namespace Microsoft.Dafny } } - void ResolveMatchStmt(Statement stmt, bool specContextOnly, ICodeContext codeContext) { + void ResolveMatchStmt(Statement stmt, ICodeContext codeContext) { MatchStmt s = (MatchStmt)stmt; DesugarMatchStmtWithTupleExpression(s); - bool bodyIsSpecOnly = specContextOnly; - int prevErrorCount = reporter.Count(ErrorLevel.Error); ResolveExpression(s.Source, new ResolveOpts(codeContext, true)); Contract.Assert(s.Source.Type != null); // follows from postcondition of ResolveExpression - bool successfullyResolved = reporter.Count(ErrorLevel.Error) == prevErrorCount; - if (!specContextOnly && successfullyResolved) { - bodyIsSpecOnly = UsesSpecFeatures(s.Source); - } UserDefinedType sourceType = null; DatatypeDecl dtd = null; if (s.Source.Type.IsDatatype) { @@ -5814,7 +5819,7 @@ namespace Microsoft.Dafny } } foreach (Statement ss in mc.Body) { - ResolveStatement(ss, bodyIsSpecOnly, codeContext); + ResolveStatement(ss, codeContext); } // substitute body to replace the case pat with v. This needs to happen // after the body is resolved so we can scope the bv correctly. @@ -5824,7 +5829,7 @@ namespace Microsoft.Dafny foreach (Statement ss in mc.Body) { Statement clone = cloner.CloneStmt(ss); // resolve it again since we just cloned it. - ResolveStatement(clone, bodyIsSpecOnly, codeContext); + ResolveStatement(clone, codeContext); list.Add(clone); } mc.UpdateBody(list); @@ -6242,7 +6247,7 @@ namespace Microsoft.Dafny reporter.Info(MessageSource.Resolver, loopStmt.Tok, s); } } - private void ResolveConcreteUpdateStmt(ConcreteUpdateStatement s, bool specContextOnly, ICodeContext codeContext) { + private void ResolveConcreteUpdateStmt(ConcreteUpdateStatement s, ICodeContext codeContext) { Contract.Requires(codeContext != null); // First, resolve all LHS's and expression-looking RHS's. @@ -6265,7 +6270,7 @@ namespace Microsoft.Dafny var suchThat = (AssignSuchThatStmt)s; // this is the other possible subclass ResolveAssignSuchThatStmt(suchThat, codeContext); } else { - ResolveUpdateStmt(update, specContextOnly, codeContext, errorCountBeforeCheckingLhs); + ResolveUpdateStmt(update, codeContext, errorCountBeforeCheckingLhs); } ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, true)); } @@ -6274,7 +6279,7 @@ namespace Microsoft.Dafny /// errorCountBeforeCheckingLhs is passed in so that this method can determined if any resolution errors were found during /// LHS or RHS checking, because only if no errors were found is update.ResolvedStmt changed. /// - private void ResolveUpdateStmt(UpdateStmt update, bool specContextOnly, ICodeContext codeContext, int errorCountBeforeCheckingLhs) { + private void ResolveUpdateStmt(UpdateStmt update, ICodeContext codeContext, int errorCountBeforeCheckingLhs) { Contract.Requires(update != null); Contract.Requires(codeContext != null); IToken firstEffectfulRhs = null; @@ -6367,7 +6372,7 @@ namespace Microsoft.Dafny } foreach (var a in update.ResolvedStatements) { - ResolveStatement(a, specContextOnly, codeContext); + ResolveStatement(a, codeContext); } } @@ -6393,7 +6398,7 @@ namespace Microsoft.Dafny ConstrainTypes(s.Expr.Type, Type.Bool, s.Expr, "type of RHS of assign-such-that statement must be boolean (got {0})", s.Expr.Type); } - void ResolveAlternatives(List alternatives, bool specContextOnly, AlternativeLoopStmt loopToCatchBreaks, ICodeContext codeContext) { + void ResolveAlternatives(List alternatives, AlternativeLoopStmt loopToCatchBreaks, ICodeContext codeContext) { Contract.Requires(alternatives != null); Contract.Requires(codeContext != null); @@ -6412,7 +6417,7 @@ namespace Microsoft.Dafny foreach (var alternative in alternatives) { scope.PushMarker(); foreach (Statement ss in alternative.Body) { - ResolveStatement(ss, specContextOnly, codeContext); + ResolveStatement(ss, codeContext); } scope.PopMarker(); } @@ -6541,7 +6546,7 @@ namespace Microsoft.Dafny } } - void ResolveBlockStatement(BlockStmt blockStmt, bool specContextOnly, ICodeContext codeContext) { + void ResolveBlockStatement(BlockStmt blockStmt, ICodeContext codeContext) { Contract.Requires(blockStmt != null); Contract.Requires(codeContext != null); @@ -6561,7 +6566,7 @@ namespace Microsoft.Dafny Contract.Assert(r == Scope.PushResult.Success); // since we just checked for duplicates, we expect the Push to succeed } } - ResolveStatement(ss, specContextOnly, codeContext); + ResolveStatement(ss, codeContext); labeledStatements.PopMarker(); } } @@ -7878,25 +7883,6 @@ namespace Microsoft.Dafny allTypeParameters.PopMarker(); expr.Type = Type.Bool; - if (prevErrorCount == reporter.Count(ErrorLevel.Error)) { - CheckTypeInference(e.LogicalBody()); // we need to resolve operators before the call to DiscoverBounds - List missingBounds; - e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.LogicalBody(), e is ExistsExpr, true, out missingBounds); - if (missingBounds.Count != 0) { - e.MissingBounds = missingBounds; - } - if (opts.codeContext is Function && e.Bounds != null) { - Contract.Assert(e.Bounds.Count == e.BoundVars.Count); - for (int i = 0; i < e.Bounds.Count; i++) { - var bound = e.Bounds[i] as ComprehensionExpr.RefBoundedPool; - if (bound != null) { - var bv = e.BoundVars[i]; - reporter.Error(MessageSource.Resolver, expr, "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 '{0}'", bv.Name); - } - } - } - } - } else if (expr is SetComprehension) { var e = (SetComprehension)expr; int prevErrorCount = reporter.Count(ErrorLevel.Error); @@ -7936,19 +7922,6 @@ namespace Microsoft.Dafny scope.PopMarker(); expr.Type = new MapType(e.Finite, e.BoundVars[0].Type, e.Term.Type); - if (prevErrorCount == reporter.Count(ErrorLevel.Error)) { - CheckTypeInference(e.Range); // we need to resolve operators before the call to DiscoverBounds - List missingBounds; - e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.Range, true, true, out missingBounds); - if (missingBounds.Count != 0) { - e.MissingBounds = missingBounds; - if (e.Finite) { - foreach (var bv in e.MissingBounds) { - reporter.Error(MessageSource.Resolver, expr, "a map comprehension must produce a finite domain, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name); - } - } - } - } } else if (expr is LambdaExpr) { var e = (LambdaExpr)expr; int prevErrorCount = reporter.Count(ErrorLevel.Error); @@ -7977,7 +7950,7 @@ namespace Microsoft.Dafny } else if (expr is StmtExpr) { var e = (StmtExpr)expr; int prevErrorCount = reporter.Count(ErrorLevel.Error); - ResolveStatement(e.S, true, opts.codeContext); + ResolveStatement(e.S, opts.codeContext); if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { var r = e.S as UpdateStmt; if (r != null && r.ResolvedStatements.Count == 1) { @@ -10335,21 +10308,19 @@ namespace Microsoft.Dafny } } else if (expr is NamedExpr) { return moduleInfo.IsAbstract ? false : UsesSpecFeatures(((NamedExpr)expr).Body); - } else if (expr is ComprehensionExpr) { - var q = expr as QuantifierExpr; - Contract.Assert(q == null || q.SplitQuantifier == null); // No split quantifiers during resolution - if (q != null && q.Bounds.Contains(null)) { - return true; // the quantifier cannot be compiled if the resolver found no bounds - } - return Contract.Exists(expr.SubExpressions, se => UsesSpecFeatures(se)); + } else if (expr is QuantifierExpr) { + var e = (QuantifierExpr)expr; + Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution + return e.UncompilableBoundVars().Count != 0; } else if (expr is SetComprehension) { var e = (SetComprehension)expr; - return (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term)); + return !e.Finite || e.UncompilableBoundVars().Count != 0 || (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term)); } else if (expr is MapComprehension) { var e = (MapComprehension)expr; - return (UsesSpecFeatures(e.Range)) || (UsesSpecFeatures(e.Term)); + return !e.Finite || e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.Range) || UsesSpecFeatures(e.Term); } else if (expr is LambdaExpr) { - return Contract.Exists(expr.SubExpressions, UsesSpecFeatures); + var e = (LambdaExpr)expr; + return UsesSpecFeatures(e.Term); } else if (expr is WildcardExpr) { return false; } else if (expr is StmtExpr) { diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 49e6efa0..e935c83d 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -586,16 +586,16 @@ method LetSuchThat(ghost z: int, n: nat) module NonInferredType { predicate P(x: T) - method NonInferredType0(x: int) + method InferredType(x: int) { var t; - assume forall z :: P(z) && z == t; // It would be nice to allow the following example, but the implementation calls DiscoverBounds before CheckInference for quantifiers. + assume forall z :: P(z) && z == t; assume t == x; // this statement determines the type of t and z } - method NonInferredType1(x: int) + method NonInferredType(x: int) { - var t; + var t; // error: the type of t is not determined assume forall z :: P(z) && z == t; // error: the type of z is not determined } } @@ -1126,15 +1126,15 @@ method TraitSynonym() // ----- set comprehensions where the term type is finite ----- module ObjectSetComprehensions { - // allowed in non-ghost context: - function A() : set { set o : object | true :: o } + // the following set comprehensions are known to be finite + function A() : set { set o : object | true :: o } // error: a function is not allowed to depend on the allocated state - lemma B() { var x := set o : object | true :: o; } + function method B() : set { set o : object | true :: o } // error: a function is not allowed to depend on the allocated state - // not allowed in non-ghost context: - function method C() : set { set o : object | true :: o } + // outside functions, the comprehension is permitted, but it cannot be compiled + lemma C() { var x := set o : object | true :: o; } - method D() { var x := set o : object | true :: o; } + method D() { var x := set o : object | true :: o; } // error: not (easily) compilable } // ------ regression test for type checking of integer division ----- @@ -1228,9 +1228,9 @@ module NonInferredTypeVariables { method BadClient(n: nat) { var p := P(n); // error: cannot infer the type argument for P - ghost var q := Q(n); // error: cannot infer the type argument for Q + ghost var q := Q(n); // error: cannot infer the type argument for Q (and thus q's type cannot be determined either) M(n); // error: cannot infer the type argument for M - var x := N(n); // error: cannot infer the type argument for N + var x := N(n); // error: cannot infer the type argument for N (and thus x's type cannot be determined either) var a := new array; // error: cannot infer the type argument for 'array' var c := new C; // error: cannot infer the type argument for 'C' var s: set; // type argument for 'set' @@ -1248,7 +1248,7 @@ module NonInferredTypeVariables { ghost var d0 := forall s :: s == {7} ==> s != {}; var d1 := forall s: set :: s in S ==> s == {}; var ggcc0: C; - var ggcc1: C; + var ggcc1: C; // error: full type cannot be determined ghost var d2 := forall c: C :: c != null ==> c.f == 10; ghost var d2' := forall c :: c == ggcc0 && c != null ==> c.f == 10; ghost var d2'' := forall c :: c == ggcc1 && c != null ==> c.f == c.f; // error: here, type of c is not determined diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index edf61b33..be19eeac 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -20,10 +20,9 @@ ResolutionErrors.dfy(535,7): Error: RHS (of type List) not assignable to LHS ResolutionErrors.dfy(540,7): Error: RHS (of type List) not assignable to LHS (of type List) ResolutionErrors.dfy(554,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>) ResolutionErrors.dfy(566,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree -ResolutionErrors.dfy(592,25): Error: the type of this variable is underspecified -ResolutionErrors.dfy(592,23): Error: type variable 'T' in the function call to 'P' could not be determined -ResolutionErrors.dfy(599,25): Error: the type of this variable is underspecified +ResolutionErrors.dfy(598,8): Error: the type of this local variable is underspecified ResolutionErrors.dfy(599,23): Error: type variable 'T' in the function call to 'P' could not be determined +ResolutionErrors.dfy(599,18): Error: type of bound variable 'z' could not be determined; please specify the type explicitly ResolutionErrors.dfy(612,13): Error: 'new' is not allowed in ghost contexts ResolutionErrors.dfy(613,9): Error: 'new' is not allowed in ghost contexts ResolutionErrors.dfy(622,23): Error: 'new' is not allowed in ghost contexts @@ -81,12 +80,28 @@ ResolutionErrors.dfy(1105,6): Error: RHS (of type P) not assignable to LHS ResolutionErrors.dfy(1110,13): Error: arguments must have the same type (got P and P) ResolutionErrors.dfy(1111,13): Error: arguments must have the same type (got P and P) ResolutionErrors.dfy(1112,13): Error: arguments must have the same type (got P and P) -ResolutionErrors.dfy(1135,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(1130,31): Error: a set comprehension 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 'o' +ResolutionErrors.dfy(1132,38): Error: a set comprehension 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 'o' ResolutionErrors.dfy(1137,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(1230,13): Error: type variable 'PT' in the function call to 'P' could not be determined +ResolutionErrors.dfy(1231,14): Error: the type of this variable is underspecified +ResolutionErrors.dfy(1231,19): Error: type variable 'QT' in the function call to 'Q' could not be determined +ResolutionErrors.dfy(1232,4): Error: type '?' to the method 'M' is not determined +ResolutionErrors.dfy(1233,8): Error: the type of this variable is underspecified +ResolutionErrors.dfy(1233,13): Error: type '?' to the method 'N' is not determined +ResolutionErrors.dfy(1234,8): Error: the type of this variable is underspecified +ResolutionErrors.dfy(1235,8): Error: the type of this variable is underspecified +ResolutionErrors.dfy(1236,8): Error: the type of this local variable is underspecified +ResolutionErrors.dfy(1237,8): Error: the type of this variable is underspecified +ResolutionErrors.dfy(1238,8): Error: the type of this local variable is underspecified ResolutionErrors.dfy(1242,26): Error: the type of this variable is underspecified +ResolutionErrors.dfy(1242,21): Error: type of bound variable 's' could not be determined; please specify the type explicitly ResolutionErrors.dfy(1243,31): Error: the type of this variable is underspecified +ResolutionErrors.dfy(1243,21): Error: type of bound variable 's' could not be determined; please specify the type explicitly ResolutionErrors.dfy(1244,29): Error: the type of this variable is underspecified -ResolutionErrors.dfy(1254,34): Error: the type of this variable is underspecified +ResolutionErrors.dfy(1244,21): Error: type of bound variable 'c' could not be determined; please specify the type explicitly +ResolutionErrors.dfy(1251,8): Error: the type of this local variable is underspecified +ResolutionErrors.dfy(1254,29): Error: type of bound variable 'c' could not be determined; please specify the type explicitly ResolutionErrors.dfy(1270,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?') ResolutionErrors.dfy(1271,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?') ResolutionErrors.dfy(1308,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y) @@ -209,4 +224,4 @@ ResolutionErrors.dfy(1123,8): Error: new cannot be applied to a trait ResolutionErrors.dfy(1144,13): Error: first argument to / must be of numeric type (instead got set) ResolutionErrors.dfy(1151,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(1166,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating -211 resolution/type errors detected in ResolutionErrors.dfy +226 resolution/type errors detected in ResolutionErrors.dfy diff --git a/Test/dafny4/Regression0.dfy b/Test/dafny4/Regression0.dfy index be092261..666d9575 100644 --- a/Test/dafny4/Regression0.dfy +++ b/Test/dafny4/Regression0.dfy @@ -4,10 +4,10 @@ // This once crashed Dafny method M() { - var s := [1, "2"]; + var s := [1, "2"]; // error: all elements must have the same type if * { - assert exists n :: n in s && n != 1; + assert exists n :: n in s && n != 1; // the type of n is inferred to be int } else { - assert "2" in s; + assert "2" in s; // error: since the type of s wasn't determined } } diff --git a/Test/dafny4/Regression0.dfy.expect b/Test/dafny4/Regression0.dfy.expect index 9d1e3019..566b3e3f 100644 --- a/Test/dafny4/Regression0.dfy.expect +++ b/Test/dafny4/Regression0.dfy.expect @@ -1,4 +1,3 @@ Regression0.dfy(7,15): Error: All elements of display must be of the same type (got string, but type of previous elements is int) -Regression0.dfy(9,28): Error: the type of this variable is underspecified Regression0.dfy(11,15): Error: second argument to "in" must be a set, multiset, or sequence with elements of type string, or a map with domain string (instead got ?) -3 resolution/type errors detected in Regression0.dfy +2 resolution/type errors detected in Regression0.dfy diff --git a/Test/dafny4/set-compr.dfy b/Test/dafny4/set-compr.dfy index 71a07f3d..d093a924 100644 --- a/Test/dafny4/set-compr.dfy +++ b/Test/dafny4/set-compr.dfy @@ -22,7 +22,7 @@ method O() returns (ghost p: set) method P() returns (p: set) { - p := set o: object | true; // not allowed -- not in a ghost context + p := set o: object | true; // error: not (easily) compilable } ghost method Q() returns (p: set) @@ -30,26 +30,54 @@ ghost method Q() returns (p: set) p := set o: object | true; // allowed, since the whole method is ghost } -function F(): int +function F(p: object): int + requires p in set o: object | true // error: function is not allowed to depend on allocation state + ensures p in set o: object | true // error: ditto (although one could argue that this would be okay) + reads set o: object | true // error: same as for 'requires' + decreases set o: object | true // error: same as for 'ensures' +{ + if p in set o: object | true then // error: function is not allowed to depend on allocation state + F(p) + else + 0 +} + +function method G(p: object): int + requires p in set o: object | true // error (see F) + ensures p in set o: object | true // error (see F) + reads set o: object | true // error (see F) + decreases set o: object | true // error (see F) +{ + if p in set o: object | true then // error (see F) + G(p) + else + 0 +} + +method M0() returns (ghost r: int, s: int) requires null in set o: object | true // allowed ensures null in set o: object | true // allowed - reads set o: object | true // allowed + modifies set o: object | true // allowed decreases set o: object | true // allowed { - if null in set o: object | true then // allowed -- in a ghost context - F() - else - 0 + if null in set o: object | true { // this makes the "if" a ghost + r := G(null); + s := G(null); // error: assignment of non-ghost not allowed inside ghost "if" + } else { + r := 0; + } } -function method G(): int +method M1() returns (ghost r: int, s: int) requires null in set o: object | true // (X) allowed ensures null in set o: object | true // (X) allowed - reads set o: object | true // allowed + modifies set o: object | true // allowed decreases set o: object | true // (X) allowed { - if null in set o: object | true then // not allowed, since this is not a ghost context - G() - else - 0 + if null in set o: object | true { // this makes the "if" a ghost + r := G(null); + s := G(null); // error: assignment of non-ghost not allowed inside ghost "if" + } else { + r := 0; + } } diff --git a/Test/dafny4/set-compr.dfy.expect b/Test/dafny4/set-compr.dfy.expect index 615ee2bc..b0490a11 100644 --- a/Test/dafny4/set-compr.dfy.expect +++ b/Test/dafny4/set-compr.dfy.expect @@ -1,3 +1,14 @@ set-compr.dfy(25,7): 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' -set-compr.dfy(51,13): 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' -2 resolution/type errors detected in set-compr.dfy +set-compr.dfy(34,16): Error: a set comprehension 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 'o' +set-compr.dfy(35,15): Error: a set comprehension 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 'o' +set-compr.dfy(36,8): Error: a set comprehension 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 'o' +set-compr.dfy(37,12): Error: a set comprehension 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 'o' +set-compr.dfy(39,10): Error: a set comprehension 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 'o' +set-compr.dfy(46,16): Error: a set comprehension 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 'o' +set-compr.dfy(47,15): Error: a set comprehension 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 'o' +set-compr.dfy(48,8): Error: a set comprehension 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 'o' +set-compr.dfy(49,12): Error: a set comprehension 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 'o' +set-compr.dfy(51,10): Error: a set comprehension 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 'o' +set-compr.dfy(65,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) +set-compr.dfy(79,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) +13 resolution/type errors detected in set-compr.dfy diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy index a6f8d922..60ac35f5 100644 --- a/Test/hofs/ReadsReads.dfy +++ b/Test/hofs/ReadsReads.dfy @@ -105,14 +105,14 @@ module WhatWeKnowAboutReads { module ReadsAll { function A(f: int -> int) : int - reads set o,x | o in f.reads(x) :: o + reads set x,o | o in f.reads(x) :: o // note, with "set o,x ..." instead, Dafny complains (this is perhaps less than ideal) requires forall x :: f.requires(x) { f(0) + f(1) + f(2) } function method B(f: int -> int) : int - reads set o,x | o in f.reads(x) :: o + reads set x,o | o in f.reads(x) :: o // note, with "set o,x ..." instead, Dafny complains (this is perhaps less than ideal) requires forall x :: f.requires(x) { f(0) + f(1) + f(2) -- cgit v1.2.3