From 49706a5d1599f9167cb627a305d4abb32cc71edb Mon Sep 17 00:00:00 2001 From: leino Date: Mon, 28 Sep 2015 15:36:45 -0700 Subject: Removed more traces of the previous resolution checks that happened during pass 0. Fixed resolution of specification components of alternative loops. --- Source/Dafny/Resolver.cs | 294 ++++++++++++++++---------------- Test/dafny0/ResolutionErrors.dfy | 215 +++++++++++++++-------- Test/dafny0/ResolutionErrors.dfy.expect | 275 ++++++++++++++--------------- 3 files changed, 430 insertions(+), 354 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index ec3a69c9..f4fac31b 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1368,7 +1368,7 @@ namespace Microsoft.Dafny var added = scope.Push(dd.Var.Name, dd.Var); Contract.Assert(added == Scope.PushResult.Success); ResolveType(dd.Var.tok, dd.Var.Type, dd, ResolveTypeOptionEnum.DontInfer, null); - ResolveExpression(dd.Constraint, new ResolveOpts(dd, false, true)); + ResolveExpression(dd.Constraint, new ResolveOpts(dd, false)); Contract.Assert(dd.Constraint.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(dd.Constraint.Type, Type.Bool, dd.Constraint, "newtype constraint must be of type bool (instead got {0})", dd.Constraint.Type); SolveAllTypeConstraints(); @@ -3129,6 +3129,12 @@ namespace Microsoft.Dafny Contract.Requires(msgArgs != null); resolver.reporter.Error(MessageSource.Resolver, expr, msg, msgArgs); } + protected void Error(IToken tok, string msg, params object[] msgArgs) { + Contract.Requires(tok != null); + Contract.Requires(msg != null); + Contract.Requires(msgArgs != null); + resolver.reporter.Error(MessageSource.Resolver, tok, msg, msgArgs); + } /// /// This method does three things: /// 0. Reports an error if "mustBeErasable" and the statement assigns to a non-ghost field @@ -3219,6 +3225,9 @@ namespace Microsoft.Dafny var gk = AssignStmt.LhsIsToGhost_Which(lhs); if (gk == AssignStmt.NonGhostKind.IsGhost) { s.IsGhost = true; + if (s.Rhs is TypeRhs) { + Error(s.Rhs.Tok, "'new' is not allowed in ghost contexts"); + } } else if (gk == AssignStmt.NonGhostKind.Variable && codeContext.IsGhost) { // cool } else if (mustBeErasable) { @@ -3322,6 +3331,9 @@ namespace Microsoft.Dafny if (s.IsGhost && s.Decreases.Expressions.Exists(e => e is WildcardExpr)) { Error(s, "'decreases *' is not allowed on ghost loops"); } + if (s.IsGhost && s.Mod.Expressions != null) { + s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers); + } if (s.Body != null) { Visit(s.Body, s.IsGhost); } @@ -3330,6 +3342,12 @@ namespace Microsoft.Dafny } else if (stmt is AlternativeLoopStmt) { var s = (AlternativeLoopStmt)stmt; s.IsGhost = mustBeErasable || s.Alternatives.Exists(alt => resolver.UsesSpecFeatures(alt.Guard)); + if (s.IsGhost && s.Decreases.Expressions.Exists(e => e is WildcardExpr)) { + Error(s, "'decreases *' is not allowed on ghost loops"); + } + if (s.IsGhost && s.Mod.Expressions != null) { + s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers); + } s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.IsGhost))); s.IsGhost = s.IsGhost || (!s.Decreases.Expressions.Exists(e => e is WildcardExpr) && s.Alternatives.All(alt => alt.Body.All(ss => ss.IsGhost))); @@ -3343,10 +3361,13 @@ namespace Microsoft.Dafny } else if (stmt is ModifyStmt) { var s = (ModifyStmt)stmt; + s.IsGhost = mustBeErasable; + if (s.IsGhost) { + s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers); + } if (s.Body != null) { Visit(s.Body, mustBeErasable); } - s.IsGhost = mustBeErasable; } else if (stmt is CalcStmt) { var s = (CalcStmt)stmt; @@ -3999,7 +4020,6 @@ namespace Microsoft.Dafny void ResolveAttributes(Attributes attrs, ResolveOpts opts) { Contract.Requires(opts != null); - Contract.Requires(opts.DontCareAboutCompilation); // attributes are never compiled // order does not matter much for resolution, so resolve them in reverse order foreach (var attr in attrs.AsEnumerable()) { if (attr.Args != null) { @@ -4093,23 +4113,23 @@ namespace Microsoft.Dafny foreach (Formal p in f.Formals) { scope.Push(p.Name, p); } - ResolveAttributes(f.Attributes, new ResolveOpts(f, false, true)); + ResolveAttributes(f.Attributes, new ResolveOpts(f, false)); foreach (Expression r in f.Req) { - ResolveExpression(r, new ResolveOpts(f, false, true)); + ResolveExpression(r, new ResolveOpts(f, false)); Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(r.Type, Type.Bool, r, "Precondition must be a boolean (got {0})", r.Type); } foreach (FrameExpression fr in f.Reads) { - ResolveFrameExpression(fr, true, f.IsGhost, f); + ResolveFrameExpression(fr, true, f); } foreach (Expression r in f.Ens) { - ResolveExpression(r, new ResolveOpts(f, false, true)); // since this is a function, the postcondition is still a one-state predicate + ResolveExpression(r, new ResolveOpts(f, false)); // since this is a function, the postcondition is still a one-state predicate Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(r.Type, Type.Bool, r, "Postcondition must be a boolean (got {0})", r.Type); } - ResolveAttributes(f.Decreases.Attributes, new ResolveOpts(f, false, true)); + ResolveAttributes(f.Decreases.Attributes, new ResolveOpts(f, false)); foreach (Expression r in f.Decreases.Expressions) { - ResolveExpression(r, new ResolveOpts(f, false, true)); + ResolveExpression(r, new ResolveOpts(f, false)); // any type is fine } SolveAllTypeConstraints(); @@ -4126,14 +4146,11 @@ namespace Microsoft.Dafny /// /// /// - /// /// True indicates "reads", false indicates "modifies". - /// - /// - void ResolveFrameExpression(FrameExpression fe, bool readsFrame, bool isGhostContext, ICodeContext codeContext) { + void ResolveFrameExpression(FrameExpression fe, bool readsFrame, ICodeContext codeContext) { Contract.Requires(fe != null); Contract.Requires(codeContext != null); - ResolveExpression(fe.E, new ResolveOpts(codeContext, false, true /* yes, this is ghost */)); + ResolveExpression(fe.E, new ResolveOpts(codeContext, false)); Type t = fe.E.Type; Contract.Assert(t != null); // follows from postcondition of ResolveExpression var arrTy = t.AsArrowType; @@ -4153,8 +4170,6 @@ namespace Microsoft.Dafny // error has already been reported by ResolveMember } else if (!(member is Field)) { reporter.Error(MessageSource.Resolver, fe.E, "member {0} in type {1} does not refer to a field", fe.FieldName, ctype.Name); - } else if (!readsFrame && isGhostContext && !member.IsGhost) { - reporter.Error(MessageSource.Resolver, fe.E, "in a ghost context, only ghost fields can be mentioned as modifies frame targets ({0})", fe.FieldName); } else { Contract.Assert(ctype != null && ctype.ResolvedClass != null); // follows from postcondition of ResolveMember fe.Field = (Field)member; @@ -4162,6 +4177,17 @@ namespace Microsoft.Dafny } } + /// + /// This method can be called even if the resolution of "fe" failed; in that case, this method will + /// not issue any error message. + /// + void DisallowNonGhostFieldSpecifiers(FrameExpression fe) { + Contract.Requires(fe != null); + if (fe.Field != null && !fe.Field.IsGhost) { + reporter.Error(MessageSource.Resolver, fe.E, "in a ghost context, only ghost fields can be mentioned as modifies frame targets ({0})", fe.FieldName); + } + } + /// /// Assumes type parameters have already been pushed /// @@ -4206,25 +4232,24 @@ namespace Microsoft.Dafny // Start resolving specification... foreach (MaybeFreeExpression e in m.Req) { - ResolveAttributes(e.Attributes, new ResolveOpts(m, false, true)); - ResolveExpression(e.E, new ResolveOpts(m, false, true)); + ResolveAttributes(e.Attributes, new ResolveOpts(m, false)); + ResolveExpression(e.E, new ResolveOpts(m, false)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(e.E.Type, Type.Bool, e.E, "Precondition must be a boolean (got {0})", e.E.Type); } - ResolveAttributes(m.Mod.Attributes, new ResolveOpts(m, false, true)); + ResolveAttributes(m.Mod.Attributes, new ResolveOpts(m, false)); foreach (FrameExpression fe in m.Mod.Expressions) { - ResolveFrameExpression(fe, false, m.IsGhost, m); + ResolveFrameExpression(fe, false, m); if (m is Lemma || m is FixpointLemma) { reporter.Error(MessageSource.Resolver, fe.tok, "{0}s are not allowed to have modifies clauses", m.WhatKind); + } else if (m.IsGhost) { + DisallowNonGhostFieldSpecifiers(fe); } } - ResolveAttributes(m.Decreases.Attributes, new ResolveOpts(m, false, true)); + ResolveAttributes(m.Decreases.Attributes, new ResolveOpts(m, false)); foreach (Expression e in m.Decreases.Expressions) { - ResolveExpression(e, new ResolveOpts(m, false, true)); + ResolveExpression(e, new ResolveOpts(m, false)); // any type is fine - if (m.IsGhost && e is WildcardExpr) { - reporter.Error(MessageSource.Resolver, e, "'decreases *' is not allowed on ghost methods"); - } } // Add out-parameters to a new scope that will also include the outermost-level locals of the body @@ -4240,8 +4265,8 @@ namespace Microsoft.Dafny // ... continue resolving specification foreach (MaybeFreeExpression e in m.Ens) { - ResolveAttributes(e.Attributes, new ResolveOpts(m, true, true)); - ResolveExpression(e.E, new ResolveOpts(m, true, true)); + ResolveAttributes(e.Attributes, new ResolveOpts(m, true)); + ResolveExpression(e.E, new ResolveOpts(m, true)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(e.E.Type, Type.Bool, e.E, "Postcondition must be a boolean (got {0})", e.E.Type); } @@ -4265,7 +4290,7 @@ namespace Microsoft.Dafny } // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for colemmas) - ResolveAttributes(m.Attributes, new ResolveOpts(m, false, true)); + ResolveAttributes(m.Attributes, new ResolveOpts(m, false)); scope.PopMarker(); // for the out-parameters and outermost-level locals scope.PopMarker(); // for the in-parameters @@ -4331,20 +4356,20 @@ namespace Microsoft.Dafny Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count); for (int i = 0; i < iter.Decreases.Expressions.Count; i++) { var e = iter.Decreases.Expressions[i]; - ResolveExpression(e, new ResolveOpts(iter, false, true)); + ResolveExpression(e, new ResolveOpts(iter, false)); // any type is fine, but associate this type with the corresponding _decreases field var d = iter.DecreasesFields[i]; // If the following type constraint does not hold, then: Bummer, there was a use--and a bad use--of the field before, so this won't be the best of error messages ConstrainTypes(d.Type, e.Type, e, "type of field {0} is {1}, but has been constrained elsewhere to be of type {2}", d.Name, e.Type, d.Type); } foreach (FrameExpression fe in iter.Reads.Expressions) { - ResolveFrameExpression(fe, true, false, iter); + ResolveFrameExpression(fe, true, iter); } foreach (FrameExpression fe in iter.Modifies.Expressions) { - ResolveFrameExpression(fe, false, false, iter); + ResolveFrameExpression(fe, false, iter); } foreach (MaybeFreeExpression e in iter.Requires) { - ResolveExpression(e.E, new ResolveOpts(iter, false, true)); + ResolveExpression(e.E, new ResolveOpts(iter, false)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(e.E.Type, Type.Bool, e.E, "Precondition must be a boolean (got {0})", e.E.Type); } @@ -4358,22 +4383,22 @@ namespace Microsoft.Dafny Contract.Assert(scope.AllowInstance); foreach (MaybeFreeExpression e in iter.YieldRequires) { - ResolveExpression(e.E, new ResolveOpts(iter, false, true)); + ResolveExpression(e.E, new ResolveOpts(iter, false)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(e.E.Type, Type.Bool, e.E, "Yield precondition must be a boolean (got {0})", e.E.Type); } foreach (MaybeFreeExpression e in iter.YieldEnsures) { - ResolveExpression(e.E, new ResolveOpts(iter, true, true)); + ResolveExpression(e.E, new ResolveOpts(iter, true)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(e.E.Type, Type.Bool, e.E, "Yield postcondition must be a boolean (got {0})", e.E.Type); } foreach (MaybeFreeExpression e in iter.Ensures) { - ResolveExpression(e.E, new ResolveOpts(iter, true, true)); + ResolveExpression(e.E, new ResolveOpts(iter, true)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(e.E.Type, Type.Bool, e.E, "Postcondition must be a boolean (got {0})", e.E.Type); } - ResolveAttributes(iter.Attributes, new ResolveOpts(iter, false, true)); + ResolveAttributes(iter.Attributes, new ResolveOpts(iter, false)); var postSpecErrorCount = reporter.Count(ErrorLevel.Error); @@ -4687,13 +4712,13 @@ namespace Microsoft.Dafny } var prevErrorCount = reporter.Count(ErrorLevel.Error); if (t.NamePath is ExprDotName) { - var ret = ResolveDotSuffix_Type((ExprDotName)t.NamePath, new ResolveOpts(context, true, true), allowDanglingDotName, option, defaultTypeArguments); + var ret = ResolveDotSuffix_Type((ExprDotName)t.NamePath, new ResolveOpts(context, true), allowDanglingDotName, option, defaultTypeArguments); if (ret != null) { return ret; } } else { var s = (NameSegment)t.NamePath; - ResolveNameSegment_Type(s, new ResolveOpts(context, true, true), option, defaultTypeArguments); + ResolveNameSegment_Type(s, new ResolveOpts(context, true), option, defaultTypeArguments); } if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { var r = t.NamePath.Resolved as Resolver_IdentifierExpr; @@ -5225,17 +5250,17 @@ namespace Microsoft.Dafny Contract.Requires(stmt != null); Contract.Requires(codeContext != null); if (!(stmt is ForallStmt)) { // forall statements do their own attribute resolution below - ResolveAttributes(stmt.Attributes, new ResolveOpts(codeContext, true, true)); + ResolveAttributes(stmt.Attributes, new ResolveOpts(codeContext, true)); } if (stmt is PredicateStmt) { PredicateStmt s = (PredicateStmt)stmt; - ResolveExpression(s.Expr, new ResolveOpts(codeContext, true, true)); + ResolveExpression(s.Expr, new ResolveOpts(codeContext, true)); Contract.Assert(s.Expr.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(s.Expr.Type, Type.Bool, s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type); } else if (stmt is PrintStmt) { var s = (PrintStmt)stmt; - var opts = new ResolveOpts(codeContext, false, specContextOnly); + var opts = new ResolveOpts(codeContext, false); s.Args.Iter(e => ResolveExpression(e, opts)); } else if (stmt is BreakStmt) { @@ -5346,7 +5371,7 @@ namespace Microsoft.Dafny } // With the new locals in scope, it's now time to resolve the attributes on all the locals foreach (var local in s.Locals) { - ResolveAttributes(local.Attributes, new ResolveOpts(codeContext, true, true)); + ResolveAttributes(local.Attributes, new ResolveOpts(codeContext, true)); } // Resolve the AssignSuchThatStmt, if any if (s.Update is AssignSuchThatStmt) { @@ -5374,18 +5399,16 @@ namespace Microsoft.Dafny } else if (stmt is AssignStmt) { AssignStmt s = (AssignStmt)stmt; int prevErrorCount = reporter.Count(ErrorLevel.Error); - ResolveExpression(s.Lhs, new ResolveOpts(codeContext, true, specContextOnly)); // allow ghosts for now, tighted up below + ResolveExpression(s.Lhs, new ResolveOpts(codeContext, true)); // allow ghosts for now, tighted up below bool lhsResolvedSuccessfully = reporter.Count(ErrorLevel.Error) == prevErrorCount; Contract.Assert(s.Lhs.Type != null); // follows from postcondition of ResolveExpression // check that LHS denotes a mutable variable or a field - bool lvalueIsGhost = false; var lhs = s.Lhs.Resolved; if (lhs is IdentifierExpr) { IVariable var = ((IdentifierExpr)lhs).Var; if (var == null) { // the LHS didn't resolve correctly; some error would already have been reported } else { - lvalueIsGhost = var.IsGhost || codeContext.IsGhost; CheckIsLvalue(lhs, codeContext); var localVar = var as LocalVariable; @@ -5411,7 +5434,6 @@ namespace Microsoft.Dafny } else if (lhs is MemberSelectExpr) { var fse = (MemberSelectExpr)lhs; if (fse.Member != null) { // otherwise, an error was reported above - lvalueIsGhost = fse.Member.IsGhost; CheckIsLvalue(fse, codeContext); } } else if (lhs is SeqSelectExpr) { @@ -5432,12 +5454,12 @@ namespace Microsoft.Dafny Type lhsType = s.Lhs.Type; if (s.Rhs is ExprRhs) { ExprRhs rr = (ExprRhs)s.Rhs; - ResolveExpression(rr.Expr, new ResolveOpts(codeContext, true, specContextOnly)); + ResolveExpression(rr.Expr, new ResolveOpts(codeContext, true)); Contract.Assert(rr.Expr.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(lhsType, rr.Expr.Type, stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, lhsType); } else if (s.Rhs is TypeRhs) { TypeRhs rr = (TypeRhs)s.Rhs; - Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost, codeContext); + Type t = ResolveTypeRhs(rr, stmt, codeContext); ConstrainTypes(lhsType, t, stmt, "type {0} is not assignable to LHS (of type {1})", t, lhsType); } else if (s.Rhs is HavocRhs) { // nothing else to do @@ -5447,7 +5469,7 @@ namespace Microsoft.Dafny } else if (stmt is CallStmt) { CallStmt s = (CallStmt)stmt; - ResolveCallStmt(s, specContextOnly, codeContext, null); + ResolveCallStmt(s, codeContext, null); } else if (stmt is BlockStmt) { var s = (BlockStmt)stmt; @@ -5460,7 +5482,7 @@ namespace Microsoft.Dafny bool branchesAreSpecOnly = specContextOnly; if (s.Guard != null) { int prevErrorCount = reporter.Count(ErrorLevel.Error); - ResolveExpression(s.Guard, new ResolveOpts(codeContext, true, specContextOnly)); + 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); @@ -5483,7 +5505,7 @@ namespace Microsoft.Dafny var fvs = new HashSet(); if (s.Guard != null) { int prevErrorCount = reporter.Count(ErrorLevel.Error); - ResolveExpression(s.Guard, new ResolveOpts(codeContext, true, specContextOnly)); + 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); @@ -5493,34 +5515,8 @@ namespace Microsoft.Dafny } } - foreach (MaybeFreeExpression inv in s.Invariants) { - ResolveAttributes(inv.Attributes, new ResolveOpts(codeContext, true, true)); - ResolveExpression(inv.E, new ResolveOpts(codeContext, true, true)); - Contract.Assert(inv.E.Type != null); // follows from postcondition of ResolveExpression - Translator.ComputeFreeVariables(inv.E, fvs); - ConstrainTypes(inv.E.Type, Type.Bool, inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type); - } + ResolveLoopSpecificationComponents(s.Invariants, s.Decreases, s.Mod, codeContext, fvs); - ResolveAttributes(s.Decreases.Attributes, new ResolveOpts(codeContext, true, true)); - foreach (Expression e in s.Decreases.Expressions) { - ResolveExpression(e, new ResolveOpts(codeContext, true, true)); - if (e is WildcardExpr) { - if (bodyMustBeSpecOnly) { - reporter.Error(MessageSource.Resolver, e, "'decreases *' is not allowed on ghost loops"); - } else if (!codeContext.AllowsNontermination && !DafnyOptions.O.Dafnycc) { - reporter.Error(MessageSource.Resolver, e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating"); - } - } - // any type is fine - } - - if (s.Mod.Expressions != null) { - ResolveAttributes(s.Mod.Attributes, new ResolveOpts(codeContext, true, true)); - foreach (FrameExpression fe in s.Mod.Expressions) { - ResolveFrameExpression(fe, false, bodyMustBeSpecOnly, codeContext); - Translator.ComputeFreeVariables(fe.E, fvs); - } - } if (s.Body != null) { loopStack.Add(s); // push if (s.Labels == null) { // otherwise, "s" is already in "inSpecOnlyContext" map @@ -5537,21 +5533,7 @@ namespace Microsoft.Dafny } else if (stmt is AlternativeLoopStmt) { var s = (AlternativeLoopStmt)stmt; ResolveAlternatives(s.Alternatives, specContextOnly, s, codeContext); - foreach (MaybeFreeExpression inv in s.Invariants) { - ResolveExpression(inv.E, new ResolveOpts(codeContext, true, true)); - Contract.Assert(inv.E.Type != null); // follows from postcondition of ResolveExpression - ConstrainTypes(inv.E.Type, Type.Bool, inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type); - } - - foreach (Expression e in s.Decreases.Expressions) { - ResolveExpression(e, new ResolveOpts(codeContext, true, true)); - if (e is WildcardExpr) { - if (!codeContext.AllowsNontermination && !DafnyOptions.O.Dafnycc) { - reporter.Error(MessageSource.Resolver, e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating"); - } - } - // any type is fine - } + ResolveLoopSpecificationComponents(s.Invariants, s.Decreases, s.Mod, codeContext, null); } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; @@ -5562,17 +5544,17 @@ namespace Microsoft.Dafny ScopePushAndReport(scope, v, "local-variable"); ResolveType(v.tok, v.Type, codeContext, ResolveTypeOptionEnum.InferTypeProxies, null); } - ResolveExpression(s.Range, new ResolveOpts(codeContext, true, specContextOnly)); + ResolveExpression(s.Range, new ResolveOpts(codeContext, true)); Contract.Assert(s.Range.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(s.Range.Type, Type.Bool, stmt, "range restriction in forall statement must be of type bool (instead got {0})", s.Range.Type); foreach (var ens in s.Ens) { - ResolveExpression(ens.E, new ResolveOpts(codeContext, true, true)); + ResolveExpression(ens.E, new ResolveOpts(codeContext, true)); Contract.Assert(ens.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(ens.E.Type, Type.Bool, ens.E, "ensures condition is expected to be of type {0}, but is {1}", Type.Bool, ens.E.Type); } // Since the range and postconditions are more likely to infer the types of the bound variables, resolve them // first (above) and only then resolve the attributes (below). - ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, true, true)); + 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)) { @@ -5637,10 +5619,9 @@ namespace Microsoft.Dafny } else if (stmt is ModifyStmt) { var s = (ModifyStmt)stmt; - ResolveAttributes(s.Mod.Attributes, new ResolveOpts(codeContext, true, true)); + ResolveAttributes(s.Mod.Attributes, new ResolveOpts(codeContext, true)); foreach (FrameExpression fe in s.Mod.Expressions) { - // (yes, say "modifies", not "modify", in the next line -- it seems to give a more readable error message - ResolveFrameExpression(fe, false, specContextOnly, codeContext); + ResolveFrameExpression(fe, false, codeContext); } if (s.Body != null) { ResolveBlockStatement(s.Body, specContextOnly, codeContext); @@ -5651,17 +5632,17 @@ namespace Microsoft.Dafny CalcStmt s = (CalcStmt)stmt; if (s.Lines.Count > 0) { var e0 = s.Lines.First(); - ResolveExpression(e0, new ResolveOpts(codeContext, true, true)); + ResolveExpression(e0, new ResolveOpts(codeContext, true)); Contract.Assert(e0.Type != null); // follows from postcondition of ResolveExpression for (int i = 1; i < s.Lines.Count; i++) { if (i < s.Lines.Count - 1 || prevErrorCount == reporter.Count(ErrorLevel.Error)) { // do not resolve the dummy step if there were errors, it might generate more errors var e1 = s.Lines[i]; - ResolveExpression(e1, new ResolveOpts(codeContext, true, true)); + ResolveExpression(e1, new ResolveOpts(codeContext, true)); Contract.Assert(e1.Type != null); // follows from postcondition of ResolveExpression if (!ConstrainTypes(e0.Type, e1.Type, e1, "all lines in a calculation must have the same type (got {0} after {1})", e1.Type, e0.Type)) { } else { var step = s.StepOps[i - 1].StepExpr(e0, e1); // Use custom line operator - ResolveExpression(step, new ResolveOpts(codeContext, true, true)); + ResolveExpression(step, new ResolveOpts(codeContext, true)); s.Steps.Add(step); } e0 = e1; @@ -5686,7 +5667,7 @@ namespace Microsoft.Dafny } else { s.Result = CalcStmt.DefaultOp.StepExpr(Expression.CreateIntLiteral(s.Tok, 0), Expression.CreateIntLiteral(s.Tok, 0)); } - ResolveExpression(s.Result, new ResolveOpts(codeContext, true, true)); + ResolveExpression(s.Result, new ResolveOpts(codeContext, true)); Contract.Assert(s.Result != null); Contract.Assert(prevErrorCount != reporter.Count(ErrorLevel.Error) || s.Steps.Count == s.Hints.Count); @@ -5704,13 +5685,51 @@ namespace Microsoft.Dafny } } + private void ResolveLoopSpecificationComponents(List invariants, Specification decreases, Specification modifies, ICodeContext codeContext, HashSet fvs) { + Contract.Requires(invariants != null); + Contract.Requires(decreases != null); + Contract.Requires(modifies != null); + Contract.Requires(codeContext != null); + + foreach (MaybeFreeExpression inv in invariants) { + ResolveAttributes(inv.Attributes, new ResolveOpts(codeContext, true)); + ResolveExpression(inv.E, new ResolveOpts(codeContext, true)); + Contract.Assert(inv.E.Type != null); // follows from postcondition of ResolveExpression + if (fvs != null) { + Translator.ComputeFreeVariables(inv.E, fvs); + } + ConstrainTypes(inv.E.Type, Type.Bool, inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type); + } + + ResolveAttributes(decreases.Attributes, new ResolveOpts(codeContext, true)); + foreach (Expression e in decreases.Expressions) { + ResolveExpression(e, new ResolveOpts(codeContext, true)); + if (e is WildcardExpr) { + if (!codeContext.AllowsNontermination && !DafnyOptions.O.Dafnycc) { + reporter.Error(MessageSource.Resolver, e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating"); + } + } + // any type is fine + } + + ResolveAttributes(modifies.Attributes, new ResolveOpts(codeContext, true)); + if (modifies.Expressions != null) { + foreach (FrameExpression fe in modifies.Expressions) { + ResolveFrameExpression(fe, false, codeContext); + if (fvs != null) { + Translator.ComputeFreeVariables(fe.E, fvs); + } + } + } + } + void ResolveMatchStmt(Statement stmt, bool specContextOnly, ICodeContext codeContext) { MatchStmt s = (MatchStmt)stmt; DesugarMatchStmtWithTupleExpression(s); bool bodyIsSpecOnly = specContextOnly; int prevErrorCount = reporter.Count(ErrorLevel.Error); - ResolveExpression(s.Source, new ResolveOpts(codeContext, true, specContextOnly)); + 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) { @@ -6230,7 +6249,7 @@ namespace Microsoft.Dafny var lhsNameSet = new HashSet(); // used to check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification) foreach (var lhs in s.Lhss) { var ec = reporter.Count(ErrorLevel.Error); - ResolveExpression(lhs, new ResolveOpts(codeContext, true, specContextOnly)); + ResolveExpression(lhs, new ResolveOpts(codeContext, true)); if (ec == reporter.Count(ErrorLevel.Error)) { if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) { reporter.Error(MessageSource.Resolver, lhs, "cannot assign to a range of array elements (try the 'forall' statement)"); @@ -6241,11 +6260,11 @@ namespace Microsoft.Dafny // Resolve RHSs if (update == null) { var suchThat = (AssignSuchThatStmt)s; // this is the other possible subclass - ResolveAssignSuchThatStmt(suchThat, specContextOnly, codeContext); + ResolveAssignSuchThatStmt(suchThat, codeContext); } else { ResolveUpdateStmt(update, specContextOnly, codeContext, errorCountBeforeCheckingLhs); } - ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, true, true)); + ResolveAttributes(s.Attributes, new ResolveOpts(codeContext, true)); } /// /// Resolve the RHSs and entire UpdateStmt (LHSs should already have been checked by the caller). @@ -6262,7 +6281,7 @@ namespace Microsoft.Dafny bool isEffectful; if (rhs is TypeRhs) { var tr = (TypeRhs)rhs; - ResolveTypeRhs(tr, update, specContextOnly, codeContext); + ResolveTypeRhs(tr, update, codeContext); isEffectful = tr.InitCall != null; } else if (rhs is HavocRhs) { isEffectful = false; @@ -6270,17 +6289,11 @@ namespace Microsoft.Dafny var er = (ExprRhs)rhs; if (er.Expr is ApplySuffix) { var a = (ApplySuffix)er.Expr; - // Note, in the following line, the dontCareAboutCompilation could be more precise. It could be computed as in the else - // branch if the ApplySuffix is really just the RHS of an assignment. However, if "update" is really a call statement, - // then we should not let the LHS influence the call to ResolveApplySuffix. Unfortunately, we don't know which case - // we're in until ResolveApplySuffix has returned (where a non-null cRhs indicates that "update" is a call statement). - // So, we'll be conservative and will simply pass in specContextOnly here. - var cRhs = ResolveApplySuffix(a, new ResolveOpts(codeContext, true, specContextOnly/*see note on previous line*/), true); + var cRhs = ResolveApplySuffix(a, new ResolveOpts(codeContext, true), true); isEffectful = cRhs != null; methodCallInfo = methodCallInfo ?? cRhs; } else { - var dontCareAboutCompilation = specContextOnly || (j < update.Lhss.Count && AssignStmt.LhsIsToGhost(update.Lhss[j])); - ResolveExpression(er.Expr, new ResolveOpts(codeContext, true, dontCareAboutCompilation)); + ResolveExpression(er.Expr, new ResolveOpts(codeContext, true)); isEffectful = false; } } @@ -6355,7 +6368,7 @@ namespace Microsoft.Dafny } } - private void ResolveAssignSuchThatStmt(AssignSuchThatStmt s, bool specContextOnly, ICodeContext codeContext) { + private void ResolveAssignSuchThatStmt(AssignSuchThatStmt s, ICodeContext codeContext) { Contract.Requires(s != null); Contract.Requires(codeContext != null); @@ -6373,7 +6386,7 @@ namespace Microsoft.Dafny } var ec = reporter.Count(ErrorLevel.Error); - ResolveExpression(s.Expr, new ResolveOpts(codeContext, true, specContextOnly)); + ResolveExpression(s.Expr, new ResolveOpts(codeContext, true)); ConstrainTypes(s.Expr.Type, Type.Bool, s.Expr, "type of RHS of assign-such-that statement must be boolean (got {0})", s.Expr.Type); } @@ -6384,7 +6397,7 @@ namespace Microsoft.Dafny // first, resolve the guards, which tells us whether or not the entire statement is a ghost statement foreach (var alternative in alternatives) { int prevErrorCount = reporter.Count(ErrorLevel.Error); - ResolveExpression(alternative.Guard, new ResolveOpts(codeContext, true, specContextOnly)); + ResolveExpression(alternative.Guard, new ResolveOpts(codeContext, true)); Contract.Assert(alternative.Guard.Type != null); // follows from postcondition of ResolveExpression bool successfullyResolved = reporter.Count(ErrorLevel.Error) == prevErrorCount; ConstrainTypes(alternative.Guard.Type, Type.Bool, alternative.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, alternative.Guard.Type); @@ -6412,7 +6425,7 @@ namespace Microsoft.Dafny /// Resolves the given call statement. /// Assumes all LHSs have already been resolved (and checked for mutability). /// - void ResolveCallStmt(CallStmt s, bool specContextOnly, ICodeContext codeContext, Type receiverType) { + void ResolveCallStmt(CallStmt s, ICodeContext codeContext, Type receiverType) { Contract.Requires(s != null); Contract.Requires(codeContext != null); bool isInitCall = receiverType != null; @@ -6430,8 +6443,7 @@ namespace Microsoft.Dafny // resolve arguments int j = 0; foreach (Expression e in s.Args) { - bool allowGhost = callee.Ins.Count <= j || callee.Ins[j].IsGhost; - ResolveExpression(e, new ResolveOpts(codeContext, true, allowGhost)); + ResolveExpression(e, new ResolveOpts(codeContext, true)); j++; } @@ -6827,16 +6839,12 @@ namespace Microsoft.Dafny } } - Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContextOnly, ICodeContext codeContext) { + Type ResolveTypeRhs(TypeRhs rr, Statement stmt, ICodeContext codeContext) { Contract.Requires(rr != null); Contract.Requires(stmt != null); Contract.Requires(codeContext != null); Contract.Ensures(Contract.Result() != null); - // "new" is not allowed in ghost contexts - if (specContextOnly) { - reporter.Error(MessageSource.Resolver, rr.Tok, "'new' is not allowed in ghost contexts"); - } if (rr.Type == null) { if (rr.ArrayDimensions != null) { // ---------- new T[EE] @@ -6888,13 +6896,13 @@ namespace Microsoft.Dafny // type, create an dot-suffix expression around this receiver, and then resolve it in the usual way for dot-suffix expressions. var lhs = new ImplicitThisExpr(initCallTok) { Type = rr.EType }; var callLhs = new ExprDotName(initCallTok, lhs, initCallName, ret == null ? null : ret.LastComponent.OptTypeArguments); - ResolveDotSuffix(callLhs, true, rr.Arguments, new ResolveOpts(codeContext, true, specContextOnly), true); + ResolveDotSuffix(callLhs, true, rr.Arguments, new ResolveOpts(codeContext, true), true); if (prevErrorCount == reporter.Count(ErrorLevel.Error)) { Contract.Assert(callLhs.ResolvedExpression is MemberSelectExpr); // since ResolveApplySuffix succeeded and call.Lhs denotes an expression (not a module or a type) var methodSel = (MemberSelectExpr)callLhs.ResolvedExpression; if (methodSel.Member is Method) { rr.InitCall = new CallStmt(initCallTok, stmt.EndTok, new List(), methodSel, rr.Arguments); - ResolveCallStmt(rr.InitCall, specContextOnly, codeContext, rr.EType); + ResolveCallStmt(rr.InitCall, codeContext, rr.EType); if (rr.InitCall.Method is Constructor) { callsConstructor = true; } @@ -7170,24 +7178,10 @@ namespace Microsoft.Dafny { public readonly ICodeContext codeContext; public readonly bool twoState; - public readonly bool DontCareAboutCompilation; public ResolveOpts(ICodeContext codeContext, bool twoState) { Contract.Requires(codeContext != null); this.codeContext = codeContext; this.twoState = twoState; - DontCareAboutCompilation = codeContext.IsGhost; - } - public ResolveOpts(ICodeContext codeContext, bool twoState, bool dontCareAboutCompilation) { - Contract.Requires(codeContext != null); - this.codeContext = codeContext; - this.twoState = twoState; - this.DontCareAboutCompilation = dontCareAboutCompilation; - } - public ResolveOpts(ResolveOpts r, bool dontCareAboutCompilation) { - Contract.Requires(r != null); - this.codeContext = r.codeContext; - this.twoState = r.twoState; - this.DontCareAboutCompilation = dontCareAboutCompilation; } } @@ -7846,7 +7840,7 @@ namespace Microsoft.Dafny } } ResolveExpression(e.Body, opts); - ResolveAttributes(e.Attributes, new ResolveOpts(opts, true)); + ResolveAttributes(e.Attributes, opts); scope.PopMarker(); expr.Type = e.Body.Type; @@ -7873,16 +7867,16 @@ namespace Microsoft.Dafny reporter.Error(MessageSource.Resolver, expr, "a quantifier cannot quantify over types. Possible fix: use the experimental attribute :typeQuantifier"); } if (e.Range != null) { - ResolveExpression(e.Range, new ResolveOpts(opts, true)); + ResolveExpression(e.Range, opts); Contract.Assert(e.Range.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(e.Range.Type, Type.Bool, expr, "range of quantifier must be of type bool (instead got {0})", e.Range.Type); } - ResolveExpression(e.Term, new ResolveOpts(opts, true)); + ResolveExpression(e.Term, opts); Contract.Assert(e.Term.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(e.Term.Type, Type.Bool, expr, "body of quantifier must be of type bool (instead got {0})", e.Term.Type); // Since the body is more likely to infer the types of the bound variables, resolve it // first (above) and only then resolve the attributes (below). - ResolveAttributes(e.Attributes, new ResolveOpts(opts, true)); + ResolveAttributes(e.Attributes, opts); scope.PopMarker(); allTypeParameters.PopMarker(); expr.Type = Type.Bool; @@ -7920,7 +7914,7 @@ namespace Microsoft.Dafny ResolveExpression(e.Term, opts); Contract.Assert(e.Term.Type != null); // follows from postcondition of ResolveExpression - ResolveAttributes(e.Attributes, new ResolveOpts(opts, true)); + ResolveAttributes(e.Attributes, opts); scope.PopMarker(); expr.Type = new SetType(e.Finite, e.Term.Type); @@ -7941,7 +7935,7 @@ namespace Microsoft.Dafny ResolveExpression(e.Term, opts); Contract.Assert(e.Term.Type != null); // follows from postcondition of ResolveExpression - ResolveAttributes(e.Attributes, new ResolveOpts(opts, true)); + ResolveAttributes(e.Attributes, opts); scope.PopMarker(); expr.Type = new MapType(e.Finite, e.BoundVars[0].Type, e.Term.Type); @@ -7974,7 +7968,7 @@ namespace Microsoft.Dafny } foreach (var read in e.Reads) { - ResolveFrameExpression(read, true, false, opts.codeContext); + ResolveFrameExpression(read, true, opts.codeContext); } ResolveExpression(e.Term, opts); diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 9d4d67f1..49e6efa0 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -9,9 +9,9 @@ method GhostDivergentLoop() a[1] := -1; ghost var i := 0; while (i < 2) - decreases *; // error: not allowed on a ghost loop - invariant i <= 2; - invariant (forall j :: 0 <= j && j < i ==> a[j] > 0); + decreases * // error: not allowed on a ghost loop + invariant i <= 2 + invariant (forall j :: 0 <= j && j < i ==> a[j] > 0) { i := 0; } @@ -613,20 +613,7 @@ module GhostAllocationTests { p := new G; // error: ditto } - method GhostNew1(n: nat) - { - var a := new G[n]; - forall i | 0 <= i < n { - a[i] := new G; // error: 'new' is currently not supported in forall statements - } - forall i | 0 <= i < n - ensures true; // this makes the whole 'forall' statement into a ghost statement - { - a[i] := new G; // error: 'new' not allowed in ghost contexts, and proof-forall cannot update state - } - } - - method GhostNew2(n: nat, ghost g: int) returns (t: G, z: int) + method GhostNew1(n: nat, ghost g: int) returns (t: G, z: int) { if n < 0 { z, t := 5, new G; // fine @@ -636,14 +623,14 @@ module GhostAllocationTests { } } - method GhostNew3(ghost b: bool) + method GhostNew2(ghost b: bool) { if (b) { var y := new GIter(); // error: 'new' not allowed in ghost contexts (and a non-ghost method is not allowed to be called here either) } } - method GhostNew4(n: nat) + method GhostNew3(n: nat) { var g := new G; calc { @@ -653,12 +640,28 @@ module GhostAllocationTests { } } - ghost method GhostNew5(g: G) + ghost method GhostNew4(g: G) modifies g; { } } +module NewForall { + class G { } + method NewForallTest(n: nat) + { + var a := new G[n]; + forall i | 0 <= i < n { + a[i] := new G; // error: 'new' is currently not supported in forall statements + } + forall i | 0 <= i < n + ensures true; // this makes the whole 'forall' statement into a ghost statement + { + a[i] := new G; // error: 'new' not allowed in ghost contexts, and proof-forall cannot update state + } + } +} + // ------------------------- underspecified types ------------------------------ module UnderspecifiedTypes { @@ -706,7 +709,7 @@ module StatementsInExpressions { { assert 6 < 8; } { var x := 8; while x != 0 - decreases *; // error: cannot use 'decreases *' in a ghost context + decreases * // error: cannot use 'decreases *' here { x := x - 1; } @@ -739,7 +742,7 @@ module StatementsInExpressions { { assert 6 < 8; } { var x := 8; while x != 0 - decreases *; // error: cannot use 'decreases *' in a ghost context + decreases * // error: cannot use 'decreases *' here { x := x - 1; } @@ -852,40 +855,48 @@ class ModifyStatementClass { ghost method G0() modifies `g; modifies `x; // error: non-ghost field mentioned in ghost context - { - modify `g; - modify `x; // error: non-ghost field mentioned in ghost context - } - method G1() - modifies this; - { - modify `x; - if g < 100 { - // we are now in a ghost context +} +module ModifyStatementClass_More { + class C { + var x: int; + ghost var g: int; + ghost method G0() + modifies `g; + { + modify `g; modify `x; // error: non-ghost field mentioned in ghost context } - } - method G2(y: nat) - modifies this; - { - if g < 100 { - // we're now in a ghost context - var n := 0; - while n < y - modifies `x; // error: non-ghost field mentioned in ghost context - { - if * { - g := g + 1; // if we got as far as verification, this would be flagged as an error too - } - n := n + 1; + method G1() + modifies this; + { + modify `x; + if g < 100 { + // we are now in a ghost context + modify `x; // error: non-ghost field mentioned in ghost context } } - modify `x; // fine - ghost var i := 0; - while i < y - modifies `x; // error: non-ghost field mentioned in ghost context + method G2(y: nat) + modifies this; { - i := i + 1; + if g < 100 { + // we're now in a ghost context + var n := 0; + while n < y + modifies `x; // error: non-ghost field mentioned in ghost context + { + if * { + g := g + 1; // if we got as far as verification, this would be flagged as an error too + } + n := n + 1; + } + } + modify `x; // fine + ghost var i := 0; + while i < y + modifies `x; // error: non-ghost field mentioned in ghost context + { + i := i + 1; + } } } } @@ -1298,7 +1309,7 @@ module FrameTargetFields { modifies `z // cool { } - +} } module FrameTargetFields_More { class C { var x: int var y: int ghost var z: int method P() modifies this { @@ -1400,20 +1411,20 @@ module SuchThat { module GhostTests { class G { } - method GhostNew4(n: nat) + method GhostNew3(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 + { if n != 0 { GhostNew3(n-1); } } // error: cannot call non-ghost method in a ghost context 1 + 4; - { GhostNew5(g); } // error: cannot call method with nonempty modifies + { GhostNew4(g); } // error: cannot call method with nonempty modifies -5 + 10; } } - ghost method GhostNew5(g: G) + ghost method GhostNew4(g: G) modifies g; { } @@ -1524,7 +1535,7 @@ module EvenMoreGhostTests { ensures false; { while (true) - decreases *; // error: not allowed in ghost context + decreases * // error: not allowed here { } } @@ -1548,20 +1559,6 @@ module EvenMoreGhostTests { } } } - 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 { @@ -1619,3 +1616,79 @@ module UnderspecifiedTypedShouldBeResolvedOnlyOnce { } } } + +module LoopResolutionTests { + class C { + var x: int + ghost var y: int + } + + ghost method M(c: C) + requires c != null + modifies c + { + var n := 0; + while n < 100 + modifies c`y + modifies c`x // error: not allowed to mention non-ghost field in modifies clause of ghost loops + { + c.x := c.x + 1; // error: assignment to non-ghost field not allowed here + } + } + + method MM(c: C) + requires c != null + modifies c + { + var n := 0; + while + invariant n <= 100 + modifies c // regression test + { + case n < 100 => n := n + 1; + } + } + + method MMX(c: C, ghost g: int) + requires c != null + modifies c + { + var n := 0; + while + invariant n <= 100 + modifies c`y + modifies c`x // error: not allowed to mention non-ghost field in modifies clause of ghost loops + { + case n < 100 => n := n + 1; // error: cannot assign to non-ghost in a ghost loop + case g < 56 && n != 100 => n := n + 1; // error: cannot assign to non-ghost in a ghost loop + } + } + + method MD0(c: C, ghost g: nat) + requires c != null + modifies c + decreases * + { + var n := 0; + while n + g < 100 + invariant n <= 100 + decreases * // error: disallowed on ghost loops + { + n := n + 1; // error: cannot assign to non-ghost in a ghost loop + } + } + + method MD1(c: C, ghost g: nat) + requires c != null + modifies c + decreases * + { + var n := 0; + while + invariant n <= 100 + decreases * // error: disallowed on ghost loops + { + case n + g < 100 => n := n + 1; // error: cannot assign to non-ghost in a ghost loop + } + } +} diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 6f4b3519..edf61b33 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -26,113 +26,126 @@ ResolutionErrors.dfy(599,25): Error: the type of this variable is underspecified ResolutionErrors.dfy(599,23): Error: type variable 'T' in the function call to 'P' could not be determined 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(620,14): Error: new allocation not supported in forall statements -ResolutionErrors.dfy(625,11): Error: the body of the enclosing forall statement is not allowed to update heap locations -ResolutionErrors.dfy(625,14): Error: new allocation not allowed in ghost context -ResolutionErrors.dfy(635,23): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(642,15): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(651,17): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(669,21): Error: the type of this variable is underspecified -ResolutionErrors.dfy(709,22): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(742,22): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(773,19): Error: calls to methods with side-effects are not allowed inside a statement expression -ResolutionErrors.dfy(774,20): Error: wrong number of method result arguments (got 0, expected 1) -ResolutionErrors.dfy(786,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -ResolutionErrors.dfy(796,4): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(807,36): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(816,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -ResolutionErrors.dfy(830,6): Error: RHS (of type B) not assignable to LHS (of type object) -ResolutionErrors.dfy(831,6): Error: RHS (of type int) not assignable to LHS (of type object) -ResolutionErrors.dfy(832,6): Error: RHS (of type B) not assignable to LHS (of type object) -ResolutionErrors.dfy(837,6): Error: RHS (of type G) not assignable to LHS (of type object) -ResolutionErrors.dfy(838,6): Error: RHS (of type Dt) not assignable to LHS (of type object) -ResolutionErrors.dfy(839,6): Error: RHS (of type CoDt) not assignable to LHS (of type object) -ResolutionErrors.dfy(901,4): Error: LHS of array assignment must denote an array element (found seq) -ResolutionErrors.dfy(902,4): Error: LHS of array assignment must denote an array element (found seq) -ResolutionErrors.dfy(907,10): Error: LHS of assignment must denote a mutable field -ResolutionErrors.dfy(908,10): Error: LHS of assignment must denote a mutable field -ResolutionErrors.dfy(909,9): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors.dfy(910,9): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors.dfy(911,5): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors.dfy(912,5): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors.dfy(993,11): Error: Wrong number of type arguments (2 instead of 1) passed to array type: array3 -ResolutionErrors.dfy(994,11): Error: Wrong number of type arguments (2 instead of 1) passed to class: C -ResolutionErrors.dfy(1005,7): Error: Duplicate name of top-level declaration: BadSyn2 -ResolutionErrors.dfy(1002,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List -ResolutionErrors.dfy(1003,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name or declare a module import 'opened?') -ResolutionErrors.dfy(1004,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?') -ResolutionErrors.dfy(1011,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A -ResolutionErrors.dfy(1014,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A -ResolutionErrors.dfy(1018,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A -ResolutionErrors.dfy(1027,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed -ResolutionErrors.dfy(1030,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A -ResolutionErrors.dfy(1035,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A -ResolutionErrors.dfy(1054,21): Error: unresolved identifier: x -ResolutionErrors.dfy(1061,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P -ResolutionErrors.dfy(1073,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name or declare a module import 'opened?') -ResolutionErrors.dfy(1083,6): Error: RHS (of type P) not assignable to LHS (of type P) -ResolutionErrors.dfy(1088,6): Error: RHS (of type P) not assignable to LHS (of type P) -ResolutionErrors.dfy(1093,6): Error: RHS (of type P) not assignable to LHS (of type P) -ResolutionErrors.dfy(1094,6): Error: RHS (of type P) not assignable to LHS (of type P) -ResolutionErrors.dfy(1099,13): Error: arguments must have the same type (got P and P) -ResolutionErrors.dfy(1100,13): Error: arguments must have the same type (got P and P) -ResolutionErrors.dfy(1101,13): Error: arguments must have the same type (got P and P) -ResolutionErrors.dfy(1124,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(1126,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(1231,26): Error: the type of this variable is underspecified -ResolutionErrors.dfy(1232,31): Error: the type of this variable is underspecified -ResolutionErrors.dfy(1233,29): Error: the type of this variable is underspecified -ResolutionErrors.dfy(1243,34): Error: the type of this variable is underspecified -ResolutionErrors.dfy(1259,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(1260,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(1297,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y) -ResolutionErrors.dfy(1307,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) -ResolutionErrors.dfy(1335,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name) -ResolutionErrors.dfy(1345,29): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(1347,49): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(1347,54): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(1368,11): Error: name of type (X) is used as a variable -ResolutionErrors.dfy(1368,16): Error: name of type (X) is used as a variable -ResolutionErrors.dfy(1369,11): Error: name of module (Y) is used as a variable -ResolutionErrors.dfy(1369,16): Error: name of module (Y) is used as a variable -ResolutionErrors.dfy(1370,11): Error: name of type (X) is used as a variable -ResolutionErrors.dfy(1370,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #type, or a map with domain #type (instead got map) -ResolutionErrors.dfy(1371,11): Error: name of module (Y) is used as a variable -ResolutionErrors.dfy(1371,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #module, or a map with domain #module (instead got map) -ResolutionErrors.dfy(1376,16): Error: name of type (X) is used as a variable -ResolutionErrors.dfy(1376,13): Error: arguments must have the same type (got int and #type) -ResolutionErrors.dfy(1377,16): Error: name of module (Y) is used as a variable -ResolutionErrors.dfy(1377,13): Error: arguments must have the same type (got int and #module) -ResolutionErrors.dfy(1378,4): Error: name of type (X) is used as a variable -ResolutionErrors.dfy(1379,4): Error: name of module (Y) is used as a variable -ResolutionErrors.dfy(1388,11): Error: type of RHS of assign-such-that statement must be boolean (got int) -ResolutionErrors.dfy(1389,9): Error: type of RHS of assign-such-that statement must be boolean (got int) -ResolutionErrors.dfy(1390,13): Error: type of RHS of assign-such-that statement must be boolean (got int) -ResolutionErrors.dfy(1393,15): Error: type of RHS of let-such-that expression must be boolean (got int) -ResolutionErrors.dfy(1436,20): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(1458,18): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(1459,23): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(1460,20): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(1463,21): Error: a while statement used inside a hint is not allowed to have a modifies clause -ResolutionErrors.dfy(1445,24): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(1458,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(1487,18): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(1488,23): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(1489,11): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(1492,21): Error: a while statement used inside a hint is not allowed to have a modifies clause -ResolutionErrors.dfy(1480,24): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(1487,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(1516,20): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(1409,29): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(1411,17): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(1527,16): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(1545,12): Error: trying to break out of more loop levels than there are enclosing loops -ResolutionErrors.dfy(1571,16): Error: ghost fields are allowed only in specification contexts -ResolutionErrors.dfy(1578,9): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(1584,4): Error: non-ghost variable cannot be assigned a value that depends on a ghost -ResolutionErrors.dfy(1601,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(1610,26): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(1618,6): Error: the type of the bound variable 't' could not be determined +ResolutionErrors.dfy(622,23): Error: 'new' is not allowed in ghost contexts +ResolutionErrors.dfy(629,15): Error: 'new' is not allowed in ghost contexts +ResolutionErrors.dfy(638,17): Error: 'new' is not allowed in ghost contexts +ResolutionErrors.dfy(655,14): Error: new allocation not supported in forall statements +ResolutionErrors.dfy(660,11): Error: the body of the enclosing forall statement is not allowed to update heap locations +ResolutionErrors.dfy(660,14): Error: new allocation not allowed in ghost context +ResolutionErrors.dfy(672,21): Error: the type of this variable is underspecified +ResolutionErrors.dfy(712,22): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating +ResolutionErrors.dfy(745,22): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating +ResolutionErrors.dfy(776,19): Error: calls to methods with side-effects are not allowed inside a statement expression +ResolutionErrors.dfy(777,20): Error: wrong number of method result arguments (got 0, expected 1) +ResolutionErrors.dfy(789,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') +ResolutionErrors.dfy(799,4): Error: ghost variables are allowed only in specification contexts +ResolutionErrors.dfy(810,36): Error: ghost variables are allowed only in specification contexts +ResolutionErrors.dfy(819,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') +ResolutionErrors.dfy(833,6): Error: RHS (of type B) not assignable to LHS (of type object) +ResolutionErrors.dfy(834,6): Error: RHS (of type int) not assignable to LHS (of type object) +ResolutionErrors.dfy(835,6): Error: RHS (of type B) not assignable to LHS (of type object) +ResolutionErrors.dfy(840,6): Error: RHS (of type G) not assignable to LHS (of type object) +ResolutionErrors.dfy(841,6): Error: RHS (of type Dt) not assignable to LHS (of type object) +ResolutionErrors.dfy(842,6): Error: RHS (of type CoDt) not assignable to LHS (of type object) +ResolutionErrors.dfy(867,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) +ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) +ResolutionErrors.dfy(885,20): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) +ResolutionErrors.dfy(896,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) +ResolutionErrors.dfy(912,4): Error: LHS of array assignment must denote an array element (found seq) +ResolutionErrors.dfy(913,4): Error: LHS of array assignment must denote an array element (found seq) +ResolutionErrors.dfy(918,10): Error: LHS of assignment must denote a mutable field +ResolutionErrors.dfy(919,10): Error: LHS of assignment must denote a mutable field +ResolutionErrors.dfy(920,9): Error: cannot assign to a range of array elements (try the 'forall' statement) +ResolutionErrors.dfy(921,9): Error: cannot assign to a range of array elements (try the 'forall' statement) +ResolutionErrors.dfy(922,5): Error: cannot assign to a range of array elements (try the 'forall' statement) +ResolutionErrors.dfy(923,5): Error: cannot assign to a range of array elements (try the 'forall' statement) +ResolutionErrors.dfy(1004,11): Error: Wrong number of type arguments (2 instead of 1) passed to array type: array3 +ResolutionErrors.dfy(1005,11): Error: Wrong number of type arguments (2 instead of 1) passed to class: C +ResolutionErrors.dfy(1016,7): Error: Duplicate name of top-level declaration: BadSyn2 +ResolutionErrors.dfy(1013,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List +ResolutionErrors.dfy(1014,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name or declare a module import 'opened?') +ResolutionErrors.dfy(1015,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?') +ResolutionErrors.dfy(1022,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A +ResolutionErrors.dfy(1025,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A +ResolutionErrors.dfy(1029,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A +ResolutionErrors.dfy(1038,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed +ResolutionErrors.dfy(1041,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A +ResolutionErrors.dfy(1046,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A +ResolutionErrors.dfy(1065,21): Error: unresolved identifier: x +ResolutionErrors.dfy(1072,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P +ResolutionErrors.dfy(1084,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name or declare a module import 'opened?') +ResolutionErrors.dfy(1094,6): Error: RHS (of type P) not assignable to LHS (of type P) +ResolutionErrors.dfy(1099,6): Error: RHS (of type P) not assignable to LHS (of type P) +ResolutionErrors.dfy(1104,6): Error: RHS (of type P) not assignable to LHS (of type P) +ResolutionErrors.dfy(1105,6): Error: RHS (of type P) not assignable to LHS (of type P) +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(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(1242,26): Error: the type of this variable is underspecified +ResolutionErrors.dfy(1243,31): Error: the type of this variable is underspecified +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(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) +ResolutionErrors.dfy(1318,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) +ResolutionErrors.dfy(1346,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name) +ResolutionErrors.dfy(1356,29): Error: ghost variables are allowed only in specification contexts +ResolutionErrors.dfy(1358,49): Error: ghost variables are allowed only in specification contexts +ResolutionErrors.dfy(1358,54): Error: ghost variables are allowed only in specification contexts +ResolutionErrors.dfy(1379,11): Error: name of type (X) is used as a variable +ResolutionErrors.dfy(1379,16): Error: name of type (X) is used as a variable +ResolutionErrors.dfy(1380,11): Error: name of module (Y) is used as a variable +ResolutionErrors.dfy(1380,16): Error: name of module (Y) is used as a variable +ResolutionErrors.dfy(1381,11): Error: name of type (X) is used as a variable +ResolutionErrors.dfy(1381,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #type, or a map with domain #type (instead got map) +ResolutionErrors.dfy(1382,11): Error: name of module (Y) is used as a variable +ResolutionErrors.dfy(1382,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #module, or a map with domain #module (instead got map) +ResolutionErrors.dfy(1387,16): Error: name of type (X) is used as a variable +ResolutionErrors.dfy(1387,13): Error: arguments must have the same type (got int and #type) +ResolutionErrors.dfy(1388,16): Error: name of module (Y) is used as a variable +ResolutionErrors.dfy(1388,13): Error: arguments must have the same type (got int and #module) +ResolutionErrors.dfy(1389,4): Error: name of type (X) is used as a variable +ResolutionErrors.dfy(1390,4): Error: name of module (Y) is used as a variable +ResolutionErrors.dfy(1399,11): Error: type of RHS of assign-such-that statement must be boolean (got int) +ResolutionErrors.dfy(1400,9): Error: type of RHS of assign-such-that statement must be boolean (got int) +ResolutionErrors.dfy(1401,13): Error: type of RHS of assign-such-that statement must be boolean (got int) +ResolutionErrors.dfy(1404,15): Error: type of RHS of let-such-that expression must be boolean (got int) +ResolutionErrors.dfy(1447,20): Error: calls to methods with side-effects are not allowed inside a hint +ResolutionErrors.dfy(1469,18): Error: a hint is not allowed to update heap locations +ResolutionErrors.dfy(1470,23): Error: a hint is not allowed to update heap locations +ResolutionErrors.dfy(1471,20): Error: calls to methods with side-effects are not allowed inside a hint +ResolutionErrors.dfy(1474,21): Error: a while statement used inside a hint is not allowed to have a modifies clause +ResolutionErrors.dfy(1456,24): Error: only ghost methods can be called from this context +ResolutionErrors.dfy(1469,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(1498,18): Error: a hint is not allowed to update heap locations +ResolutionErrors.dfy(1499,23): Error: a hint is not allowed to update heap locations +ResolutionErrors.dfy(1500,11): Error: calls to methods with side-effects are not allowed inside a hint +ResolutionErrors.dfy(1503,21): Error: a while statement used inside a hint is not allowed to have a modifies clause +ResolutionErrors.dfy(1491,24): Error: only ghost methods can be called from this context +ResolutionErrors.dfy(1498,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(1527,20): Error: only ghost methods can be called from this context +ResolutionErrors.dfy(1420,29): Error: only ghost methods can be called from this context +ResolutionErrors.dfy(1422,17): Error: calls to methods with side-effects are not allowed inside a hint +ResolutionErrors.dfy(1538,16): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating +ResolutionErrors.dfy(1556,12): Error: trying to break out of more loop levels than there are enclosing loops +ResolutionErrors.dfy(1568,16): Error: ghost fields are allowed only in specification contexts +ResolutionErrors.dfy(1575,9): Error: ghost variables are allowed only in specification contexts +ResolutionErrors.dfy(1581,4): Error: non-ghost variable cannot be assigned a value that depends on a ghost +ResolutionErrors.dfy(1598,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(1607,26): Error: ghost variables are allowed only in specification contexts +ResolutionErrors.dfy(1615,6): Error: the type of the bound variable 't' could not be determined +ResolutionErrors.dfy(1633,15): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) +ResolutionErrors.dfy(1635,10): 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(1660,15): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) +ResolutionErrors.dfy(1662,25): 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) +ResolutionErrors.dfy(1663,35): 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) +ResolutionErrors.dfy(1673,4): Error: 'decreases *' is not allowed on ghost loops +ResolutionErrors.dfy(1677,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) +ResolutionErrors.dfy(1687,4): Error: 'decreases *' is not allowed on ghost loops +ResolutionErrors.dfy(1691,29): 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) ResolutionErrors.dfy(469,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') @@ -144,18 +157,14 @@ ResolutionErrors.dfy(475,14): Error: when allocating an object of type 'YHWH', o ResolutionErrors.dfy(480,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called ResolutionErrors.dfy(481,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called ResolutionErrors.dfy(483,9): Error: class Lamb does not have an anonymous constructor -ResolutionErrors.dfy(850,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int) -ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) -ResolutionErrors.dfy(857,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) -ResolutionErrors.dfy(865,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) -ResolutionErrors.dfy(875,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) -ResolutionErrors.dfy(886,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) -ResolutionErrors.dfy(1042,23): Error: unresolved identifier: x -ResolutionErrors.dfy(1045,20): Error: unresolved identifier: x -ResolutionErrors.dfy(1048,23): Error: unresolved identifier: x -ResolutionErrors.dfy(1050,19): Error: unresolved identifier: x -ResolutionErrors.dfy(1052,19): Error: unresolved identifier: x -ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops +ResolutionErrors.dfy(853,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int) +ResolutionErrors.dfy(857,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) +ResolutionErrors.dfy(1053,23): Error: unresolved identifier: x +ResolutionErrors.dfy(1056,20): Error: unresolved identifier: x +ResolutionErrors.dfy(1059,23): Error: unresolved identifier: x +ResolutionErrors.dfy(1061,19): Error: unresolved identifier: x +ResolutionErrors.dfy(1063,19): Error: unresolved identifier: x +ResolutionErrors.dfy(12,16): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3) ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3) ResolutionErrors.dfy(26,11): Error: array selection requires an array4 (got array) @@ -187,17 +196,17 @@ ResolutionErrors.dfy(416,10): Error: second argument to ==> must be of type bool ResolutionErrors.dfy(421,10): Error: first argument to ==> must be of type bool (instead got int) ResolutionErrors.dfy(421,10): Error: second argument to ==> must be of type bool (instead got int) ResolutionErrors.dfy(580,18): Error: unresolved identifier: w -ResolutionErrors.dfy(683,11): Error: lemmas are not allowed to have modifies clauses -ResolutionErrors.dfy(924,9): Error: unresolved identifier: s -ResolutionErrors.dfy(935,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int)) -ResolutionErrors.dfy(936,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real)) -ResolutionErrors.dfy(942,16): Error: condition is expected to be of type bool, but is int -ResolutionErrors.dfy(943,16): Error: member 3 does not exist in datatype _tuple#3 -ResolutionErrors.dfy(943,26): Error: member x does not exist in datatype _tuple#2 -ResolutionErrors.dfy(966,15): Error: arguments to / must have the same type (got real and int) -ResolutionErrors.dfy(967,10): Error: second argument to % must be of type int (instead got real) -ResolutionErrors.dfy(1112,8): Error: new cannot be applied to a trait -ResolutionErrors.dfy(1133,13): Error: first argument to / must be of numeric type (instead got set) -ResolutionErrors.dfy(1140,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(1155,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating -202 resolution/type errors detected in ResolutionErrors.dfy +ResolutionErrors.dfy(686,11): Error: lemmas are not allowed to have modifies clauses +ResolutionErrors.dfy(935,9): Error: unresolved identifier: s +ResolutionErrors.dfy(946,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int)) +ResolutionErrors.dfy(947,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real)) +ResolutionErrors.dfy(953,16): Error: condition is expected to be of type bool, but is int +ResolutionErrors.dfy(954,16): Error: member 3 does not exist in datatype _tuple#3 +ResolutionErrors.dfy(954,26): Error: member x does not exist in datatype _tuple#2 +ResolutionErrors.dfy(977,15): Error: arguments to / must have the same type (got real and int) +ResolutionErrors.dfy(978,10): Error: second argument to % must be of type int (instead got real) +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 -- cgit v1.2.3