diff --git a/Source/DafnyCore/AST/AstVisitor.cs b/Source/DafnyCore/AST/AstVisitor.cs index ec47429cead..4a699106e75 100644 --- a/Source/DafnyCore/AST/AstVisitor.cs +++ b/Source/DafnyCore/AST/AstVisitor.cs @@ -57,7 +57,7 @@ protected virtual void VisitOneDeclaration(TopLevelDecl decl) { } if (decl is TopLevelDeclWithMembers cl) { - cl.Members.Iter(member => VisitMember(cl, member)); + cl.Members.Iter(VisitMember); } } @@ -89,19 +89,9 @@ private void VisitIterator(IteratorDecl iteratorDecl) { } } - protected virtual void VisitMember(TopLevelDeclWithMembers cl, MemberDecl member) { - if (member is ConstantField constantField) { - var context = GetContext(constantField, false); - VisitAttributes(constantField, constantField.EnclosingModule); - VisitUserProvidedType(constantField.Type, context); - if (constantField.Rhs != null) { - VisitExpression(constantField.Rhs, context); - } - - } else if (member is Field field) { - var context = GetContext(new NoContext(cl.EnclosingModuleDefinition), false); - VisitAttributes(field, cl.EnclosingModuleDefinition); - VisitUserProvidedType(field.Type, context); + public void VisitMember(MemberDecl member) { + if (member is Field field) { + VisitField(field); } else if (member is Function function) { VisitFunction(function); @@ -129,6 +119,18 @@ protected virtual void VisitMember(TopLevelDeclWithMembers cl, MemberDecl member } } + public virtual void VisitField(Field field) { + var enclosingModule = field.EnclosingClass.EnclosingModuleDefinition; + VisitAttributes(field, enclosingModule); + + var context = GetContext(field as IASTVisitorContext ?? new NoContext(enclosingModule), false); + VisitUserProvidedType(field.Type, context); + + if (field is ConstantField { Rhs: { } rhs }) { + VisitExpression(rhs, context); + } + } + public virtual void VisitFunction(Function function) { var context = GetContext(function, false); @@ -260,18 +262,25 @@ protected virtual void VisitExpression(Expression expr, VisitorContext context) // Visit subexpressions expr.SubExpressions.Iter(ee => VisitExpression(ee, context)); + + PostVisitOneExpression(expr, context); } } /// /// Visits the given expression. - /// Returns "true" to request that the caller keeps visiting all user-provided types, subexpressions, and substatements of "expr", and - /// returns "false" to tell the caller not to. + /// Returns "true" to request that the caller + /// - keeps visiting all user-provided types, subexpressions, and substatements of "expr", and + /// - then calls PostVisitOneExpression. + /// Returns "false" to tell the caller not to do those things. /// protected virtual bool VisitOneExpression(Expression expr, VisitorContext context) { return true; } + protected virtual void PostVisitOneExpression(Expression expr, VisitorContext context) { + } + protected virtual void VisitStatement(Statement stmt, VisitorContext context) { if (VisitOneStatement(stmt, context)) { // Visit user-provided types @@ -317,17 +326,24 @@ protected virtual void VisitStatement(Statement stmt, VisitorContext context) { // Visit substatements stmt.SubStatements.Iter(ss => VisitStatement(ss, context)); + + PostVisitOneStatement(stmt, context); } } /// /// Visits the given statement. - /// Returns "true" to request that the caller keeps visiting all user-provided types, subexpressions, and substatements of "stmt", and - /// returns "false" to tell the caller not to. + /// Returns "true" to request that the caller + /// - keeps visiting all user-provided types, subexpressions, and substatements of "stmt", and + /// - then calls PostVisitOneStatement. + /// Returns "false" to tell the caller not to do those things. /// protected virtual bool VisitOneStatement(Statement stmt, VisitorContext context) { return true; } + + protected virtual void PostVisitOneStatement(Statement stmt, VisitorContext context) { + } } } diff --git a/Source/DafnyCore/AST/DafnyAst.cs b/Source/DafnyCore/AST/DafnyAst.cs index 084377d4eac..a335538f323 100644 --- a/Source/DafnyCore/AST/DafnyAst.cs +++ b/Source/DafnyCore/AST/DafnyAst.cs @@ -345,22 +345,21 @@ public static bool Contains(Attributes attrs, string nm) { /// - if the attribute is {:nm true}, then value==true /// - if the attribute is {:nm false}, then value==false /// - if the attribute is anything else, then value returns as whatever it was passed in as. + /// This method does NOT use type information of the attribute arguments, so it can safely + /// be called very early during resolution before types are available and names have been resolved. /// [Pure] public static bool ContainsBool(Attributes attrs, string nm, ref bool value) { Contract.Requires(nm != null); - foreach (var attr in attrs.AsEnumerable()) { - if (attr.Name == nm) { - if (attr.Args.Count == 1) { - var arg = attr.Args[0] as LiteralExpr; - if (arg != null && arg.Value is bool) { - value = (bool)arg.Value; - } - } - return true; - } + var attr = attrs.AsEnumerable().FirstOrDefault(attr => attr.Name == nm); + if (attr == null) { + return false; } - return false; + + if (attr.Args.Count == 1 && attr.Args[0] is LiteralExpr { Value: bool v }) { + value = v; + } + return true; } /// diff --git a/Source/DafnyCore/AST/Printer.cs b/Source/DafnyCore/AST/Printer.cs index fab2e84b852..4112b6bc92f 100644 --- a/Source/DafnyCore/AST/Printer.cs +++ b/Source/DafnyCore/AST/Printer.cs @@ -309,6 +309,7 @@ public void PrintTopLevelDecls(List decls, int indent, List { + private readonly ErrorReporter reporter; + + public BoundsDiscoveryVisitor(ErrorReporter reporter) { + this.reporter = reporter; + } + + public override IASTVisitorContext GetContext(IASTVisitorContext astVisitorContext, bool inFunctionPostcondition) { + return astVisitorContext; + } + + protected override bool VisitOneStatement(Statement stmt, IASTVisitorContext context) { + if (stmt is ForallStmt forallStmt) { + forallStmt.Bounds = DiscoverBestBounds_MultipleVars(forallStmt.BoundVars, forallStmt.Range, true, + ComprehensionExpr.BoundedPool.PoolVirtues.Enumerable); + } else if (stmt is AssignSuchThatStmt assignSuchThatStmt) { + if (assignSuchThatStmt.AssumeToken == null) { + var varLhss = new List(); + foreach (var lhs in assignSuchThatStmt.Lhss) { + var ide = (IdentifierExpr)lhs.Resolved; // successful resolution implies all LHS's are IdentifierExpr's + varLhss.Add(ide.Var); + } + assignSuchThatStmt.Bounds = DiscoverBestBounds_MultipleVars(varLhss, assignSuchThatStmt.Expr, true, + ComprehensionExpr.BoundedPool.PoolVirtues.None); + } + } + + return base.VisitOneStatement(stmt, context); + } + + protected override bool VisitOneExpression(Expression expr, IASTVisitorContext context) { + if (expr is ComprehensionExpr) { + var e = (ComprehensionExpr)expr; + // apply bounds discovery to quantifiers, finite sets, and finite maps + string what = e.WhatKind; + Expression whereToLookForBounds = null; + var polarity = true; + if (e is QuantifierExpr quantifierExpr) { + whereToLookForBounds = quantifierExpr.LogicalBody(); + polarity = quantifierExpr is ExistsExpr; + } else if (e is SetComprehension setComprehension) { + whereToLookForBounds = setComprehension.Range; + } else if (e is MapComprehension) { + whereToLookForBounds = e.Range; + } else { + Contract.Assume(e is LambdaExpr); // otherwise, unexpected ComprehensionExpr + } + if (whereToLookForBounds != null) { + e.Bounds = DiscoverBestBounds_MultipleVars_AllowReordering(e.BoundVars, whereToLookForBounds, polarity, ComprehensionExpr.BoundedPool.PoolVirtues.None); + if (2 <= DafnyOptions.O.Allocated && (context is Function or ConstantField or RedirectingTypeDecl)) { + // functions are not allowed to depend on the set of allocated objects + foreach (var bv in ComprehensionExpr.BoundedPool.MissingBounds(e.BoundVars, e.Bounds, ComprehensionExpr.BoundedPool.PoolVirtues.IndependentOfAlloc)) { + var msgFormat = "a {0} involved in a {3} definition is not allowed to depend on the set of allocated references, but values of '{1}' may contain references"; + if (bv.Type.IsTypeParameter || bv.Type.IsOpaqueType) { + msgFormat += " (perhaps declare its type, '{2}', as '{2}(!new)')"; + } + msgFormat += " (see documentation for 'older' parameters)"; + var declKind = context is RedirectingTypeDecl redir ? redir.WhatKind : ((MemberDecl)context).WhatKind; + reporter.Error(MessageSource.Resolver, e, msgFormat, e.WhatKind, bv.Name, bv.Type, declKind); + } + } + + if ((e as SetComprehension)?.Finite == true || (e as MapComprehension)?.Finite == true) { + // the comprehension had better produce a finite set + if (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 ComprehensionExpr.BoundedPool.MissingBounds(e.BoundVars, e.Bounds, ComprehensionExpr.BoundedPool.PoolVirtues.Finite)) { + reporter.Error(MessageSource.Resolver, e, + "the result of a {0} must be finite, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{1}'", + e.WhatKind, bv.Name); + } + } + } + } + + } + + return base.VisitOneExpression(expr, context); + } + } + /// /// For a list of variables "bvars", returns a list of best bounds, subject to the constraint "requiredVirtues", for each respective variable. /// If no bound matching "requiredVirtues" is found for a variable "v", then the bound for "v" in the returned list is set to "null". diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs index e127392560b..e228384a696 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs @@ -21,6 +21,129 @@ namespace Microsoft.Dafny { public partial class Resolver { + /// + /// There are two rounds of name resolution + type inference. The "initialRound" parameter says which one to do. + /// + void ResolveNamesAndInferTypes(List declarations, bool initialRound) { + foreach (TopLevelDecl topd in declarations) { + Contract.Assert(topd != null); + Contract.Assert(VisibleInScope(topd)); + Contract.Assert(AllTypeConstraints.Count == 0); + Contract.Assert(currentClass == null); + + allTypeParameters.PushMarker(); + ResolveTypeParameters(topd.TypeArgs, !initialRound, topd); + + if (initialRound) { + ResolveNamesAndInferTypesForOneDeclarationInitial(topd); + } else { + ResolveNamesAndInferTypesForOneDeclaration(topd); + } + + allTypeParameters.PopMarker(); + + Contract.Assert(AllTypeConstraints.Count == 0); + Contract.Assert(currentClass == null); + } + } + + /// + /// Assumes type parameters of "topd" have already been pushed. + /// + void ResolveNamesAndInferTypesForOneDeclarationInitial(TopLevelDecl topd) { + if (topd is NewtypeDecl newtypeDecl) { + // this check can be done only after it has been determined that the redirected types do not involve cycles + AddXConstraint(newtypeDecl.tok, "NumericType", newtypeDecl.BaseType, "newtypes must be based on some numeric type (got {0})"); + // type check the constraint, if any + if (newtypeDecl.Var != null) { + Contract.Assert(object.ReferenceEquals(newtypeDecl.Var.Type, newtypeDecl.BaseType)); // follows from NewtypeDecl invariant + Contract.Assert(newtypeDecl.Constraint != null); // follows from NewtypeDecl invariant + + scope.PushMarker(); + scope.AllowInstance = false; + var added = scope.Push(newtypeDecl.Var.Name, newtypeDecl.Var); + Contract.Assert(added == Scope.PushResult.Success); + ResolveExpression(newtypeDecl.Constraint, new ResolutionContext(new CodeContextWrapper(newtypeDecl, true), false)); + Contract.Assert(newtypeDecl.Constraint.Type != null); // follows from postcondition of ResolveExpression + ConstrainTypeExprBool(newtypeDecl.Constraint, "newtype constraint must be of type bool (instead got {0})"); + scope.PopMarker(); + } + SolveAllTypeConstraints(); + + } else if (topd is SubsetTypeDecl subsetTypeDecl) { + // type check the constraint + Contract.Assert(object.ReferenceEquals(subsetTypeDecl.Var.Type, subsetTypeDecl.Rhs)); // follows from SubsetTypeDecl invariant + Contract.Assert(subsetTypeDecl.Constraint != null); // follows from SubsetTypeDecl invariant + scope.PushMarker(); + scope.AllowInstance = false; + var added = scope.Push(subsetTypeDecl.Var.Name, subsetTypeDecl.Var); + Contract.Assert(added == Scope.PushResult.Success); + ResolveExpression(subsetTypeDecl.Constraint, new ResolutionContext(new CodeContextWrapper(subsetTypeDecl, true), false)); + Contract.Assert(subsetTypeDecl.Constraint.Type != null); // follows from postcondition of ResolveExpression + ConstrainTypeExprBool(subsetTypeDecl.Constraint, "subset-type constraint must be of type bool (instead got {0})"); + scope.PopMarker(); + SolveAllTypeConstraints(); + } + + if (topd is TopLevelDeclWithMembers cl) { + ResolveClassMemberBodiesInitial(cl); + } + } + + void ResolveNamesAndInferTypesForOneDeclaration(TopLevelDecl topd) { + if (topd is NewtypeDecl newtypeDecl) { + if (newtypeDecl.Witness != null) { + var codeContext = new CodeContextWrapper(newtypeDecl, newtypeDecl.WitnessKind == SubsetTypeDecl.WKind.Ghost); + scope.PushMarker(); + scope.AllowInstance = false; + ResolveExpression(newtypeDecl.Witness, new ResolutionContext(codeContext, false)); + scope.PopMarker(); + ConstrainSubtypeRelation(newtypeDecl.Var.Type, newtypeDecl.Witness.Type, newtypeDecl.Witness, "witness expression must have type '{0}' (got '{1}')", newtypeDecl.Var.Type, newtypeDecl.Witness.Type); + } + SolveAllTypeConstraints(); + + } else if (topd is SubsetTypeDecl subsetTypeDecl) { + if (subsetTypeDecl.Witness != null) { + var codeContext = new CodeContextWrapper(subsetTypeDecl, subsetTypeDecl.WitnessKind == SubsetTypeDecl.WKind.Ghost); + scope.PushMarker(); + scope.AllowInstance = false; + ResolveExpression(subsetTypeDecl.Witness, new ResolutionContext(codeContext, false)); + scope.PopMarker(); + ConstrainSubtypeRelation(subsetTypeDecl.Var.Type, subsetTypeDecl.Witness.Type, subsetTypeDecl.Witness, + "witness expression must have type '{0}' (got '{1}')", subsetTypeDecl.Var.Type, subsetTypeDecl.Witness.Type); + } + SolveAllTypeConstraints(); + + } else if (topd is IteratorDecl iteratorDecl) { + ResolveIterator(iteratorDecl); + + } else if (topd is DatatypeDecl dt) { + // resolve any default parameters + foreach (var ctor in dt.Ctors) { + scope.PushMarker(); + scope.AllowInstance = false; + ctor.Formals.ForEach(p => scope.Push(p.Name, p)); + ResolveParameterDefaultValues(ctor.Formals, ResolutionContext.FromCodeContext(dt)); + ResolveAttributes(ctor, new ResolutionContext(new NoContext(topd.EnclosingModuleDefinition), false), true); + scope.PopMarker(); + } + } + + if (topd is TopLevelDeclWithMembers cl) { + ResolveClassMemberBodies(cl); + } + + // resolve attributes + scope.PushMarker(); + Contract.Assert(currentClass == null); + scope.AllowInstance = false; + if (topd is IteratorDecl iter) { + iter.Ins.ForEach(p => scope.Push(p.Name, p)); + } + ResolveAttributes(topd, new ResolutionContext(new NoContext(topd.EnclosingModuleDefinition), false), true); + scope.PopMarker(); + } + void EagerAddAssignableConstraint(IToken tok, Type lhs, Type rhs, string errMsgFormat) { Contract.Requires(tok != null); Contract.Requires(lhs != null); @@ -148,10 +271,18 @@ void SolveAllTypeConstraints() { AllXConstraints.Clear(); } - void ResolveAttributes(IAttributeBearingDeclaration attributeHost, ResolutionContext resolutionContext) { + /// + /// Adds type constraints for the expressions in the given attributes. + /// + /// If "solveConstraints" is "true", then the constraints are also solved. In this case, it is assumed on entry that there are no + /// prior type constraints. That is, the only type constraints being solved for are the ones in the given attributes. + /// + void ResolveAttributes(IAttributeBearingDeclaration attributeHost, ResolutionContext resolutionContext, bool solveConstraints = false) { Contract.Requires(resolutionContext != null); Contract.Requires(attributeHost != null); + Contract.Assume(!solveConstraints || AllTypeConstraints.Count == 0); + // order does not matter much for resolution, so resolve them in reverse order foreach (var attr in attributeHost.Attributes.AsEnumerable()) { if (attr is UserSuppliedAttributes) { @@ -161,14 +292,14 @@ void ResolveAttributes(IAttributeBearingDeclaration attributeHost, ResolutionCon if (attr.Args != null) { foreach (var arg in attr.Args) { Contract.Assert(arg != null); - int prevErrors = reporter.Count(ErrorLevel.Error); ResolveExpression(arg, resolutionContext); - if (prevErrors == reporter.Count(ErrorLevel.Error)) { - CheckTypeInference(arg, resolutionContext.CodeContext); - } } } } + + if (solveConstraints) { + SolveAllTypeConstraints(); + } } /// @@ -1668,7 +1799,7 @@ public bool Confirm(Resolver resolver, bool fullstrength, out bool convertedInto case "Assignable": { Contract.Assert(t == t.Normalize()); // it's already been normalized above var u = Types[1].NormalizeExpand(); - if (CheckTypeInference_Visitor.IsDetermined(t) && + if (CheckTypeInferenceVisitor.IsDetermined(t) && (fullstrength || !ProxyWithNoSubTypeConstraint(u, resolver) || (u is TypeProxy @@ -1676,7 +1807,7 @@ public bool Confirm(Resolver resolver, bool fullstrength, out bool convertedInto && (t0constrained.IsNonNullRefType || t0constrained.AsSubsetType != null) && resolver.HasApplicableNullableRefTypeConstraint(new HashSet() { (TypeProxy)u })))) { // This is the best case. We convert Assignable(t, u) to the subtype constraint base(t) :> u. - if (CheckTypeInference_Visitor.IsDetermined(u) && t.IsSubtypeOf(u, false, true) && t.IsRefType) { + if (CheckTypeInferenceVisitor.IsDetermined(u) && t.IsSubtypeOf(u, false, true) && t.IsRefType) { // But we also allow cases where the rhs is a proper supertype of the lhs, and let the verifier // determine whether the rhs is provably an instance of the lhs. resolver.ConstrainAssignable((NonProxyType)u, (NonProxyType)t, errorMsg, out moreXConstraints, fullstrength); @@ -3084,6 +3215,35 @@ private bool Reaches_aux(Type t, TypeProxy proxy, int direction, HashSet + /// Assumes type parameters have already been pushed, and that all types in class members have been resolved + /// + void ResolveClassMemberBodiesInitial(TopLevelDeclWithMembers cl) { + Contract.Requires(cl != null); + Contract.Requires(currentClass == null); + Contract.Requires(AllTypeConstraints.Count == 0); + Contract.Ensures(currentClass == null); + Contract.Ensures(AllTypeConstraints.Count == 0); + + currentClass = cl; + foreach (MemberDecl member in cl.Members) { + Contract.Assert(VisibleInScope(member)); + if (member is ConstantField { Rhs: { } } constantField) { + var resolutionContext = new ResolutionContext(constantField, false); + scope.PushMarker(); + if (constantField.IsStatic || currentClass == null || !currentClass.AcceptThis) { + scope.AllowInstance = false; + } + ResolveExpression(constantField.Rhs, resolutionContext); + scope.PopMarker(); + AddAssignableConstraint(constantField.tok, constantField.Type, constantField.Rhs.Type, + "type for constant '" + constantField.Name + "' is '{0}', but its initialization value type is '{1}'"); + SolveAllTypeConstraints(); + } + } + currentClass = null; + } + /// /// Assumes type parameters have already been pushed, and that all types in class members have been resolved /// @@ -3097,38 +3257,38 @@ void ResolveClassMemberBodies(TopLevelDeclWithMembers cl) { currentClass = cl; foreach (MemberDecl member in cl.Members) { Contract.Assert(VisibleInScope(member)); - if (member is ConstantField) { - // don't do anything here, because const fields have already been resolved - } else if (member is Field) { + if (member is Field) { var resolutionContext = new ResolutionContext(new NoContext(currentClass.EnclosingModuleDefinition), false); - ResolveAttributes(member, resolutionContext); - } else if (member is Function) { - var f = (Function)member; + scope.PushMarker(); + if (member.IsStatic) { + scope.AllowInstance = false; + } + ResolveAttributes(member, resolutionContext, true); + scope.PopMarker(); + + } else if (member is Function function) { var ec = reporter.Count(ErrorLevel.Error); allTypeParameters.PushMarker(); - ResolveTypeParameters(f.TypeArgs, false, f); - ResolveFunction(f); + ResolveTypeParameters(function.TypeArgs, false, function); + ResolveFunction(function); allTypeParameters.PopMarker(); - if (f is ExtremePredicate ef && ef.PrefixPredicate != null && ec == reporter.Count(ErrorLevel.Error)) { - var ff = ef.PrefixPredicate; + if (function is ExtremePredicate { PrefixPredicate: { } prefixPredicate } && ec == reporter.Count(ErrorLevel.Error)) { allTypeParameters.PushMarker(); - ResolveTypeParameters(ff.TypeArgs, false, ff); - ResolveFunction(ff); + ResolveTypeParameters(prefixPredicate.TypeArgs, false, prefixPredicate); + ResolveFunction(prefixPredicate); allTypeParameters.PopMarker(); } - } else if (member is Method) { - var m = (Method)member; + } else if (member is Method method) { var ec = reporter.Count(ErrorLevel.Error); allTypeParameters.PushMarker(); - ResolveTypeParameters(m.TypeArgs, false, m); - ResolveMethod(m); + ResolveTypeParameters(method.TypeArgs, false, method); + ResolveMethod(method); allTypeParameters.PopMarker(); - if (m is ExtremeLemma em && em.PrefixLemma != null && ec == reporter.Count(ErrorLevel.Error)) { - var mm = em.PrefixLemma; + if (method is ExtremeLemma { PrefixLemma: { } prefixLemma } && ec == reporter.Count(ErrorLevel.Error)) { allTypeParameters.PushMarker(); - ResolveTypeParameters(mm.TypeArgs, false, mm); - ResolveMethod(mm); + ResolveTypeParameters(prefixLemma.TypeArgs, false, prefixLemma); + ResolveMethod(prefixLemma); allTypeParameters.PopMarker(); } @@ -3208,32 +3368,24 @@ void ResolveFunction(Function f) { Contract.Requires(AllTypeConstraints.Count == 0); Contract.Ensures(AllTypeConstraints.Count == 0); + // make note of the warnShadowing attribute bool warnShadowingOption = DafnyOptions.O.WarnShadowing; // save the original warnShadowing value bool warnShadowing = false; + if (Attributes.ContainsBool(f.Attributes, "warnShadowing", ref warnShadowing)) { + DafnyOptions.O.WarnShadowing = warnShadowing; // set the value according to the attribute + } scope.PushMarker(); if (f.IsStatic) { scope.AllowInstance = false; } - if (f.IsGhost) { - foreach (TypeParameter p in f.TypeArgs) { - if (p.SupportsEquality) { - reporter.Warning(MessageSource.Resolver, p.tok, - $"type parameter {p.Name} of ghost {f.WhatKind} {f.Name} is declared (==), which is unnecessary because the {f.WhatKind} doesn't contain any compiled code"); - } - } - } - foreach (Formal p in f.Formals) { scope.Push(p.Name, p); } - ResolveAttributes(f, new ResolutionContext(f, false)); - // take care of the warnShadowing attribute - if (Attributes.ContainsBool(f.Attributes, "warnShadowing", ref warnShadowing)) { - DafnyOptions.O.WarnShadowing = warnShadowing; // set the value according to the attribute - } + ResolveParameterDefaultValues(f.Formals, ResolutionContext.FromCodeContext(f)); + foreach (AttributedExpression e in f.Req) { ResolveAttributes(e, new ResolutionContext(f, f is TwoStateFunction)); Expression r = e.E; @@ -3244,53 +3396,55 @@ void ResolveFunction(Function f) { foreach (FrameExpression fr in f.Reads) { ResolveFrameExpressionTopLevel(fr, FrameExpressionUse.Reads, f); } + + scope.PushMarker(); + if (f.Result != null) { + scope.Push(f.Result.Name, f.Result); // function return only visible in post-conditions (and in function attributes) + } foreach (AttributedExpression e in f.Ens) { Expression r = e.E; - if (f.Result != null) { - scope.PushMarker(); - scope.Push(f.Result.Name, f.Result); // function return only visible in post-conditions - } ResolveAttributes(e, new ResolutionContext(f, f is TwoStateFunction)); ResolveExpression(r, new ResolutionContext(f, f is TwoStateFunction) with { InFunctionPostcondition = true }); Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression ConstrainTypeExprBool(r, "Postcondition must be a boolean (got {0})"); - if (f.Result != null) { - scope.PopMarker(); - } } + scope.PopMarker(); // function result name + ResolveAttributes(f.Decreases, new ResolutionContext(f, f is TwoStateFunction)); foreach (Expression r in f.Decreases.Expressions) { ResolveExpression(r, new ResolutionContext(f, f is TwoStateFunction)); // any type is fine } - SolveAllTypeConstraints(); + SolveAllTypeConstraints(); // solve type constraints in the specification - if (f.ByMethodBody != null) { - // The following conditions are assured by the parser and other callers of the Function constructor - Contract.Assert(f.Body != null); - Contract.Assert(!f.IsGhost); - } if (f.Body != null) { - var prevErrorCount = reporter.Count(ErrorLevel.Error); ResolveExpression(f.Body, new ResolutionContext(f, f is TwoStateFunction)); Contract.Assert(f.Body.Type != null); // follows from postcondition of ResolveExpression AddAssignableConstraint(f.tok, f.ResultType, f.Body.Type, "Function body type mismatch (expected {0}, got {1})"); SolveAllTypeConstraints(); + } - if (f.ByMethodBody != null) { - var method = f.ByMethodDecl; - if (method != null) { - ResolveMethod(method); - } else { - // method should have been filled in by now, - // unless there was a function by method and a method of the same name - // but then this error must have been reported. - Contract.Assert(reporter.ErrorCount > 0); - } - } + scope.PushMarker(); + if (f.Result != null) { + scope.Push(f.Result.Name, f.Result); // function return only visible in post-conditions (and in function attributes) } + ResolveAttributes(f, new ResolutionContext(f, f is TwoStateFunction), true); + scope.PopMarker(); // function result name - scope.PopMarker(); + scope.PopMarker(); // formals + + if (f.ByMethodBody != null) { + Contract.Assert(f.Body != null && !f.IsGhost); // assured by the parser and other callers of the Function constructor + var method = f.ByMethodDecl; + if (method != null) { + ResolveMethod(method); + } else { + // method should have been filled in by now, + // unless there was a function by method and a method of the same name + // but then this error must have been reported. + Contract.Assert(reporter.ErrorCount > 0); + } + } DafnyOptions.O.WarnShadowing = warnShadowingOption; // restore the original warnShadowing value } @@ -3344,22 +3498,13 @@ void ResolveMethod(Method m) { try { currentMethod = m; + // make note of the warnShadowing attribute bool warnShadowingOption = DafnyOptions.O.WarnShadowing; // save the original warnShadowing value bool warnShadowing = false; - // take care of the warnShadowing attribute if (Attributes.ContainsBool(m.Attributes, "warnShadowing", ref warnShadowing)) { DafnyOptions.O.WarnShadowing = warnShadowing; // set the value according to the attribute } - if (m.IsGhost) { - foreach (TypeParameter p in m.TypeArgs) { - if (p.SupportsEquality) { - reporter.Warning(MessageSource.Resolver, p.tok, - $"type parameter {p.Name} of ghost {m.WhatKind} {m.Name} is declared (==), which is unnecessary because the {m.WhatKind} doesn't contain any compiled code"); - } - } - } - // Add in-parameters to the scope, but don't care about any duplication errors, since they have already been reported scope.PushMarker(); if (m.IsStatic || m is Constructor) { @@ -3420,7 +3565,7 @@ void ResolveMethod(Method m) { Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypeExprBool(e.E, "Postcondition must be a boolean (got {0})"); } - SolveAllTypeConstraints(); + SolveAllTypeConstraints(); // solve type constraints for specification // Resolve body if (m.Body != null) { @@ -3448,11 +3593,12 @@ void ResolveMethod(Method m) { } // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for greatest lemmas) - ResolveAttributes(m, new ResolutionContext(m, m is TwoStateLemma)); + ResolveAttributes(m, new ResolutionContext(m, m is TwoStateLemma), true); DafnyOptions.O.WarnShadowing = warnShadowingOption; // restore the original warnShadowing value scope.PopMarker(); // for the out-parameters and outermost-level locals scope.PopMarker(); // for the in-parameters + } finally { currentMethod = null; @@ -3481,7 +3627,7 @@ void ResolveIterator(IteratorDecl iter) { // these fields; so, with no further ado, here we go ResolveAttributes(iter.Decreases, new ResolutionContext(iter, false)); Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count); - for (int i = 0; i < iter.Decreases.Expressions.Count; i++) { + for (var i = 0; i < iter.Decreases.Expressions.Count; i++) { var e = iter.Decreases.Expressions[i]; ResolveExpression(e, new ResolutionContext(iter, false)); // any type is fine, but associate this type with the corresponding _decreases field @@ -3531,8 +3677,6 @@ void ResolveIterator(IteratorDecl iter) { } SolveAllTypeConstraints(); - ResolveAttributes(iter, new ResolutionContext(iter, false)); - var postSpecErrorCount = reporter.Count(ErrorLevel.Error); // Resolve body @@ -3768,6 +3912,287 @@ void ResolveCallStmt(CallStmt s, ResolutionContext resolutionContext, Type recei } } + /// + /// Resolve the actual arguments given in "bindings". Then, check that there is exactly one + /// actual for each formal, and impose assignable constraints. + /// "typeMap" is applied to the type of each formal. + /// This method should be called only once. That is, bindings.arguments is required to be null on entry to this method. + /// + void ResolveActualParameters(ActualBindings bindings, List formals, IToken callTok, object context, ResolutionContext resolutionContext, + Dictionary typeMap, Expression/*?*/ receiver) { + Contract.Requires(bindings != null); + Contract.Requires(formals != null); + Contract.Requires(callTok != null); + Contract.Requires(context is Method || context is Function || context is DatatypeCtor || context is ArrowType); + Contract.Requires(typeMap != null); + Contract.Requires(!bindings.WasResolved); + + string whatKind; + string name; + if (context is Method cMethod) { + whatKind = cMethod.WhatKind; + name = $"{whatKind} '{cMethod.Name}'"; + } else if (context is Function cFunction) { + whatKind = cFunction.WhatKind; + name = $"{whatKind} '{cFunction.Name}'"; + } else if (context is DatatypeCtor cCtor) { + whatKind = "datatype constructor"; + name = $"{whatKind} '{cCtor.Name}'"; + } else { + var cArrowType = (ArrowType)context; + whatKind = "function application"; + name = $"function type '{cArrowType}'"; + } + + // If all arguments are passed positionally, use simple error messages that talk about the count of arguments. + var onlyPositionalArguments = bindings.ArgumentBindings.TrueForAll(binding => binding.FormalParameterName == null); + var simpleErrorReported = false; + if (onlyPositionalArguments) { + var requiredParametersCount = formals.Count(f => f.DefaultValue == null); + var actualsCounts = bindings.ArgumentBindings.Count; + if (requiredParametersCount <= actualsCounts && actualsCounts <= formals.Count) { + // the situation is plausible + } else if (requiredParametersCount == formals.Count) { + // this is the common, classical case of no default parameter values; generate a straightforward error message + reporter.Error(MessageSource.Resolver, callTok, $"wrong number of arguments ({name} expects {formals.Count}, got {actualsCounts})"); + simpleErrorReported = true; + } else if (actualsCounts < requiredParametersCount) { + reporter.Error(MessageSource.Resolver, callTok, $"wrong number of arguments ({name} expects at least {requiredParametersCount}, got {actualsCounts})"); + simpleErrorReported = true; + } else { + reporter.Error(MessageSource.Resolver, callTok, $"wrong number of arguments ({name} expects at most {formals.Count}, got {actualsCounts})"); + simpleErrorReported = true; + } + } + + // resolve given arguments and populate the "namesToActuals" map + var namesToActuals = new Dictionary(); + formals.ForEach(f => namesToActuals.Add(f.Name, null)); // a name mapping to "null" says it hasn't been filled in yet + var stillAcceptingPositionalArguments = true; + var bindingIndex = 0; + foreach (var binding in bindings.ArgumentBindings) { + var arg = binding.Actual; + // insert the actual into "namesToActuals" under an appropriate name, unless there is an error + if (binding.FormalParameterName != null) { + var pname = binding.FormalParameterName.val; + stillAcceptingPositionalArguments = false; + if (!namesToActuals.TryGetValue(pname, out var b)) { + reporter.Error(MessageSource.Resolver, binding.FormalParameterName, $"the binding named '{pname}' does not correspond to any formal parameter"); + } else if (b == null) { + // all is good + namesToActuals[pname] = binding; + } else if (b.FormalParameterName == null) { + reporter.Error(MessageSource.Resolver, binding.FormalParameterName, $"the parameter named '{pname}' is already given positionally"); + } else { + reporter.Error(MessageSource.Resolver, binding.FormalParameterName, $"duplicate binding for parameter name '{pname}'"); + } + } else if (!stillAcceptingPositionalArguments) { + reporter.Error(MessageSource.Resolver, arg.tok, "a positional argument is not allowed to follow named arguments"); + } else if (bindingIndex < formals.Count) { + // use the name of formal corresponding to this positional argument, unless the parameter is named-only + var formal = formals[bindingIndex]; + var pname = formal.Name; + if (formal.IsNameOnly) { + reporter.Error(MessageSource.Resolver, arg.tok, + $"nameonly parameter '{pname}' must be passed using a name binding; it cannot be passed positionally"); + } + Contract.Assert(namesToActuals[pname] == null); // we expect this, since we've only filled parameters positionally so far + namesToActuals[pname] = binding; + } else { + // too many positional arguments + if (onlyPositionalArguments) { + // error was reported before the "foreach" loop + Contract.Assert(simpleErrorReported); + } else if (formals.Count < bindingIndex) { + // error was reported on a previous iteration of this "foreach" loop + } else { + reporter.Error(MessageSource.Resolver, callTok, + $"wrong number of arguments ({name} expects {formals.Count}, got {bindings.ArgumentBindings.Count})"); + } + } + + // resolve argument + ResolveExpression(arg, resolutionContext); + bindingIndex++; + } + + var actuals = new List(); + var formalIndex = 0; + var substMap = new Dictionary(); + foreach (var formal in formals) { + var b = namesToActuals[formal.Name]; + if (b != null) { + actuals.Add(b.Actual); + substMap.Add(formal, b.Actual); + var what = GetLocationInformation(formal, + bindings.ArgumentBindings.Count(), bindings.ArgumentBindings.IndexOf(b), + whatKind + (context is Method ? " in-parameter" : " parameter")); + + AddAssignableConstraint( + callTok, formal.Type.Subst(typeMap), b.Actual.Type, + $"incorrect argument type {what} (expected {{0}}, found {{1}})"); + } else if (formal.DefaultValue != null) { + // Note, in the following line, "substMap" is passed in, but it hasn't been fully filled in until the + // end of this foreach loop. Still, that's soon enough, because DefaultValueExpression won't use it + // until FillInDefaultValueExpressions at the end of Pass 1 of the Resolver. + var n = new DefaultValueExpression(callTok, formal, receiver, substMap, typeMap); + allDefaultValueExpressions.Add(n); + actuals.Add(n); + substMap.Add(formal, n); + } else { + // parameter has no value + if (onlyPositionalArguments) { + // a simple error message has already been reported + Contract.Assert(simpleErrorReported); + } else { + var formalDescription = whatKind + (context is Method ? " in-parameter" : " parameter"); + var nameWithIndex = formal.HasName && formal is not ImplicitFormal ? "'" + formal.Name + "'" : ""; + if (formals.Count > 1 || nameWithIndex == "") { + nameWithIndex += nameWithIndex == "" ? "" : " "; + nameWithIndex += $"at index {formalIndex}"; + } + var message = $"{formalDescription} {nameWithIndex} requires an argument of type {formal.Type}"; + reporter.Error(MessageSource.Resolver, callTok, message); + } + } + formalIndex++; + } + + bindings.AcceptArgumentExpressionsAsExactParameterList(actuals); + } + + private static string GetLocationInformation(Formal parameter, int bindingCount, int bindingIndex, string formalDescription) { + var displayName = parameter.HasName && parameter is not ImplicitFormal; + var description = ""; + if (bindingCount > 1) { + description += $"at index {bindingIndex} "; + } + + description += $"for {formalDescription}"; + + if (displayName) { + description += $" '{parameter.Name}'"; + } + + return description; + } + + /// + /// To resolve "id" in expression "E . id", do: + /// * If E denotes a module name M: + /// 0. Member of module M: sub-module (including submodules of imports), class, datatype, etc. + /// (if two imported types have the same name, an error message is produced here) + /// 1. Static member of M._default denoting an async task type + /// (Note that in contrast to ResolveNameSegment_Type, imported modules, etc. are ignored) + /// * If E denotes a type: + /// 2. a. Member of that type denoting an async task type, or: + /// b. If allowDanglingDotName: + /// Return the type "E" and the given "expr", letting the caller try to make sense of the final dot-name. + /// + /// Note: 1 and 2a are not used now, but they will be of interest when async task types are supported. + /// + ResolveTypeReturn ResolveDotSuffix_Type(ExprDotName expr, ResolutionContext resolutionContext, bool allowDanglingDotName, ResolveTypeOption option, List defaultTypeArguments) { + Contract.Requires(expr != null); + Contract.Requires(!expr.WasResolved()); + Contract.Requires(expr.Lhs is NameSegment || expr.Lhs is ExprDotName); + Contract.Requires(resolutionContext != null); + Contract.Ensures(Contract.Result() == null || allowDanglingDotName); + + // resolve the LHS expression + if (expr.Lhs is NameSegment) { + ResolveNameSegment_Type((NameSegment)expr.Lhs, resolutionContext, option, defaultTypeArguments); + } else { + ResolveDotSuffix_Type((ExprDotName)expr.Lhs, resolutionContext, false, option, defaultTypeArguments); + } + + if (expr.OptTypeArguments != null) { + foreach (var ty in expr.OptTypeArguments) { + ResolveType(expr.tok, ty, resolutionContext, option, defaultTypeArguments); + } + } + + Expression r = null; // the resolved expression, if successful + + var lhs = expr.Lhs.Resolved; + if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Module) { + var ri = (Resolver_IdentifierExpr)lhs; + var sig = ((ModuleDecl)ri.Decl).AccessibleSignature(useCompileSignatures); + sig = GetSignature(sig); + // For 0: + TopLevelDecl decl; + + if (sig.TopLevels.TryGetValue(expr.SuffixName, out decl)) { + // ----- 0. Member of the specified module + if (decl is AmbiguousTopLevelDecl) { + var ad = (AmbiguousTopLevelDecl)decl; + reporter.Error(MessageSource.Resolver, expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", expr.SuffixName, ad.ModuleNames()); + } else { + // We have found a module name or a type name. We create a temporary expression that will never be seen by the compiler + // or verifier, just to have a placeholder where we can recorded what we have found. + r = CreateResolver_IdentifierExpr(expr.tok, expr.SuffixName, expr.OptTypeArguments, decl); + } +#if ASYNC_TASK_TYPES + } else if (sig.StaticMembers.TryGetValue(expr.SuffixName, out member)) { + // ----- 1. static member of the specified module + Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default + if (ReallyAmbiguousThing(ref member)) { + reporter.Error(MessageSource.Resolver, expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1} (try qualifying the member name with the module name)", expr.SuffixName, ((AmbiguousMemberDecl)member).ModuleNames()); + } else { + var receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass); + r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.resolutionContext, allowMethodCall); + } +#endif + } else { + reporter.Error(MessageSource.Resolver, expr.tok, "module '{0}' does not declare a type '{1}'", ri.Decl.Name, expr.SuffixName); + } + + } else if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Type) { + var ri = (Resolver_IdentifierExpr)lhs; + // ----- 2. Look up name in type + var ty = new UserDefinedType(ri.tok, ri.Decl.Name, ri.Decl, ri.TypeArgs); + if (allowDanglingDotName && ty.IsRefType) { + return new ResolveTypeReturn(ty, expr); + } + if (r == null) { + reporter.Error(MessageSource.Resolver, expr.tok, "member '{0}' does not exist in type '{1}' or cannot be part of type name", expr.SuffixName, ri.Decl.Name); + } + } + + if (r == null) { + // an error has been reported above; we won't fill in .ResolvedExpression, but we still must fill in .Type + expr.Type = new InferredTypeProxy(); + } else { + expr.ResolvedExpression = r; + expr.Type = r.Type; + } + return null; + } + + Resolver_IdentifierExpr CreateResolver_IdentifierExpr(IToken tok, string name, List optTypeArguments, TopLevelDecl decl) { + Contract.Requires(tok != null); + Contract.Requires(name != null); + Contract.Requires(decl != null); + Contract.Ensures(Contract.Result() != null); + + if (!moduleInfo.IsAbstract) { + if (decl is ModuleDecl md && md.Signature.IsAbstract) { + reporter.Error(MessageSource.Resolver, tok, "a compiled module is not allowed to use an abstract module ({0})", decl.Name); + } + } + var n = optTypeArguments == null ? 0 : optTypeArguments.Count; + if (optTypeArguments != null) { + // type arguments were supplied; they must be equal in number to those expected + if (n != decl.TypeArgs.Count) { + reporter.Error(MessageSource.Resolver, tok, "Wrong number of type arguments ({0} instead of {1}) passed to {2}: {3}", n, decl.TypeArgs.Count, decl.WhatKind, name); + } + } + List tpArgs = new List(); + for (int i = 0; i < decl.TypeArgs.Count; i++) { + tpArgs.Add(i < n ? optTypeArguments[i] : new InferredTypeProxy()); + } + return new Resolver_IdentifierExpr(tok, decl, tpArgs); + } + private void ResolveAssignSuchThatStmt(AssignSuchThatStmt s, ResolutionContext resolutionContext) { Contract.Requires(s != null); Contract.Requires(resolutionContext != null); @@ -4614,10 +5039,19 @@ private void ResolveLoopSpecificationComponents(List invar } } + /// + /// Resolves the default-valued expression for each formal in "formals". + /// Solves the resulting type constraints. + /// Assumes these are the only type constraints to be solved. + /// + /// Reports an error for any cyclic dependency among the default-value expressions of the formals. + /// void ResolveParameterDefaultValues(List formals, ResolutionContext resolutionContext) { Contract.Requires(formals != null); Contract.Requires(resolutionContext != null); + Contract.Assume(AllTypeConstraints.Count == 0); + var dependencies = new Graph(); var allowMoreRequiredParameters = true; var allowNamelessParameters = true; @@ -6277,6 +6711,37 @@ Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List + /// Check whether the name we just resolved may have been resolved differently if we didn't allow member `M.M` of + /// module `M` to shadow `M` when the user writes `import opened M`. Raising an error in that case allowed us to + /// change the behavior of `import opened` without silently changing the meaning of existing programs. + /// (https://github.com/dafny-lang/dafny/issues/1996) + /// + /// Note the extra care for the constructor case, which is needed because the constructors of datatype `M.M` are + /// exposed through both `M` and `M.M`, without ambiguity. + /// + private void CheckForAmbiguityInShadowedImportedModule(ModuleDecl moduleDecl, string name, + IToken tok, bool useCompileSignatures, bool isLastNameSegment) { + if (moduleDecl != null && NameConflictsWithModuleContents(moduleDecl, name, useCompileSignatures, isLastNameSegment)) { + reporter.Error(MessageSource.Resolver, tok, + "Reference to member '{0}' is ambiguous: name '{1}' shadows an import-opened module of the same name, and " + + "both have a member '{0}'. To solve this issue, give a different name to the imported module using " + + "`import opened XYZ = ...` instead of `import opened ...`.", + name, moduleDecl.Name); + } + } + + private bool NameConflictsWithModuleContents(ModuleDecl moduleDecl, string name, bool useCompileSignatures, bool isLastNameSegment) { + var sig = GetSignature(moduleDecl.AccessibleSignature(useCompileSignatures)); + return ( + (isLastNameSegment + && sig.Ctors.GetValueOrDefault(name) is { Item1: var constructor, Item2: var ambiguous } + && !ambiguous && constructor.EnclosingDatatype.Name != moduleDecl.Name) + || sig.TopLevels.ContainsKey(name) + || sig.StaticMembers.ContainsKey(name) + ); + } + Expression ResolveExprDotCall(IToken tok, Expression receiver, Type receiverTypeBound/*?*/, MemberDecl member, List args, List optTypeArguments, ResolutionContext resolutionContext, bool allowMethodCall) { Contract.Requires(tok != null); diff --git a/Source/DafnyCore/Resolver/Resolver.cs b/Source/DafnyCore/Resolver/Resolver.cs index 56768ed91df..02825ff3e79 100644 --- a/Source/DafnyCore/Resolver/Resolver.cs +++ b/Source/DafnyCore/Resolver/Resolver.cs @@ -468,8 +468,8 @@ public void ResolveProgram(Program prog) { ResolveType(d.tok, d.Rhs, d, ResolveTypeOptionEnum.AllowPrefix, d.TypeArgs); allTypeParameters.PopMarker(); } - - ResolveTopLevelDecls_Core(systemModuleClassesWithNonNullTypes, new Graph(), new Graph()); + ResolveTopLevelDecls_Core(ModuleDefinition.AllDeclarationsAndNonNullTypeDecls(systemModuleClassesWithNonNullTypes).ToList(), + new Graph(), new Graph()); foreach (var rewriter in rewriters) { rewriter.PreResolve(prog); @@ -1035,13 +1035,18 @@ private bool ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, bo ResolveOpenedImports(moduleInfo, m, useCompileSignatures, this); // opened imports do not persist var datatypeDependencies = new Graph(); var codatatypeDependencies = new Graph(); + var allDeclarations = ModuleDefinition.AllDeclarationsAndNonNullTypeDecls(m.TopLevelDecls).ToList(); int prevErrorCount = reporter.Count(ErrorLevel.Error); - ResolveTopLevelDecls_Signatures(m, sig, m.TopLevelDecls, datatypeDependencies, codatatypeDependencies); + ResolveTopLevelDecls_Signatures(m, sig, allDeclarations, datatypeDependencies, codatatypeDependencies); Contract.Assert(AllTypeConstraints.Count == 0); // signature resolution does not add any type constraints - ResolveAttributes(m, new ResolutionContext(new NoContext(m.EnclosingModule), false)); // Must follow ResolveTopLevelDecls_Signatures, in case attributes refer to members - SolveAllTypeConstraints(); // solve any type constraints entailed by the attributes + + scope.PushMarker(); + scope.AllowInstance = false; + ResolveAttributes(m, new ResolutionContext(new NoContext(m.EnclosingModule), false), true); // Must follow ResolveTopLevelDecls_Signatures, in case attributes refer to members + scope.PopMarker(); + if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { - ResolveTopLevelDecls_Core(m.TopLevelDecls, datatypeDependencies, codatatypeDependencies, isAnExport); + ResolveTopLevelDecls_Core(allDeclarations, datatypeDependencies, codatatypeDependencies, isAnExport); } Type.PopScope(moduleInfo.VisibilityScope); @@ -2572,7 +2577,7 @@ public void ResolveTopLevelDecls_Signatures(ModuleDefinition def, ModuleSignatur }*/ var typeRedirectionDependencies = new Graph(); // this concerns the type directions, not their constraints (which are checked for cyclic dependencies later) - foreach (TopLevelDecl d in ModuleDefinition.AllDeclarationsAndNonNullTypeDecls(declarations)) { + foreach (TopLevelDecl d in declarations) { Contract.Assert(d != null); allTypeParameters.PushMarker(); ResolveTypeParameters(d.TypeArgs, true, d); @@ -2670,270 +2675,103 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, int prevErrorCount = reporter.Count(ErrorLevel.Error); // ---------------------------------- Pass 0 ---------------------------------- - // This pass resolves names, introduces (and may solve) type constraints, and - // builds the module's call graph. - // For 'newtype' and subset-type declarations, it also checks that all types were fully - // determined. + // This pass: + // * resolves names, introduces (and may solve) type constraints + // * checks that all types were properly inferred + // * fills in .ResolvedOp fields + // * perform substitution for DefaultValueExpression's // ---------------------------------------------------------------------------- - // Resolve the meat of classes and iterators, the definitions of type synonyms, and the type parameters of all top-level type declarations - // In the first two loops below, resolve the newtype/subset-type declarations and their constraint clauses and const definitions, including - // filling in .ResolvedOp fields. This is needed for the resolution of the other declarations, because those other declarations may invoke - // DiscoverBounds, which looks at the .Constraint or .Rhs field of any such types involved. - // The third loop resolves the other declarations. It also resolves any witness expressions of newtype/subset-type declarations. - foreach (TopLevelDecl topd in declarations) { - Contract.Assert(topd != null); - Contract.Assert(VisibleInScope(topd)); - TopLevelDecl d = topd is ClassDecl ? ((ClassDecl)topd).NonNullTypeDecl : topd; - if (d is NewtypeDecl) { - var dd = (NewtypeDecl)d; - ResolveAttributes(d, new ResolutionContext(new NoContext(d.EnclosingModuleDefinition), false)); - // this check can be done only after it has been determined that the redirected types do not involve cycles - AddXConstraint(dd.tok, "NumericType", dd.BaseType, "newtypes must be based on some numeric type (got {0})"); - // type check the constraint, if any - if (dd.Var == null) { - SolveAllTypeConstraints(); - } else { - Contract.Assert(object.ReferenceEquals(dd.Var.Type, dd.BaseType)); // follows from NewtypeDecl invariant - Contract.Assert(dd.Constraint != null); // follows from NewtypeDecl invariant + // Resolve all names and infer types. These two are done together, because name resolution depends on having type information + // and type inference depends on having resolved names. + // The task is first performed for (the constraints of) newtype declarations, (the constraints of) subset type declarations, and + // (the right-hand sides of) const declarations, because type resolution sometimes needs to know the base type of newtypes and subset types + // and needs to know the type of const fields. Doing these declarations increases the chances the right information will be provided + // in time. + // Once the task is done for these newtype/subset-type/const parts, the task continues with everything else. + ResolveNamesAndInferTypes(declarations, true); + ResolveNamesAndInferTypes(declarations, false); + + // Check that all types have been determined. During this process, fill in all .ResolvedOp fields. + if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { + var checkTypeInferenceVisitor = new CheckTypeInferenceVisitor(this); + checkTypeInferenceVisitor.VisitDeclarations(declarations); + } - scope.PushMarker(); - var added = scope.Push(dd.Var.Name, dd.Var); - Contract.Assert(added == Scope.PushResult.Success); - ResolveExpression(dd.Constraint, new ResolutionContext(new CodeContextWrapper(dd, true), false)); - Contract.Assert(dd.Constraint.Type != null); // follows from postcondition of ResolveExpression - ConstrainTypeExprBool(dd.Constraint, "newtype constraint must be of type bool (instead got {0})"); - SolveAllTypeConstraints(); - 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); - } - scope.PopMarker(); - } + // Substitute for DefaultValueExpression's + FillInDefaultValueExpressions(); - } else if (d is SubsetTypeDecl) { - var dd = (SubsetTypeDecl)d; - allTypeParameters.PushMarker(); - ResolveTypeParameters(d.TypeArgs, false, d); - ResolveAttributes(d, new ResolutionContext(new NoContext(d.EnclosingModuleDefinition), false)); - // type check the constraint - Contract.Assert(object.ReferenceEquals(dd.Var.Type, dd.Rhs)); // follows from SubsetTypeDecl invariant - Contract.Assert(dd.Constraint != null); // follows from SubsetTypeDecl invariant - scope.PushMarker(); - scope.AllowInstance = false; - var added = scope.Push(dd.Var.Name, dd.Var); - Contract.Assert(added == Scope.PushResult.Success); - ResolveExpression(dd.Constraint, new ResolutionContext(new CodeContextWrapper(dd, true), false)); - Contract.Assert(dd.Constraint.Type != null); // follows from postcondition of ResolveExpression - ConstrainTypeExprBool(dd.Constraint, "subset-type constraint must be of type bool (instead got {0})"); - SolveAllTypeConstraints(); - if (!CheckTypeInference_Visitor.IsDetermined(dd.Rhs.NormalizeExpand())) { - reporter.Error(MessageSource.Resolver, dd.tok, "subset type's base type is not fully determined; add an explicit type for '{0}'", dd.Var.Name); - } - dd.ConstraintIsCompilable = ExpressionTester.CheckIsCompilable(null, dd.Constraint, new CodeContextWrapper(dd, true)); - dd.CheckedIfConstraintIsCompilable = true; + // ---------------------------------- Pass 1 ---------------------------------- + // This pass does the following: + // * discovers bounds + // * builds the module's call graph. + // * compute and checks ghosts (this makes use of bounds discovery, as done above) + // * for newtypes, figure out native types + // * for datatypes, check that shared destructors are in agreement in ghost matters + // * for functions and methods, determine tail recursion + // ---------------------------------------------------------------------------- - scope.PopMarker(); - allTypeParameters.PopMarker(); - } - if (topd is TopLevelDeclWithMembers) { - var cl = (TopLevelDeclWithMembers)topd; - currentClass = cl; - foreach (var member in cl.Members) { - Contract.Assert(VisibleInScope(member)); - if (member is ConstantField) { - var field = (ConstantField)member; - var resolutionContext = new ResolutionContext(field, false); - ResolveAttributes(field, resolutionContext); - // Resolve the value expression - if (field.Rhs != null) { - var ec = reporter.Count(ErrorLevel.Error); - scope.PushMarker(); - if (currentClass == null || !currentClass.AcceptThis) { - scope.AllowInstance = false; - } - ResolveExpression(field.Rhs, resolutionContext); - scope.PopMarker(); - AddAssignableConstraint(field.tok, field.Type, field.Rhs.Type, "type for constant '" + field.Name + "' is '{0}', but its initialization value type is '{1}'"); - } - SolveAllTypeConstraints(); - if (!CheckTypeInference_Visitor.IsDetermined(field.Type.NormalizeExpand())) { - reporter.Error(MessageSource.Resolver, field.tok, "const field's type is not fully determined"); - } - } - } - currentClass = null; - } - } - Contract.Assert(AllTypeConstraints.Count == 0); + // Discover bounds. These are needed later to determine if certain things are ghost or compiled, and thus this should + // be done before building the call graph. if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { - // Check type inference, which also discovers bounds, in newtype/subset-type constraints and const declarations - foreach (TopLevelDecl topd in declarations) { - TopLevelDecl d = topd is ClassDecl ? ((ClassDecl)topd).NonNullTypeDecl : topd; - if (d is RedirectingTypeDecl dd && dd.Constraint != null) { - CheckTypeInference(dd.Constraint, dd); - } - if (topd is TopLevelDeclWithMembers cl) { - foreach (var member in cl.Members) { - if (member is ConstantField field && field.Rhs != null) { - CheckTypeInference(field.Rhs, field); - if (!field.IsGhost) { - ExpressionTester.CheckIsCompilable(this, field.Rhs, field); - } - } - } - } - } - } - // Now, we're ready for the other declarations, along with any witness clauses of newtype/subset-type declarations. - foreach (TopLevelDecl d in declarations) { - Contract.Assert(AllTypeConstraints.Count == 0); - allTypeParameters.PushMarker(); - ResolveTypeParameters(d.TypeArgs, false, d); - if (d is NewtypeDecl || d is SubsetTypeDecl) { - // NewTypeDecl's and SubsetTypeDecl's were already processed in the loop above, except for any witness clauses - var dd = (RedirectingTypeDecl)d; - if (dd.Witness != null) { - var prevErrCnt = reporter.Count(ErrorLevel.Error); - var codeContext = new CodeContextWrapper(dd, dd.WitnessKind == SubsetTypeDecl.WKind.Ghost); - scope.PushMarker(); - if (d is not TopLevelDeclWithMembers topLevelDecl || !topLevelDecl.AcceptThis) { - scope.AllowInstance = false; - } - ResolveExpression(dd.Witness, new ResolutionContext(codeContext, false)); - scope.PopMarker(); - ConstrainSubtypeRelation(dd.Var.Type, dd.Witness.Type, dd.Witness, "witness expression must have type '{0}' (got '{1}')", dd.Var.Type, dd.Witness.Type); - SolveAllTypeConstraints(); - if (reporter.Count(ErrorLevel.Error) == prevErrCnt) { - CheckTypeInference(dd.Witness, dd); - } - if (reporter.Count(ErrorLevel.Error) == prevErrCnt && dd.WitnessKind == SubsetTypeDecl.WKind.Compiled) { - ExpressionTester.CheckIsCompilable(this, dd.Witness, codeContext); - } - } - if (d is TopLevelDeclWithMembers dm) { - ResolveClassMemberBodies(dm); - } - } else { - if (!(d is IteratorDecl)) { - // Note, attributes of iterators are resolved by ResolvedIterator, after registering any names in the iterator signature - ResolveAttributes(d, new ResolutionContext(new NoContext(d.EnclosingModuleDefinition), false)); - } - if (d is IteratorDecl) { - var iter = (IteratorDecl)d; - ResolveIterator(iter); - ResolveClassMemberBodies(iter); // resolve the automatically generated members - } else if (d is DatatypeDecl) { - var dt = (DatatypeDecl)d; - foreach (var ctor in dt.Ctors) { - ResolveAttributes(ctor, new ResolutionContext(new NoContext(d.EnclosingModuleDefinition), false)); - } - // resolve any default parameters - foreach (var ctor in dt.Ctors) { - scope.PushMarker(); - scope.AllowInstance = false; - ctor.Formals.ForEach(p => scope.Push(p.Name, p)); - ResolveParameterDefaultValues(ctor.Formals, ResolutionContext.FromCodeContext(dt)); - scope.PopMarker(); - } - // resolve members - ResolveClassMemberBodies(dt); - } else if (d is TopLevelDeclWithMembers) { - var dd = (TopLevelDeclWithMembers)d; - ResolveClassMemberBodies(dd); - } - } - allTypeParameters.PopMarker(); + var boundsDiscoveryVisitor = new BoundsDiscoveryVisitor(reporter); + boundsDiscoveryVisitor.VisitDeclarations(declarations); } if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { CallGraphBuilder.Build(declarations, reporter); } - // ---------------------------------- Pass 1 ---------------------------------- - // This pass: - // * checks that type inference was able to determine all types - // * check that shared destructors in datatypes are in agreement - // * fills in the .ResolvedOp field of binary expressions - // * performs substitution for DefaultValueExpression's - // * discovers bounds for: - // - forall statements - // - set comprehensions - // - map comprehensions - // - quantifier expressions - // - assign-such-that statements - // - compilable let-such-that expressions - // - newtype constraints - // - subset-type constraints - // For each statement body that it successfully typed, this pass also: - // * computes ghost interests - // * determines/checks tail-recursion. - // ---------------------------------------------------------------------------- - + // Compute ghost interests, figure out native types, check agreement among datatype destructors, and determine tail calls. if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { - // Check that type inference went well everywhere; this will also fill in the .ResolvedOp field in binary expressions - // Also, for each datatype, check that shared destructors are in agreement foreach (TopLevelDecl d in declarations) { if (d is IteratorDecl) { var iter = (IteratorDecl)d; - var prevErrCnt = reporter.Count(ErrorLevel.Error); - foreach (var formal in iter.Ins) { - if (formal.DefaultValue != null) { - CheckTypeInference(formal.DefaultValue, iter); - } - } - iter.Members.Iter(CheckTypeInference_Member); - if (prevErrCnt == reporter.Count(ErrorLevel.Error)) { - iter.SubExpressions.Iter(e => CheckExpression(e, this, iter)); - } - ResolveParameterDefaultValues_Pass1(iter.Ins, iter); + iter.SubExpressions.Iter(e => CheckExpression(e, this, iter)); if (iter.Body != null) { - CheckTypeInference(iter.Body, iter); - if (prevErrCnt == reporter.Count(ErrorLevel.Error)) { - ComputeGhostInterest(iter.Body, false, null, iter); - CheckExpression(iter.Body, this, iter); + ComputeGhostInterest(iter.Body, false, null, iter); + CheckExpression(iter.Body, this, iter); + } + + } else if (d is SubsetTypeDecl subsetTypeDecl) { + Contract.Assert(subsetTypeDecl.Constraint != null); + CheckExpression(subsetTypeDecl.Constraint, this, new CodeContextWrapper(subsetTypeDecl, true)); + subsetTypeDecl.ConstraintIsCompilable = + ExpressionTester.CheckIsCompilable(null, subsetTypeDecl.Constraint, new CodeContextWrapper(subsetTypeDecl, true)); + subsetTypeDecl.CheckedIfConstraintIsCompilable = true; + + if (subsetTypeDecl.Witness != null) { + CheckExpression(subsetTypeDecl.Witness, this, new CodeContextWrapper(subsetTypeDecl, subsetTypeDecl.WitnessKind == SubsetTypeDecl.WKind.Ghost)); + if (subsetTypeDecl.WitnessKind == SubsetTypeDecl.WKind.Compiled) { + var codeContext = new CodeContextWrapper(subsetTypeDecl, subsetTypeDecl.WitnessKind == SubsetTypeDecl.WKind.Ghost); + ExpressionTester.CheckIsCompilable(this, subsetTypeDecl.Witness, codeContext); } } - } else if (d is ClassDecl) { - var dd = (ClassDecl)d; - ResolveClassMembers_Pass1(dd); - } else if (d is SubsetTypeDecl) { - var dd = (SubsetTypeDecl)d; - Contract.Assert(dd.Constraint != null); - CheckExpression(dd.Constraint, this, new CodeContextWrapper(dd, true)); - if (dd.Witness != null) { - CheckExpression(dd.Witness, this, new CodeContextWrapper(dd, dd.WitnessKind == SubsetTypeDecl.WKind.Ghost)); - } - } else if (d is NewtypeDecl) { - var dd = (NewtypeDecl)d; - if (dd.Var != null) { - Contract.Assert(dd.Constraint != null); - CheckExpression(dd.Constraint, this, new CodeContextWrapper(dd, true)); - if (dd.Witness != null) { - CheckExpression(dd.Witness, this, new CodeContextWrapper(dd, dd.WitnessKind == SubsetTypeDecl.WKind.Ghost)); + + } else if (d is NewtypeDecl newtypeDecl) { + if (newtypeDecl.Var != null) { + Contract.Assert(newtypeDecl.Constraint != null); + CheckExpression(newtypeDecl.Constraint, this, new CodeContextWrapper(newtypeDecl, true)); + if (newtypeDecl.Witness != null) { + CheckExpression(newtypeDecl.Witness, this, new CodeContextWrapper(newtypeDecl, newtypeDecl.WitnessKind == SubsetTypeDecl.WKind.Ghost)); } } - FigureOutNativeType(dd); - ResolveClassMembers_Pass1(dd); + if (newtypeDecl.Witness != null && newtypeDecl.WitnessKind == SubsetTypeDecl.WKind.Compiled) { + var codeContext = new CodeContextWrapper(newtypeDecl, newtypeDecl.WitnessKind == SubsetTypeDecl.WKind.Ghost); + ExpressionTester.CheckIsCompilable(this, newtypeDecl.Witness, codeContext); + } + + FigureOutNativeType(newtypeDecl); + } else if (d is DatatypeDecl) { var dd = (DatatypeDecl)d; - foreach (var ctor in dd.Ctors) { - foreach (var formal in ctor.Formals) { - if (formal.DefaultValue != null) { - CheckTypeInference(formal.DefaultValue, dd); - } - } - } foreach (var member in classMembers[dd].Values) { var dtor = member as DatatypeDestructor; if (dtor != null) { var rolemodel = dtor.CorrespondingFormals[0]; for (int i = 1; i < dtor.CorrespondingFormals.Count; i++) { var other = dtor.CorrespondingFormals[i]; - if (!Type.Equal_Improved(rolemodel.Type, other.Type)) { - reporter.Error(MessageSource.Resolver, other, - "shared destructors must have the same type, but '{0}' has type '{1}' in constructor '{2}' and type '{3}' in constructor '{4}'", - rolemodel.Name, rolemodel.Type, dtor.EnclosingCtors[0].Name, other.Type, dtor.EnclosingCtors[i].Name); - } else if (rolemodel.IsGhost != other.IsGhost) { + if (rolemodel.IsGhost != other.IsGhost) { reporter.Error(MessageSource.Resolver, other, "shared destructors must agree on whether or not they are ghost, but '{0}' is {1} in constructor '{2}' and {3} in constructor '{4}'", rolemodel.Name, @@ -2944,18 +2782,16 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, } } foreach (var ctor in dd.Ctors) { - ResolveParameterDefaultValues_Pass1(ctor.Formals, dd); + CheckParameterDefaultValuesAreCompilable(ctor.Formals, dd); } - ResolveClassMembers_Pass1(dd); - } else if (d is OpaqueTypeDecl) { - var dd = (OpaqueTypeDecl)d; - ResolveClassMembers_Pass1(dd); + } + + if (d is TopLevelDeclWithMembers cl) { + ResolveClassMembers_Pass1(cl); } } } - FillInDefaultValueExpressions(); - // ---------------------------------- Pass 2 ---------------------------------- // This pass fills in various additional information. // * Subset type in comprehensions have a compilable constraint @@ -3105,7 +2941,7 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, ResolveMethod(prefixLemma); allTypeParameters.PopMarker(); currentClass = null; - CheckTypeInference_Member(prefixLemma); + new CheckTypeInferenceVisitor(this).VisitMethod(prefixLemma); CallGraphBuilder.VisitMethod(prefixLemma, reporter); } } @@ -3226,12 +3062,17 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, if (d is IteratorDecl) { var iter = (IteratorDecl)d; var done = false; - foreach (var tp in iter.TypeArgs) { + var nonnullIter = iter.NonNullTypeDecl; + Contract.Assert(nonnullIter.TypeArgs.Count == iter.TypeArgs.Count); + for (var i = 0; i < iter.TypeArgs.Count; i++) { + var tp = iter.TypeArgs[i]; + var correspondingNonnullIterTypeParameter = nonnullIter.TypeArgs[i]; if (tp.Characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) { // here's our chance to infer the need for equality support foreach (var p in iter.Ins) { if (InferRequiredEqualitySupport(tp, p.Type)) { tp.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; + correspondingNonnullIterTypeParameter.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; done = true; break; } @@ -3243,6 +3084,7 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, if (InferRequiredEqualitySupport(tp, p.Type)) { tp.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; + correspondingNonnullIterTypeParameter.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; break; } } @@ -3445,8 +3287,7 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, } } - if (d is RedirectingTypeDecl) { - var dd = (RedirectingTypeDecl)d; + if (d is RedirectingTypeDecl dd) { if (d.EnclosingModuleDefinition.CallGraph.GetSCCSize(dd) != 1) { var r = d.EnclosingModuleDefinition.CallGraph.GetSCCRepresentative(dd); if (cycleErrorHasBeenReported.Contains(r)) { @@ -3582,28 +3423,28 @@ private void CheckIsOkayWithoutRHS(ConstantField f) { private void ResolveClassMembers_Pass1(TopLevelDeclWithMembers cl) { foreach (var member in cl.Members) { var prevErrCnt = reporter.Count(ErrorLevel.Error); - CheckTypeInference_Member(member); if (prevErrCnt == reporter.Count(ErrorLevel.Error)) { - if (member is Method) { - var m = (Method)member; - ResolveParameterDefaultValues_Pass1(m.Ins, m); - if (m.Body != null) { - ComputeGhostInterest(m.Body, m.IsGhost, m.IsLemmaLike ? "a " + m.WhatKind : null, m); - CheckExpression(m.Body, this, m); - new TailRecursion(reporter).DetermineTailRecursion(m); - } - } else if (member is Function) { - var f = (Function)member; - ResolveParameterDefaultValues_Pass1(f.Formals, f); - if (f.ByMethodBody == null) { - if (!f.IsGhost && f.Body != null) { - ExpressionTester.CheckIsCompilable(this, f.Body, f); + if (member is Method method) { + CheckForUnnecessaryEqualitySupportDeclarations(method, method.TypeArgs); + CheckParameterDefaultValuesAreCompilable(method.Ins, method); + if (method.Body != null) { + ComputeGhostInterest(method.Body, method.IsGhost, method.IsLemmaLike ? "a " + method.WhatKind : null, method); + CheckExpression(method.Body, this, method); + new TailRecursion(reporter).DetermineTailRecursion(method); + } + + } else if (member is Function function) { + CheckForUnnecessaryEqualitySupportDeclarations(function, function.TypeArgs); + CheckParameterDefaultValuesAreCompilable(function.Formals, function); + if (function.ByMethodBody == null) { + if (!function.IsGhost && function.Body != null) { + ExpressionTester.CheckIsCompilable(this, function.Body, function); } - if (f.Body != null) { - new TailRecursion(reporter).DetermineTailRecursion(f); + if (function.Body != null) { + new TailRecursion(reporter).DetermineTailRecursion(function); } } else { - var m = f.ByMethodDecl; + var m = function.ByMethodDecl; if (m != null) { Contract.Assert(!m.IsGhost); ComputeGhostInterest(m.Body, false, null, m); @@ -3615,7 +3456,11 @@ private void ResolveClassMembers_Pass1(TopLevelDeclWithMembers cl) { Contract.Assert(reporter.ErrorCount > 0); } } + + } else if (member is ConstantField field && field.Rhs != null && !field.IsGhost) { + ExpressionTester.CheckIsCompilable(this, field.Rhs, field); } + if (prevErrCnt == reporter.Count(ErrorLevel.Error) && member is ICodeContext) { member.SubExpressions.Iter(e => CheckExpression(e, this, (ICodeContext)member)); } @@ -3623,10 +3468,19 @@ private void ResolveClassMembers_Pass1(TopLevelDeclWithMembers cl) { } } + void CheckForUnnecessaryEqualitySupportDeclarations(MemberDecl member, List typeParameters) { + if (member.IsGhost) { + foreach (var p in typeParameters.Where(p => p.SupportsEquality)) { + reporter.Warning(MessageSource.Resolver, p.tok, + $"type parameter {p.Name} of ghost {member.WhatKind} {member.Name} is declared (==), which is unnecessary because the {member.WhatKind} doesn't contain any compiled code"); + } + } + } + /// /// Check that default-value expressions are compilable, for non-ghost formals. /// - void ResolveParameterDefaultValues_Pass1(List formals, ICodeContext codeContext) { + void CheckParameterDefaultValuesAreCompilable(List formals, ICodeContext codeContext) { Contract.Requires(formals != null); foreach (var formal in formals.Where(f => f.DefaultValue != null)) { @@ -8466,318 +8320,6 @@ void ResolveCasePattern(CasePattern pat, Type sourceType, ResolutionCont } } - Resolver_IdentifierExpr CreateResolver_IdentifierExpr(IToken tok, string name, List optTypeArguments, TopLevelDecl decl) { - Contract.Requires(tok != null); - Contract.Requires(name != null); - Contract.Requires(decl != null); - Contract.Ensures(Contract.Result() != null); - - if (!moduleInfo.IsAbstract) { - if (decl is ModuleDecl md && md.Signature.IsAbstract) { - reporter.Error(MessageSource.Resolver, tok, "a compiled module is not allowed to use an abstract module ({0})", decl.Name); - } - } - var n = optTypeArguments == null ? 0 : optTypeArguments.Count; - if (optTypeArguments != null) { - // type arguments were supplied; they must be equal in number to those expected - if (n != decl.TypeArgs.Count) { - reporter.Error(MessageSource.Resolver, tok, "Wrong number of type arguments ({0} instead of {1}) passed to {2}: {3}", n, decl.TypeArgs.Count, decl.WhatKind, name); - } - } - List tpArgs = new List(); - for (int i = 0; i < decl.TypeArgs.Count; i++) { - tpArgs.Add(i < n ? optTypeArguments[i] : new InferredTypeProxy()); - } - return new Resolver_IdentifierExpr(tok, decl, tpArgs); - } - - /// - /// Check whether the name we just resolved may have been resolved differently if we didn't allow member `M.M` of - /// module `M` to shadow `M` when the user writes `import opened M`. Raising an error in that case allowed us to - /// change the behavior of `import opened` without silently changing the meaning of existing programs. - /// (https://github.com/dafny-lang/dafny/issues/1996) - /// - /// Note the extra care for the constructor case, which is needed because the constructors of datatype `M.M` are - /// exposed through both `M` and `M.M`, without ambiguity. - /// - private void CheckForAmbiguityInShadowedImportedModule(ModuleDecl moduleDecl, string name, - IToken tok, bool useCompileSignatures, bool isLastNameSegment) { - if (moduleDecl != null && NameConflictsWithModuleContents(moduleDecl, name, useCompileSignatures, isLastNameSegment)) { - reporter.Error(MessageSource.Resolver, tok, - "Reference to member '{0}' is ambiguous: name '{1}' shadows an import-opened module of the same name, and " - + "both have a member '{0}'. To solve this issue, give a different name to the imported module using " - + "`import opened XYZ = ...` instead of `import opened ...`.", - name, moduleDecl.Name); - } - } - - private bool NameConflictsWithModuleContents(ModuleDecl moduleDecl, string name, bool useCompileSignatures, bool isLastNameSegment) { - var sig = GetSignature(moduleDecl.AccessibleSignature(useCompileSignatures)); - return ( - (isLastNameSegment - && sig.Ctors.GetValueOrDefault(name) is { Item1: var constructor, Item2: var ambiguous } - && !ambiguous && constructor.EnclosingDatatype.Name != moduleDecl.Name) - || sig.TopLevels.ContainsKey(name) - || sig.StaticMembers.ContainsKey(name) - ); - } - - /// - /// To resolve "id" in expression "E . id", do: - /// * If E denotes a module name M: - /// 0. Member of module M: sub-module (including submodules of imports), class, datatype, etc. - /// (if two imported types have the same name, an error message is produced here) - /// 1. Static member of M._default denoting an async task type - /// (Note that in contrast to ResolveNameSegment_Type, imported modules, etc. are ignored) - /// * If E denotes a type: - /// 2. a. Member of that type denoting an async task type, or: - /// b. If allowDanglingDotName: - /// Return the type "E" and the given "expr", letting the caller try to make sense of the final dot-name. - /// - /// Note: 1 and 2a are not used now, but they will be of interest when async task types are supported. - /// - ResolveTypeReturn ResolveDotSuffix_Type(ExprDotName expr, ResolutionContext resolutionContext, bool allowDanglingDotName, ResolveTypeOption option, List defaultTypeArguments) { - Contract.Requires(expr != null); - Contract.Requires(!expr.WasResolved()); - Contract.Requires(expr.Lhs is NameSegment || expr.Lhs is ExprDotName); - Contract.Requires(resolutionContext != null); - Contract.Ensures(Contract.Result() == null || allowDanglingDotName); - - // resolve the LHS expression - if (expr.Lhs is NameSegment) { - ResolveNameSegment_Type((NameSegment)expr.Lhs, resolutionContext, option, defaultTypeArguments); - } else { - ResolveDotSuffix_Type((ExprDotName)expr.Lhs, resolutionContext, false, option, defaultTypeArguments); - } - - if (expr.OptTypeArguments != null) { - foreach (var ty in expr.OptTypeArguments) { - ResolveType(expr.tok, ty, resolutionContext, option, defaultTypeArguments); - } - } - - Expression r = null; // the resolved expression, if successful - - var lhs = expr.Lhs.Resolved; - if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Module) { - var ri = (Resolver_IdentifierExpr)lhs; - var sig = ((ModuleDecl)ri.Decl).AccessibleSignature(useCompileSignatures); - sig = GetSignature(sig); - // For 0: - TopLevelDecl decl; - - if (sig.TopLevels.TryGetValue(expr.SuffixName, out decl)) { - // ----- 0. Member of the specified module - if (decl is AmbiguousTopLevelDecl) { - var ad = (AmbiguousTopLevelDecl)decl; - reporter.Error(MessageSource.Resolver, expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", expr.SuffixName, ad.ModuleNames()); - } else { - // We have found a module name or a type name. We create a temporary expression that will never be seen by the compiler - // or verifier, just to have a placeholder where we can recorded what we have found. - r = CreateResolver_IdentifierExpr(expr.tok, expr.SuffixName, expr.OptTypeArguments, decl); - } -#if ASYNC_TASK_TYPES - } else if (sig.StaticMembers.TryGetValue(expr.SuffixName, out member)) { - // ----- 1. static member of the specified module - Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default - if (ReallyAmbiguousThing(ref member)) { - reporter.Error(MessageSource.Resolver, expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1} (try qualifying the member name with the module name)", expr.SuffixName, ((AmbiguousMemberDecl)member).ModuleNames()); - } else { - var receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass); - r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.resolutionContext, allowMethodCall); - } -#endif - } else { - reporter.Error(MessageSource.Resolver, expr.tok, "module '{0}' does not declare a type '{1}'", ri.Decl.Name, expr.SuffixName); - } - - } else if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Type) { - var ri = (Resolver_IdentifierExpr)lhs; - // ----- 2. Look up name in type - var ty = new UserDefinedType(ri.tok, ri.Decl.Name, ri.Decl, ri.TypeArgs); - if (allowDanglingDotName && ty.IsRefType) { - return new ResolveTypeReturn(ty, expr); - } - if (r == null) { - reporter.Error(MessageSource.Resolver, expr.tok, "member '{0}' does not exist in type '{1}' or cannot be part of type name", expr.SuffixName, ri.Decl.Name); - } - } - - if (r == null) { - // an error has been reported above; we won't fill in .ResolvedExpression, but we still must fill in .Type - expr.Type = new InferredTypeProxy(); - } else { - expr.ResolvedExpression = r; - expr.Type = r.Type; - } - return null; - } - - /// - /// Resolve the actual arguments given in "bindings". Then, check that there is exactly one - /// actual for each formal, and impose assignable constraints. - /// "typeMap" is applied to the type of each formal. - /// This method should be called only once. That is, bindings.arguments is required to be null on entry to this method. - /// - void ResolveActualParameters(ActualBindings bindings, List formals, IToken callTok, object context, ResolutionContext resolutionContext, - Dictionary typeMap, Expression/*?*/ receiver) { - Contract.Requires(bindings != null); - Contract.Requires(formals != null); - Contract.Requires(callTok != null); - Contract.Requires(context is Method || context is Function || context is DatatypeCtor || context is ArrowType); - Contract.Requires(typeMap != null); - Contract.Requires(!bindings.WasResolved); - - string whatKind; - string name; - if (context is Method cMethod) { - whatKind = cMethod.WhatKind; - name = $"{whatKind} '{cMethod.Name}'"; - } else if (context is Function cFunction) { - whatKind = cFunction.WhatKind; - name = $"{whatKind} '{cFunction.Name}'"; - } else if (context is DatatypeCtor cCtor) { - whatKind = "datatype constructor"; - name = $"{whatKind} '{cCtor.Name}'"; - } else { - var cArrowType = (ArrowType)context; - whatKind = "function application"; - name = $"function type '{cArrowType}'"; - } - - // If all arguments are passed positionally, use simple error messages that talk about the count of arguments. - var onlyPositionalArguments = bindings.ArgumentBindings.TrueForAll(binding => binding.FormalParameterName == null); - var simpleErrorReported = false; - if (onlyPositionalArguments) { - var requiredParametersCount = formals.Count(f => f.DefaultValue == null); - var actualsCounts = bindings.ArgumentBindings.Count; - if (requiredParametersCount <= actualsCounts && actualsCounts <= formals.Count) { - // the situation is plausible - } else if (requiredParametersCount == formals.Count) { - // this is the common, classical case of no default parameter values; generate a straightforward error message - reporter.Error(MessageSource.Resolver, callTok, $"wrong number of arguments ({name} expects {formals.Count}, got {actualsCounts})"); - simpleErrorReported = true; - } else if (actualsCounts < requiredParametersCount) { - reporter.Error(MessageSource.Resolver, callTok, $"wrong number of arguments ({name} expects at least {requiredParametersCount}, got {actualsCounts})"); - simpleErrorReported = true; - } else { - reporter.Error(MessageSource.Resolver, callTok, $"wrong number of arguments ({name} expects at most {formals.Count}, got {actualsCounts})"); - simpleErrorReported = true; - } - } - - // resolve given arguments and populate the "namesToActuals" map - var namesToActuals = new Dictionary(); - formals.ForEach(f => namesToActuals.Add(f.Name, null)); // a name mapping to "null" says it hasn't been filled in yet - var stillAcceptingPositionalArguments = true; - var bindingIndex = 0; - foreach (var binding in bindings.ArgumentBindings) { - var arg = binding.Actual; - // insert the actual into "namesToActuals" under an appropriate name, unless there is an error - if (binding.FormalParameterName != null) { - var pname = binding.FormalParameterName.val; - stillAcceptingPositionalArguments = false; - if (!namesToActuals.TryGetValue(pname, out var b)) { - reporter.Error(MessageSource.Resolver, binding.FormalParameterName, $"the binding named '{pname}' does not correspond to any formal parameter"); - } else if (b == null) { - // all is good - namesToActuals[pname] = binding; - } else if (b.FormalParameterName == null) { - reporter.Error(MessageSource.Resolver, binding.FormalParameterName, $"the parameter named '{pname}' is already given positionally"); - } else { - reporter.Error(MessageSource.Resolver, binding.FormalParameterName, $"duplicate binding for parameter name '{pname}'"); - } - } else if (!stillAcceptingPositionalArguments) { - reporter.Error(MessageSource.Resolver, arg.tok, "a positional argument is not allowed to follow named arguments"); - } else if (bindingIndex < formals.Count) { - // use the name of formal corresponding to this positional argument, unless the parameter is named-only - var formal = formals[bindingIndex]; - var pname = formal.Name; - if (formal.IsNameOnly) { - reporter.Error(MessageSource.Resolver, arg.tok, - $"nameonly parameter '{pname}' must be passed using a name binding; it cannot be passed positionally"); - } - Contract.Assert(namesToActuals[pname] == null); // we expect this, since we've only filled parameters positionally so far - namesToActuals[pname] = binding; - } else { - // too many positional arguments - if (onlyPositionalArguments) { - // error was reported before the "foreach" loop - Contract.Assert(simpleErrorReported); - } else if (formals.Count < bindingIndex) { - // error was reported on a previous iteration of this "foreach" loop - } else { - reporter.Error(MessageSource.Resolver, callTok, - $"wrong number of arguments ({name} expects {formals.Count}, got {bindings.ArgumentBindings.Count})"); - } - } - - // resolve argument - ResolveExpression(arg, resolutionContext); - bindingIndex++; - } - - var actuals = new List(); - var formalIndex = 0; - var substMap = new Dictionary(); - foreach (var formal in formals) { - var b = namesToActuals[formal.Name]; - if (b != null) { - actuals.Add(b.Actual); - substMap.Add(formal, b.Actual); - var what = GetLocationInformation(formal, - bindings.ArgumentBindings.Count(), bindings.ArgumentBindings.IndexOf(b), - whatKind + (context is Method ? " in-parameter" : " parameter")); - - AddAssignableConstraint( - callTok, formal.Type.Subst(typeMap), b.Actual.Type, - $"incorrect argument type {what} (expected {{0}}, found {{1}})"); - } else if (formal.DefaultValue != null) { - // Note, in the following line, "substMap" is passed in, but it hasn't been fully filled in until the - // end of this foreach loop. Still, that's soon enough, because DefaultValueExpression won't use it - // until FillInDefaultValueExpressions at the end of Pass 1 of the Resolver. - var n = new DefaultValueExpression(callTok, formal, receiver, substMap, typeMap); - allDefaultValueExpressions.Add(n); - actuals.Add(n); - substMap.Add(formal, n); - } else { - // parameter has no value - if (onlyPositionalArguments) { - // a simple error message has already been reported - Contract.Assert(simpleErrorReported); - } else { - var formalDescription = whatKind + (context is Method ? " in-parameter" : " parameter"); - var nameWithIndex = formal.HasName && formal is not ImplicitFormal ? "'" + formal.Name + "'" : ""; - if (formals.Count > 1 || nameWithIndex == "") { - nameWithIndex += nameWithIndex == "" ? "" : " "; - nameWithIndex += $"at index {formalIndex}"; - } - var message = $"{formalDescription} {nameWithIndex} requires an argument of type {formal.Type}"; - reporter.Error(MessageSource.Resolver, callTok, message); - } - } - formalIndex++; - } - - bindings.AcceptArgumentExpressionsAsExactParameterList(actuals); - } - - private static string GetLocationInformation(Formal parameter, int bindingCount, int bindingIndex, string formalDescription) { - var displayName = parameter.HasName && parameter is not ImplicitFormal; - var description = ""; - if (bindingCount > 1) { - description += $"at index {bindingIndex} "; - } - - description += $"for {formalDescription}"; - - if (displayName) { - description += $" '{parameter.Name}'"; - } - - return description; - } - private List allDefaultValueExpressions = new List(); /// diff --git a/Source/DafnyCore/Resolver/Scope.cs b/Source/DafnyCore/Resolver/Scope.cs index 5fb437cbeaa..15dfb1049ad 100644 --- a/Source/DafnyCore/Resolver/Scope.cs +++ b/Source/DafnyCore/Resolver/Scope.cs @@ -21,7 +21,7 @@ void ObjectInvariant() { public bool AllowInstance { get { return scopeSizeWhereInstancesWereDisallowed == -1; } set { - Contract.Requires(AllowInstance && !value); // only allowed to change from true to false (that's all that's currently needed in Dafny); Pop is what can make the change in the other direction + Contract.Assume(AllowInstance && !value); // only allowed to change from true to false (that's all that's currently needed in Dafny); Pop is what can make the change in the other direction scopeSizeWhereInstancesWereDisallowed = names.Count; } } diff --git a/Source/DafnyCore/Resolver/CheckTypeInference_Visitor.cs b/Source/DafnyCore/Resolver/TypeInferenceChecker.cs similarity index 54% rename from Source/DafnyCore/Resolver/CheckTypeInference_Visitor.cs rename to Source/DafnyCore/Resolver/TypeInferenceChecker.cs index 811349d8b97..d3a07fb6ea4 100644 --- a/Source/DafnyCore/Resolver/CheckTypeInference_Visitor.cs +++ b/Source/DafnyCore/Resolver/TypeInferenceChecker.cs @@ -7,160 +7,105 @@ namespace Microsoft.Dafny; partial class Resolver { - // ------------------------------------------------------------------------------------------------------ - // ----- CheckTypeInference ----------------------------------------------------------------------------- - // ------------------------------------------------------------------------------------------------------ - // The CheckTypeInference machinery visits every type in a given part of the AST (for example, - // CheckTypeInference(Expression) does so for an Expression and CheckTypeInference_Member(MemberDecl) - // does so for a MemberDecl) to make sure that all parts of types were fully inferred. - #region CheckTypeInference - private void CheckTypeInference_Member(MemberDecl member) { - if (member is ConstantField) { - var field = (ConstantField)member; - if (field.Rhs != null) { - CheckTypeInference(field.Rhs, new NoContext(member.EnclosingClass.EnclosingModuleDefinition)); - } - CheckTypeInference(field.Type, new NoContext(member.EnclosingClass.EnclosingModuleDefinition), field.tok, "const"); - } else if (member is Method) { - var m = (Method)member; - foreach (var formal in m.Ins) { - if (formal.DefaultValue != null) { - CheckTypeInference(formal.DefaultValue, m); + class CheckTypeInferenceVisitor : ASTVisitor { + private readonly Resolver resolver; + private ErrorReporter reporter => resolver.reporter; + + public CheckTypeInferenceVisitor(Resolver resolver) { + this.resolver = resolver; + } + + public override IASTVisitorContext GetContext(IASTVisitorContext astVisitorContext, bool inFunctionPostcondition) { + return astVisitorContext; + } + + protected override void VisitOneDeclaration(TopLevelDecl decl) { + if (decl is NewtypeDecl newtypeDecl) { + if (newtypeDecl.Var != null) { + if (!IsDetermined(newtypeDecl.BaseType.NormalizeExpand())) { + reporter.Error(MessageSource.Resolver, newtypeDecl.tok, "newtype's base type is not fully determined; add an explicit type for '{0}'", + newtypeDecl.Var.Name); + } } - } - 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, m); - } - } else if (member is Function) { - var f = (Function)member; - foreach (var formal in f.Formals) { - if (formal.DefaultValue != null) { - CheckTypeInference(formal.DefaultValue, f); + + } else if (decl is SubsetTypeDecl subsetTypeDecl) { + if (!IsDetermined(subsetTypeDecl.Rhs.NormalizeExpand())) { + reporter.Error(MessageSource.Resolver, subsetTypeDecl.tok, + "subset type's base type is not fully determined; add an explicit type for '{0}'", subsetTypeDecl.Var.Name); } - } - var errorCount = reporter.Count(ErrorLevel.Error); - f.Req.Iter(e => CheckTypeInference(e.E, f)); - f.Ens.Iter(e => CheckTypeInference(e.E, f)); - f.Reads.Iter(fe => CheckTypeInference(fe.E, f)); - CheckTypeInference_Specification_Expr(f.Decreases, f); - if (f.Body != null) { - CheckTypeInference(f.Body, f); - } - if (errorCount == reporter.Count(ErrorLevel.Error)) { - if (f is ExtremePredicate cop) { - CheckTypeInference_Member(cop.PrefixPredicate); - } else if (f.ByMethodDecl != null) { - CheckTypeInference_Member(f.ByMethodDecl); + + } else if (decl is DatatypeDecl datatypeDecl) { + foreach (var member in resolver.classMembers[datatypeDecl].Values) { + if (member is DatatypeDestructor dtor) { + var rolemodel = dtor.CorrespondingFormals[0]; + for (var i = 1; i < dtor.CorrespondingFormals.Count; i++) { + var other = dtor.CorrespondingFormals[i]; + if (!Type.Equal_Improved(rolemodel.Type, other.Type)) { + reporter.Error(MessageSource.Resolver, other, + "shared destructors must have the same type, but '{0}' has type '{1}' in constructor '{2}' and type '{3}' in constructor '{4}'", + rolemodel.Name, rolemodel.Type, dtor.EnclosingCtors[0].Name, other.Type, dtor.EnclosingCtors[i].Name); + } + } + } } } - } - } - private void CheckTypeInference_MaybeFreeExpression(AttributedExpression mfe, ICodeContext codeContext) { - Contract.Requires(mfe != null); - Contract.Requires(codeContext != null); - foreach (var e in Attributes.SubExpressions(mfe.Attributes)) { - CheckTypeInference(e, codeContext); - } - CheckTypeInference(mfe.E, codeContext); - } - 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, codeContext); + base.VisitOneDeclaration(decl); } - spec.Expressions.Iter(e => CheckTypeInference(e, codeContext)); - } - 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, codeContext); + + public override void VisitField(Field field) { + if (field is ConstantField constantField) { + resolver.PartiallySolveTypeConstraints(true); + CheckTypeIsDetermined(field.tok, field.Type, "const"); + } + + base.VisitField(field); } - spec.Expressions.Iter(fe => CheckTypeInference(fe.E, codeContext)); - } - void CheckTypeInference(Expression expr, ICodeContext codeContext) { - Contract.Requires(expr != null); - Contract.Requires(codeContext != null); - PartiallySolveTypeConstraints(true); - var c = new CheckTypeInference_Visitor(this, codeContext); - c.Visit(expr); - } - void CheckTypeInference(Type type, ICodeContext codeContext, IToken tok, string what) { - Contract.Requires(type != null); - Contract.Requires(codeContext != null); - Contract.Requires(tok != null); - Contract.Requires(what != null); - PartiallySolveTypeConstraints(true); - var c = new CheckTypeInference_Visitor(this, codeContext); - c.CheckTypeIsDetermined(tok, type, what); - } - void CheckTypeInference(Statement stmt, ICodeContext codeContext) { - Contract.Requires(stmt != null); - Contract.Requires(codeContext != null); - PartiallySolveTypeConstraints(true); - var c = new CheckTypeInference_Visitor(this, codeContext); - c.Visit(stmt); - } - class CheckTypeInference_Visitor : ResolverBottomUpVisitor { - 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 bool VisitOneStatement(Statement stmt, IASTVisitorContext context) { + if (stmt is CalcStmt calcStmt) { + // The resolution of the calc statement builds up .Steps and .Result, which are of the form E0 OP E1, where + // E0 and E1 are expressions from .Lines. These additional expressions still need to have their .ResolvedOp + // fields filled in, so we visit them, rather than just the parsed .Lines. + Attributes.SubExpressions(calcStmt.Attributes).Iter(e => VisitExpression(e, context)); + calcStmt.Steps.Iter(e => VisitExpression(e, context)); + VisitExpression(calcStmt.Result, context); + calcStmt.Hints.Iter(hint => VisitStatement(hint, context)); + return false; // we're done with all subcomponents of the CalcStmt + } + + return base.VisitOneStatement(stmt, context); } - protected override void VisitOneStmt(Statement stmt) { + protected override void PostVisitOneStatement(Statement stmt, IASTVisitorContext context) { if (stmt is VarDeclStmt) { var s = (VarDeclStmt)stmt; foreach (var local in s.Locals) { CheckTypeIsDetermined(local.Tok, local.Type, "local variable"); - CheckTypeArgsContainNoOrdinal(local.Tok, local.type); + CheckTypeArgsContainNoOrdinal(local.Tok, local.type, context); } } else if (stmt is VarDeclPattern) { var s = (VarDeclPattern)stmt; s.LocalVars.Iter(local => CheckTypeIsDetermined(local.Tok, local.Type, "local variable")); - s.LocalVars.Iter(local => CheckTypeArgsContainNoOrdinal(local.Tok, local.Type)); + s.LocalVars.Iter(local => CheckTypeArgsContainNoOrdinal(local.Tok, local.Type, context)); } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable")); - s.Bounds = DiscoverBestBounds_MultipleVars(s.BoundVars, s.Range, true, ComprehensionExpr.BoundedPool.PoolVirtues.Enumerable); - s.BoundVars.Iter(bv => CheckTypeArgsContainNoOrdinal(bv.tok, bv.Type)); + s.BoundVars.Iter(bv => CheckTypeArgsContainNoOrdinal(bv.tok, bv.Type, context)); } else if (stmt is AssignSuchThatStmt) { var s = (AssignSuchThatStmt)stmt; - if (s.AssumeToken == null) { - var varLhss = new List(); - foreach (var lhs in s.Lhss) { - var ide = (IdentifierExpr)lhs.Resolved; // successful resolution implies all LHS's are IdentifierExpr's - varLhss.Add(ide.Var); - } - s.Bounds = DiscoverBestBounds_MultipleVars(varLhss, s.Expr, true, ComprehensionExpr.BoundedPool.PoolVirtues.None); - } foreach (var lhs in s.Lhss) { - var what = lhs is IdentifierExpr ? string.Format("variable '{0}'", ((IdentifierExpr)lhs).Name) : "LHS"; - CheckTypeArgsContainNoOrdinal(lhs.tok, lhs.Type); - } - } else if (stmt is CalcStmt) { - var s = (CalcStmt)stmt; - // The resolution of the calc statement builds up .Steps and .Result, which are of the form E0 OP E1, where - // E0 and E1 are expressions from .Lines. These additional expressions still need to have their .ResolvedOp - // fields filled in, so we visit them (but not their subexpressions) here. - foreach (var e in s.Steps) { - Visit(e); + var what = lhs is IdentifierExpr ? $"variable '{((IdentifierExpr)lhs).Name}'" : "LHS"; + CheckTypeArgsContainNoOrdinal(lhs.tok, lhs.Type, context); } - Visit(s.Result); } + + base.PostVisitOneStatement(stmt, context); } - protected override void VisitOneExpr(Expression expr) { + protected override void PostVisitOneExpression(Expression expr, IASTVisitorContext context) { if (expr is LiteralExpr) { var e = (LiteralExpr)expr; if (e.Type.IsBitVectorType || e.Type.IsBigOrdinalType) { @@ -180,7 +125,7 @@ protected override void VisitOneExpr(Expression expr) { if (expr is StaticReceiverExpr stexpr) { if (stexpr.ObjectToDiscard != null) { - Visit(stexpr.ObjectToDiscard); + VisitExpression(stexpr.ObjectToDiscard, context); } else { foreach (Type t in stexpr.Type.TypeArgs) { if (t is InferredTypeProxy && ((InferredTypeProxy)t).T == null) { @@ -194,52 +139,10 @@ protected override void VisitOneExpr(Expression expr) { var e = (ComprehensionExpr)expr; foreach (var bv in e.BoundVars) { if (!IsDetermined(bv.Type.Normalize())) { - resolver.reporter.Error(MessageSource.Resolver, bv.tok, "type of bound variable '{0}' could not be determined; please specify the type explicitly", bv.Name); - } else if (codeContext is ExtremePredicate) { - CheckContainsNoOrdinal(bv.tok, bv.Type, string.Format("type of bound variable '{0}' ('{1}') is not allowed to use type ORDINAL", bv.Name, bv.Type)); - } - } - // apply bounds discovery to quantifiers, finite sets, and finite maps - string what = e.WhatKind; - Expression whereToLookForBounds = null; - var polarity = true; - if (e is QuantifierExpr quantifierExpr) { - whereToLookForBounds = quantifierExpr.LogicalBody(); - polarity = quantifierExpr is ExistsExpr; - } else if (e is SetComprehension setComprehension) { - whereToLookForBounds = setComprehension.Range; - } else if (e is MapComprehension) { - whereToLookForBounds = e.Range; - } else { - Contract.Assume(e is LambdaExpr); // otherwise, unexpected ComprehensionExpr - } - if (whereToLookForBounds != null) { - e.Bounds = DiscoverBestBounds_MultipleVars_AllowReordering(e.BoundVars, whereToLookForBounds, polarity, ComprehensionExpr.BoundedPool.PoolVirtues.None); - if (2 <= DafnyOptions.O.Allocated && (codeContext is Function || codeContext is ConstantField || CodeContextWrapper.Unwrap(codeContext) is RedirectingTypeDecl)) { - // functions are not allowed to depend on the set of allocated objects - foreach (var bv in ComprehensionExpr.BoundedPool.MissingBounds(e.BoundVars, e.Bounds, ComprehensionExpr.BoundedPool.PoolVirtues.IndependentOfAlloc)) { - var msgFormat = "a {0} involved in a {3} definition is not allowed to depend on the set of allocated references, but values of '{1}' may contain references"; - if (bv.Type.IsTypeParameter || bv.Type.IsOpaqueType) { - msgFormat += " (perhaps declare its type, '{2}', as '{2}(!new)')"; - } - msgFormat += " (see documentation for 'older' parameters)"; - var declKind = CodeContextWrapper.Unwrap(codeContext) is RedirectingTypeDecl redir ? redir.WhatKind : ((MemberDecl)codeContext).WhatKind; - resolver.reporter.Error(MessageSource.Resolver, e, msgFormat, what, bv.Name, bv.Type, declKind); - } - } - if ((e is SetComprehension && ((SetComprehension)e).Finite) || (e is MapComprehension && ((MapComprehension)e).Finite)) { - // the comprehension had better produce a finite set - if (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 ComprehensionExpr.BoundedPool.MissingBounds(e.BoundVars, e.Bounds, ComprehensionExpr.BoundedPool.PoolVirtues.Finite)) { - resolver.reporter.Error(MessageSource.Resolver, e, - "the result of a {0} must be finite, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{1}'", what, bv.Name); - } - } + resolver.reporter.Error(MessageSource.Resolver, bv.tok, + $"type of bound variable '{bv.Name}' could not be determined; please specify the type explicitly"); + } else if (context is ExtremePredicate) { + CheckContainsNoOrdinal(bv.tok, bv.Type, $"type of bound variable '{bv.Name}' ('{bv.Type}') is not allowed to use type ORDINAL"); } } @@ -258,11 +161,15 @@ protected override void VisitOneExpr(Expression expr) { if (e.Member is Function || e.Member is Method) { var i = 0; foreach (var p in Util.Concat(e.TypeApplication_AtEnclosingClass, e.TypeApplication_JustMember)) { - var tp = i < e.TypeApplication_AtEnclosingClass.Count ? e.Member.EnclosingClass.TypeArgs[i] : ((ICallable)e.Member).TypeArgs[i - e.TypeApplication_AtEnclosingClass.Count]; + var tp = i < e.TypeApplication_AtEnclosingClass.Count + ? e.Member.EnclosingClass.TypeArgs[i] + : ((ICallable)e.Member).TypeArgs[i - e.TypeApplication_AtEnclosingClass.Count]; if (!IsDetermined(p.Normalize())) { - resolver.reporter.Error(MessageSource.Resolver, e.tok, "type parameter '{0}' (inferred to be '{1}') to the {2} '{3}' could not be determined", tp.Name, p, e.Member.WhatKind, e.Member.Name); - } else { - CheckContainsNoOrdinal(e.tok, p, string.Format("type parameter '{0}' (passed in as '{1}') to the {2} '{3}' is not allowed to use ORDINAL", tp.Name, p, e.Member.WhatKind, e.Member.Name)); + resolver.reporter.Error(MessageSource.Resolver, e.tok, + $"type parameter '{tp.Name}' (inferred to be '{p}') to the {e.Member.WhatKind} '{e.Member.Name}' could not be determined"); + } else if (context is not PrefixPredicate) { // this check is done in extreme predicates, so no need to repeat it here for prefix predicates + CheckContainsNoOrdinal(e.tok, p, + $"type parameter '{tp.Name}' (passed in as '{p}') to the {e.Member.WhatKind} '{e.Member.Name}' is not allowed to use ORDINAL"); } i++; } @@ -271,15 +178,18 @@ protected override void VisitOneExpr(Expression expr) { var e = (FunctionCallExpr)expr; var i = 0; foreach (var p in Util.Concat(e.TypeApplication_AtEnclosingClass, e.TypeApplication_JustFunction)) { - var tp = i < e.TypeApplication_AtEnclosingClass.Count ? e.Function.EnclosingClass.TypeArgs[i] : e.Function.TypeArgs[i - e.TypeApplication_AtEnclosingClass.Count]; + var tp = i < e.TypeApplication_AtEnclosingClass.Count + ? e.Function.EnclosingClass.TypeArgs[i] + : e.Function.TypeArgs[i - e.TypeApplication_AtEnclosingClass.Count]; if (!IsDetermined(p.Normalize())) { - resolver.reporter.Error(MessageSource.Resolver, e.tok, "type parameter '{0}' (inferred to be '{1}') in the function call to '{2}' could not be determined{3}", tp.Name, p, e.Name, - (e.Name.StartsWith("reveal_")) + var hint = e.Name.StartsWith("reveal_") ? ". If you are making an opaque function, make sure that the function can be called." - : "" - ); - } else { - CheckContainsNoOrdinal(e.tok, p, string.Format("type parameter '{0}' (passed in as '{1}') to function call '{2}' is not allowed to use ORDINAL", tp.Name, p, e.Name)); + : ""; + resolver.reporter.Error(MessageSource.Resolver, e.tok, + $"type parameter '{tp.Name}' (inferred to be '{p}') in the function call to '{e.Name}' could not be determined{hint}"); + } else if (context is not PrefixPredicate) { // this check is done in extreme predicates, so no need to repeat it here for prefix predicates + CheckContainsNoOrdinal(e.tok, p, + $"type parameter '{tp.Name}' (passed in as '{p}') to function call '{e.Name}' is not allowed to use ORDINAL"); } i++; } @@ -288,9 +198,9 @@ protected override void VisitOneExpr(Expression expr) { foreach (var p in e.LHSs) { foreach (var x in p.Vars) { if (!IsDetermined(x.Type.Normalize())) { - resolver.reporter.Error(MessageSource.Resolver, x.tok, "the type of the bound variable '{0}' could not be determined", x.Name); + resolver.reporter.Error(MessageSource.Resolver, x.tok, $"the type of the bound variable '{x.Name}' could not be determined"); } else { - CheckTypeArgsContainNoOrdinal(x.tok, x.Type); + CheckTypeArgsContainNoOrdinal(x.tok, x.Type, context); } } } @@ -306,7 +216,8 @@ protected override void VisitOneExpr(Expression expr) { // looks good } else { resolver.reporter.Error(MessageSource.Resolver, e.tok, - "a type cast to a reference type ({0}) must be from a compatible type (got {1}); this cast could never succeed", e.ToType, fromType); + "a type cast to a reference type ({0}) must be from a compatible type (got {1}); this cast could never succeed", + e.ToType, fromType); } } } else if (expr is TypeTestExpr) { @@ -351,12 +262,12 @@ protected override void VisitOneExpr(Expression expr) { string hint = ""; other = other.Resolved; if (other is IdentifierExpr) { - name = string.Format("variable '{0}'", ((IdentifierExpr)other).Name); + name = $"variable '{((IdentifierExpr)other).Name}'"; } else if (other is MemberSelectExpr) { var field = ((MemberSelectExpr)other).Member as Field; // The type of the field may be a formal type parameter, in which case the hint is omitted if (field.Type.IsNonNullRefType) { - name = string.Format("field '{0}'", field.Name); + name = $"field '{field.Name}'"; } } if (name != null) { @@ -370,11 +281,11 @@ protected override void VisitOneExpr(Expression expr) { Contract.Assert(nonNullTypeDecl.TypeArgs.Count == nntUdf.TypeArgs.Count); var ty = new UserDefinedType(nntUdf.tok, possiblyNullUdf.Name, possiblyNullTypeDecl, nntUdf.TypeArgs); - hint = string.Format(" (to make it possible for {0} to have the value 'null', declare its type to be '{1}')", name, ty); + hint = $" (to make it possible for {name} to have the value 'null', declare its type to be '{ty}')"; } + var b = sense ? "false" : "true"; resolver.reporter.Warning(MessageSource.Resolver, e.tok, - string.Format("the type of the other operand is a non-null type, so this comparison with 'null' will always return '{0}'{1}", - sense ? "false" : "true", hint)); + $"the type of the other operand is a non-null type, so this comparison with 'null' will always return '{b}'{hint}"); } break; } @@ -389,9 +300,10 @@ protected override void VisitOneExpr(Expression expr) { var ty = other.Type.NormalizeExpand(); var what = ty is SetType ? "set" : ty is SeqType ? "seq" : "multiset"; if (((CollectionType)ty).Arg.IsNonNullRefType) { + var non = sense ? "" : "non-"; + var b = sense ? "false" : "true"; resolver.reporter.Warning(MessageSource.Resolver, e.tok, - string.Format("the type of the other operand is a {0} of non-null elements, so the {1}inclusion test of 'null' will always return '{2}'", - what, sense ? "" : "non-", sense ? "false" : "true")); + $"the type of the other operand is a {what} of non-null elements, so the {non}inclusion test of 'null' will always return '{b}'"); } break; } @@ -400,9 +312,9 @@ protected override void VisitOneExpr(Expression expr) { case BinaryExpr.ResolvedOpcode.InMap: { var ty = other.Type.NormalizeExpand(); if (((MapType)ty).Domain.IsNonNullRefType) { + var b = sense ? "false" : "true"; resolver.reporter.Warning(MessageSource.Resolver, e.tok, - string.Format("the type of the other operand is a map to a non-null type, so the inclusion test of 'null' will always return '{0}'", - sense ? "false" : "true")); + $"the type of the other operand is a map to a non-null type, so the inclusion test of 'null' will always return '{b}'"); } break; } @@ -414,7 +326,8 @@ protected override void VisitOneExpr(Expression expr) { var e = (NegationExpression)expr; Expression resolved = null; if (e.E is LiteralExpr lit) { // note, not e.E.Resolved, since we don't want to do this for double negations - // For real-based types, integer-based types, and bi (but not bitvectors), "-" followed by a literal is just a literal expression with a negative value + // For real-based types, integer-based types, and bi (but not bitvectors), "-" followed by a literal is + // just a literal expression with a negative value if (e.E.Type.IsNumericBased(Type.NumericPersuasion.Real)) { var d = (BaseTypes.BigDec)lit.Value; Contract.Assert(!d.IsNegative); @@ -441,14 +354,19 @@ protected override void VisitOneExpr(Expression expr) { e.ResolvedExpression = resolved; } } + + base.VisitOneExpression(expr, context); } + public static bool IsDetermined(Type t) { Contract.Requires(t != null); Contract.Requires(!(t is TypeProxy) || ((TypeProxy)t).T == null); // all other proxies indicate the type has not yet been determined, provided their type parameters have been return !(t is TypeProxy) && t.TypeArgs.All(tt => IsDetermined(tt.Normalize())); } - ISet UnderspecifiedTypeProxies = new HashSet(); + + readonly ISet UnderspecifiedTypeProxies = new HashSet(); + public bool CheckTypeIsDetermined(IToken tok, Type t, string what) { Contract.Requires(tok != null); Contract.Requires(t != null); @@ -467,12 +385,19 @@ public bool CheckTypeIsDetermined(IToken tok, Type t, string what) { // Recurse on type arguments: return t.TypeArgs.All(rg => CheckTypeIsDetermined(tok, rg, what)); } - public void CheckTypeArgsContainNoOrdinal(IToken tok, Type t) { + + public void CheckTypeArgsContainNoOrdinal(IToken tok, Type t, IASTVisitorContext context) { Contract.Requires(tok != null); Contract.Requires(t != null); - t = t.NormalizeExpand(); - t.TypeArgs.Iter(rg => CheckContainsNoOrdinal(tok, rg, "an ORDINAL type is not allowed to be used as a type argument")); + if (context is PrefixPredicate or PrefixLemma) { + // User-provided expressions in extreme predicates/lemmas are checked in the extreme declarations, so need + // need to do them here again for the prefix predicates/lemmas. + } else { + t = t.NormalizeExpand(); + t.TypeArgs.Iter(rg => CheckContainsNoOrdinal(tok, rg, "an ORDINAL type is not allowed to be used as a type argument")); + } } + public void CheckContainsNoOrdinal(IToken tok, Type t, string errMsg) { Contract.Requires(tok != null); Contract.Requires(t != null); @@ -484,5 +409,4 @@ public void CheckContainsNoOrdinal(IToken tok, Type t, string errMsg) { t.TypeArgs.Iter(rg => CheckContainsNoOrdinal(tok, rg, errMsg)); } } - #endregion CheckTypeInference } \ No newline at end of file diff --git a/Test/dafny0/AttributeChecks.dfy b/Test/dafny0/AttributeChecks.dfy index 24e3906cdf1..2475d7c4859 100644 --- a/Test/dafny0/AttributeChecks.dfy +++ b/Test/dafny0/AttributeChecks.dfy @@ -101,10 +101,10 @@ module JustAboutEverything { } datatype {:dt 0} {:dt false + 3} Datatype = // error: false + 3 is ill-typed - {:dt k} Blue | {:dt 50} Green // error: k is unknown + {:dt k, this} Blue | {:dt 50} Green // error (x2): k is unknown, this is not allowed datatype {:dt 0} {:dt false + 3} AnotherDatatype = // error: false + 3 is ill-typed - | {:dt 50} Blue | {:dt k} Green // error: k is unknown + | {:dt 50} Blue | {:dt k, this} Green // error (x2): k is unknown, this is not allowed function FAttr(x: int): int requires {:myAttr false + 3} true // error: false + 3 is ill-typed @@ -366,7 +366,7 @@ module JustAboutEverything { predicate method IsFailure() { DoesNotHave? } - function method PropagateFailure(): Option + function method PropagateFailure(): Option requires DoesNotHave? { None @@ -381,3 +381,116 @@ module Modu { } + +module TwoStateAttributes { + class C { + var data: int + + function {:myAttr old(data), x, r} F(x: int): (r: int) // error: old not allowed in this context + + twostate function {:myAttr old(data), x, r} F2(x: int): (r: int) // old is allowed + + lemma {:myAttr old(data), x, y} L(x: int) returns (y: int) // error: old not allowed in this context + + twostate lemma {:myAttr old(data), x, y} L2(x: int) returns (y: int) // old is allowed + + method {:myAttr old(data), x, y} M(x: int) returns (y: int) // error: old not allowed in this context + + least predicate {:myAttr old(data), x} LP(x: int) // error: old not allowed in this context + + least lemma {:myAttr old(data), x} LL(x: int) // error: old not allowed in this context + } +} + +module TopLevelAttributes { + // ---- iterator + + // an attribute on an iterator is allowed to refer to the in-parameters of the iterator, but not to "this" or to the yield-parameters. + iterator + {:myAttr x} + {:myAttr y} // error: y is not allowed here + {:myAttr this} // error: this is not allowed here + {:myAttr ys} // error: ys is not allowed here (because "this" isn't) + {:myAttr old(arr[0])} // error: "old" is not allowed here + Iterator(x: int, arr: array) yields (y: int) + requires arr.Length != 0 + + // ---- opaque type + + type + {:myAttr this} // error: this is not allowed here + {:myAttr N} // error: N unresolved + Opaque + { + const N: int + } + + // ---- subset type + + type {:myAttr this} Subset = x: int | true // error: "this" is not allowed here + + // ---- type synonym + + type {:myAttr this} Synonym = int // error: "this" is not allowed here + + // ---- newtype + + newtype + {:myAttr this} // error: this is not allowed + {:myAttr N} // error: N unresolved + Newtype = x: int | true + { + const N: int + } + + // ---- trait + + trait + {:myAttr this} // error: this is not allowed + {:myAttr x} // error: x unresolved + Trait + { + var x: int + } + + // ---- class + + class + {:myAttr this} // error: this is not allowed + {:myAttr x} // error: x unresolved + Class + { + var x: int + } + + // ---- datatype + + datatype + {:myAttr this} // error: this is not allowed here + {:myAttr Ctor?} // error: Ctor? unresolved + {:myAttr y} // error: y unresolved + {:myAttr N} // error: N unresolved + Datatype = Ctor(y: int) + { + const N: int + } + + // ---- codatatype + + codatatype + {:myAttr this} // error: this is not allowed here + {:myAttr Ctor?} // error: Ctor? unresolved + {:myAttr y} // error: y unresolved + {:myAttr N} // error: N unresolved + CoDatatype = Ctor(y: int) + { + const N: int + } +} + +module TopLevelAttributesModule { + // ---- module + + module {:myAttr this} Module { // error: "this" is not allowed here + } +} diff --git a/Test/dafny0/AttributeChecks.dfy.expect b/Test/dafny0/AttributeChecks.dfy.expect index 79612601f40..f1e4c74e947 100644 --- a/Test/dafny0/AttributeChecks.dfy.expect +++ b/Test/dafny0/AttributeChecks.dfy.expect @@ -4,9 +4,9 @@ module JustAboutEverything { datatype List = Nil | Cons(hd: T, tl: List) - datatype {:dt 0} {:dt false + 3} Datatype = {:dt k} Blue | {:dt 50} Green + datatype {:dt 0} {:dt false + 3} Datatype = {:dt k, this} Blue | {:dt 50} Green - datatype {:dt 0} {:dt false + 3} AnotherDatatype = {:dt 50} Blue | {:dt k} Green + datatype {:dt 0} {:dt false + 3} AnotherDatatype = {:dt 50} Blue | {:dt k, this} Green iterator Iter(x: int) yields (y: int) requires {:myAttr false + 3} true @@ -71,7 +71,7 @@ module JustAboutEverything { DoesNotHave? } - function method PropagateFailure(): Option + function method PropagateFailure(): Option requires DoesNotHave? { None @@ -352,23 +352,87 @@ module JustAboutEverything { module {:myAttr false + 3} {:myAttr old(3)} {:myAttr k} Modu { } + +module TwoStateAttributes { + class C { + var data: int + + function {:myAttr old(data), x, r} F(x: int): (r: int) + + twostate function {:myAttr old(data), x, r} F2(x: int): (r: int) + + lemma {:myAttr old(data), x, y} L(x: int) returns (y: int) + + twostate lemma {:myAttr old(data), x, y} L2(x: int) returns (y: int) + + method {:myAttr old(data), x, y} M(x: int) returns (y: int) + + least predicate {:myAttr old(data), x} LP(x: int) + + least lemma {:myAttr old(data), x} LL(x: int) + } +} + +module TopLevelAttributes { + iterator {:myAttr x} {:myAttr y} {:myAttr this} {:myAttr ys} {:myAttr old(arr[0])} Iterator(x: int, arr: array) yields (y: int) + requires arr.Length != 0 + + type {:myAttr this} {:myAttr N} Opaque { + const N: int + } + + type {:myAttr this} Subset = x: int + | true + + type {:myAttr this} Synonym = int + + newtype {:myAttr this} {:myAttr N} Newtype = x: int + | true + { + const N: int + } + + trait {:myAttr this} {:myAttr x} Trait { + var x: int + } + + class {:myAttr this} {:myAttr x} Class { + var x: int + } + + datatype {:myAttr this} {:myAttr Ctor?} {:myAttr y} {:myAttr N} Datatype = Ctor(y: int) { + const N: int + } + + codatatype {:myAttr this} {:myAttr Ctor?} {:myAttr y} {:myAttr N} CoDatatype = Ctor(y: int) { + const N: int + } +} + +module TopLevelAttributesModule { + + module {:myAttr this} Module { + } +} AttributeChecks.dfy(104,9): Error: unresolved identifier: k +AttributeChecks.dfy(104,12): Error: 'this' is not allowed in a 'static' context AttributeChecks.dfy(103,30): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) AttributeChecks.dfy(103,30): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(107,27): Error: unresolved identifier: k +AttributeChecks.dfy(107,30): Error: 'this' is not allowed in a 'static' context AttributeChecks.dfy(106,30): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) AttributeChecks.dfy(106,30): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(211,29): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(211,29): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(208,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(208,28): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(206,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(206,28): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(207,34): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(207,34): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(209,33): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(209,33): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(210,27): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(211,29): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(208,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(206,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(207,34): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(209,33): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(210,27): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(221,23): Error: old expressions are not allowed in this context AttributeChecks.dfy(218,22): Error: old expressions are not allowed in this context @@ -399,10 +463,10 @@ AttributeChecks.dfy(85,25): Error: type of + must be of a numeric type, a bitvec AttributeChecks.dfy(96,32): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(96,32): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) AttributeChecks.dfy(110,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(110,28): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(111,27): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(111,27): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(112,29): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(110,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(111,27): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(112,29): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(118,22): Error: old expressions are not allowed in this context AttributeChecks.dfy(119,21): Error: old expressions are not allowed in this context @@ -410,20 +474,20 @@ AttributeChecks.dfy(120,23): Error: old expressions are not allowed in this cont AttributeChecks.dfy(126,25): Error: unresolved identifier: r AttributeChecks.dfy(128,26): Error: unresolved identifier: r AttributeChecks.dfy(134,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(134,28): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(135,27): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(135,27): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(136,29): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(134,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(135,27): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(136,29): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(150,25): Error: unresolved identifier: r AttributeChecks.dfy(152,26): Error: unresolved identifier: r AttributeChecks.dfy(158,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(158,28): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(159,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(159,28): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(161,29): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(161,29): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(160,27): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(158,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(159,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(161,29): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(160,27): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(166,22): Error: old expressions are not allowed in this context AttributeChecks.dfy(167,22): Error: old expressions are not allowed in this context @@ -433,12 +497,12 @@ AttributeChecks.dfy(175,25): Error: unresolved identifier: y AttributeChecks.dfy(177,26): Error: unresolved identifier: y AttributeChecks.dfy(183,33): Error: twostate lemmas are not allowed to have modifies clauses AttributeChecks.dfy(182,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(182,28): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(183,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(183,28): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(185,29): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(185,29): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(184,27): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(182,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(183,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(185,29): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(184,27): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(191,22): Error: old expressions are not allowed in this context AttributeChecks.dfy(191,30): Error: twostate lemmas are not allowed to have modifies clauses @@ -450,106 +514,106 @@ AttributeChecks.dfy(201,26): Error: unresolved identifier: y AttributeChecks.dfy(236,26): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) AttributeChecks.dfy(236,26): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(242,23): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(242,23): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(243,23): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(243,23): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(247,26): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(247,26): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(248,26): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(248,26): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(250,26): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(250,26): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(251,26): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(251,26): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(254,25): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(254,25): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(255,38): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(255,38): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(256,34): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(256,34): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(259,25): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(259,25): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(260,38): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(260,38): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(261,29): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(261,29): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(264,25): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(264,25): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(265,42): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(265,42): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(266,38): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(266,38): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(267,25): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(267,25): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(268,44): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(268,44): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(269,40): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(269,40): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(273,25): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(273,25): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(275,23): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(275,23): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(276,23): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(276,23): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(280,38): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(280,38): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(283,25): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(283,25): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(285,23): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(285,23): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(286,23): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(286,23): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(289,25): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(289,25): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(291,23): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(291,23): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(292,23): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(292,23): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(296,35): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(296,35): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(298,27): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(298,27): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(299,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(299,28): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(301,27): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(301,27): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(302,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(302,28): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(303,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(303,28): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(305,44): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(305,44): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(306,49): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(306,49): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(308,33): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(308,33): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(309,39): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(309,39): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(312,38): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(312,38): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(313,38): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(313,38): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(314,38): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(314,38): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(315,34): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(315,34): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(316,34): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(316,34): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(317,34): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(317,34): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(320,38): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(320,38): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(321,38): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(321,38): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(322,38): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(322,38): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(323,34): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(323,34): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(324,34): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(324,34): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(325,34): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(325,34): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(329,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(242,23): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(243,23): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(247,26): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(248,26): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(250,26): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(251,26): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(254,25): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(255,38): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(256,34): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(259,25): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(260,38): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(261,29): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(264,25): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(265,42): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(266,38): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(267,25): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(268,44): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(269,40): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(273,25): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(275,23): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(276,23): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(280,38): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(283,25): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(285,23): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(286,23): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(289,25): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(291,23): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(292,23): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(296,35): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(298,27): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(299,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(301,27): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(302,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(303,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(305,44): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(306,49): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(308,33): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(309,39): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(312,38): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(313,38): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(314,38): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(315,34): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(316,34): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(317,34): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(320,38): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(321,38): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(322,38): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(323,34): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(324,34): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(325,34): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(329,28): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(335,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) AttributeChecks.dfy(335,28): Error: type of right argument to + (int) must agree with the result type (bool) @@ -557,4 +621,32 @@ AttributeChecks.dfy(380,11): Error: unresolved identifier: k AttributeChecks.dfy(379,11): Error: old expressions are not allowed in this context AttributeChecks.dfy(378,17): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) AttributeChecks.dfy(378,17): Error: type of right argument to + (int) must agree with the result type (bool) -205 resolution/type errors detected in AttributeChecks.dfy +AttributeChecks.dfy(389,22): Error: old expressions are not allowed in this context +AttributeChecks.dfy(393,19): Error: old expressions are not allowed in this context +AttributeChecks.dfy(397,20): Error: old expressions are not allowed in this context +AttributeChecks.dfy(399,29): Error: old expressions are not allowed in this context +AttributeChecks.dfy(401,25): Error: old expressions are not allowed in this context +AttributeChecks.dfy(414,13): Error: old expressions are not allowed in this context +AttributeChecks.dfy(413,13): Error: unresolved identifier: ys +AttributeChecks.dfy(412,13): Error: 'this' is not allowed in a 'static' context +AttributeChecks.dfy(411,13): Error: unresolved identifier: y +AttributeChecks.dfy(422,13): Error: unresolved identifier: N +AttributeChecks.dfy(421,13): Error: 'this' is not allowed in a 'static' context +AttributeChecks.dfy(430,16): Error: 'this' is not allowed in a 'static' context +AttributeChecks.dfy(434,16): Error: 'this' is not allowed in a 'static' context +AttributeChecks.dfy(440,13): Error: unresolved identifier: N +AttributeChecks.dfy(439,13): Error: 'this' is not allowed in a 'static' context +AttributeChecks.dfy(450,13): Error: unresolved identifier: x +AttributeChecks.dfy(449,13): Error: 'this' is not allowed in a 'static' context +AttributeChecks.dfy(460,13): Error: unresolved identifier: x +AttributeChecks.dfy(459,13): Error: 'this' is not allowed in a 'static' context +AttributeChecks.dfy(472,13): Error: unresolved identifier: N +AttributeChecks.dfy(471,13): Error: unresolved identifier: y +AttributeChecks.dfy(470,13): Error: unresolved identifier: Ctor? +AttributeChecks.dfy(469,13): Error: 'this' is not allowed in a 'static' context +AttributeChecks.dfy(484,13): Error: unresolved identifier: N +AttributeChecks.dfy(483,13): Error: unresolved identifier: y +AttributeChecks.dfy(482,13): Error: unresolved identifier: Ctor? +AttributeChecks.dfy(481,13): Error: 'this' is not allowed in a 'static' context +AttributeChecks.dfy(494,18): Error: 'this' is not allowed in a 'static' context +235 resolution/type errors detected in AttributeChecks.dfy diff --git a/Test/dafny0/AutoContracts.dfy.expect b/Test/dafny0/AutoContracts.dfy.expect index f9967197034..a13e5572849 100644 --- a/Test/dafny0/AutoContracts.dfy.expect +++ b/Test/dafny0/AutoContracts.dfy.expect @@ -8,7 +8,11 @@ module _System { * SCC at height 1: * RotateRight * SCC at height 0: + * array + * SCC at height 0: * nat + * SCC at height 0: + * object */ type string(==,0) = seq @@ -123,6 +127,10 @@ module OneModule { * SCC at height 1: * C.Valid * SCC at height 0: + * C + * SCC at height 0: + * D + * SCC at height 0: * D.Valid */ class {:autocontracts} D { @@ -276,6 +284,8 @@ module N0 { * SCC at height 1: * C.Z * SCC at height 0: + * C + * SCC at height 0: * C.Valid */ class {:autocontracts} C { @@ -370,6 +380,8 @@ module N1 refines N0 { * SCC at height 1: * C.Z * SCC at height 0: + * C + * SCC at height 0: * C.Valid */ class {:autocontracts} C ... { @@ -470,6 +482,8 @@ module N2 refines N1 { * SCC at height 1: * C.Z * SCC at height 0: + * C + * SCC at height 0: * C.Valid */ class {:autocontracts} C ... { diff --git a/Test/dafny0/Bitvectors.dfy.expect b/Test/dafny0/Bitvectors.dfy.expect index ef96ee6e5c1..b06b2aef28a 100644 --- a/Test/dafny0/Bitvectors.dfy.expect +++ b/Test/dafny0/Bitvectors.dfy.expect @@ -8,7 +8,11 @@ module _System { * SCC at height 1: * RotateRight * SCC at height 0: + * array + * SCC at height 0: * nat + * SCC at height 0: + * object */ type string(==,0) = seq diff --git a/Test/dafny0/BitvectorsMore.dfy.expect b/Test/dafny0/BitvectorsMore.dfy.expect index 911d62d6c15..ffbf0323487 100644 --- a/Test/dafny0/BitvectorsMore.dfy.expect +++ b/Test/dafny0/BitvectorsMore.dfy.expect @@ -8,7 +8,11 @@ module _System { * SCC at height 1: * RotateRight * SCC at height 0: + * array + * SCC at height 0: * nat + * SCC at height 0: + * object */ type string(==,0) = seq diff --git a/Test/dafny0/ModuleInsertion.dfy.expect b/Test/dafny0/ModuleInsertion.dfy.expect index 8fac0f5bd35..22a1f026338 100644 --- a/Test/dafny0/ModuleInsertion.dfy.expect +++ b/Test/dafny0/ModuleInsertion.dfy.expect @@ -114,7 +114,11 @@ module _System { * SCC at height 1: * RotateRight * SCC at height 0: + * array + * SCC at height 0: * nat + * SCC at height 0: + * object */ type string(==,0) = seq diff --git a/Test/dafny0/PrefixTypeSubst.dfy.expect b/Test/dafny0/PrefixTypeSubst.dfy.expect index 9ac1e5f9e49..5d056a74424 100644 --- a/Test/dafny0/PrefixTypeSubst.dfy.expect +++ b/Test/dafny0/PrefixTypeSubst.dfy.expect @@ -8,7 +8,11 @@ module _System { * SCC at height 1: * RotateRight * SCC at height 0: + * array + * SCC at height 0: * nat + * SCC at height 0: + * object */ type string(==,0) = seq diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 75d4799dfce..57fe7cb203d 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1153,16 +1153,16 @@ module MiscTrait { // ----- set comprehensions where the term type is finite ----- -module ObjectSetComprehensions { +module ObjectSetComprehensionsNever { // 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 - function method B() : set { set o : object | true :: o } // error: a function is not allowed to depend on the allocated state - +} +module ObjectSetComprehensionsSometimes { // outside functions, the comprehension is permitted, but it cannot be compiled lemma C() { var x; x := set o : object | true :: o; } - method D() { var x; x := set o : object | true :: o; } // error: not (easily) compilable + method D() { var x; x := set o : object | true :: o; } // error: not (easily) compilable, so this is allowed only in ghost contexts } // ------ regression test for type checking of integer division ----- @@ -2347,14 +2347,21 @@ module Regression15 { } } -module AllocDepend0 { +module AllocDepend0a { class Class { - const z := if {} == set c: Class | true then 5 else 4 // error (x2): condition depends on alloc; not compilable + const z := if {} == set c: Class | true then 5 else 4 // error: condition depends on alloc (also not compilable, but that's not reported in the same pass) } - const y := if {} == set c: Class | true then 5 else 4 // error (x2): condition depends on alloc; not compilable + const y := if {} == set c: Class | true then 5 else 4 // error: condition depends on alloc (also not compilable, but that's not reported in the same pass) newtype byte = x | x < 5 || {} == set c: Class | true // error: condition not allowed to depend on alloc type small = x | x < 5 || {} == set c: Class | true // error: condition not allowed to depend on alloc } +module AllocDepend0b { + class Class { } + method M() returns (y: int, z: int) { + z := if {} == set c: Class | true then 5 else 4; // error: not compilable + y := if {} == set c: Class | true then 5 else 4; // error: not compilable + } +} module AllocDepend1 { class Class { } predicate method P(x: int) { @@ -2793,16 +2800,16 @@ module GhostReceiverTests { module GhostRhsConst { class C { function F(n: nat): nat { n } // a ghost function - + static function G(n: nat): nat { n } // a ghost function const b := F(0); // error: RHS uses a ghost function - static const u := F(0); // error: RHS uses a ghost function + static const u := G(0); // error: RHS uses a ghost function } trait R { function F(n: nat): nat { n } // a ghost function - + static function G(n: nat): nat { n } // a ghost function const b := F(0); // error: RHS uses a ghost function - static const u := F(0); // error: RHS uses a ghost function + static const u := G(0); // error: RHS uses a ghost function } } @@ -3848,3 +3855,54 @@ module LabelRegressions { } } } + +// --------------- regressions: using "this" in places where there is no enclosing class/type ------------------------------ + +module UseOfThis { + // The following uses of "this." once caused the resolver to crash. + + type {:badUseOfThis this.K} OpaqueType { // error: cannot use "this" here + const K: int + } + + newtype {:badUseOfThis this.x} Newtype = // error: cannot use "this" here + x: int | this.u // error: cannot use "this" here + witness this.u // error: cannot use "this" here + { + const K: int + } + + type {:badUseOfThis this.x} SynonymType = int // error: cannot use "this" here + + type {:badUseOfThis this.x} SubsetType = // error: cannot use "this" here + x: int | this.u // error: cannot use "this" here + witness this.u // error: cannot use "this" here + + trait {:badUseOfThis this.K} MyTrait { // error: cannot use "this" here + const K: int + } + + class {:badUseOfThis this.M} MyClass { // error: cannot use "this" here + const M: int + + var {:goodUseOfThis this.M} I: int + const {:goodUseOfThis this.M} J := 3 + method {:goodUseOfThis this.M} CM() + ensures {:goodUseOfThis this.M} true + function {:goodUseOfThis this.M} CF(): int + ensures {:goodUseOfThis this.M} true + + static const {:badUseOfThis this.M} L := 3 // error: cannot use "this" here + static const N := this.M // error: cannot use "this" here + static method {:badUseOfThis this.M} SM() // error: cannot use "this" here + ensures {:badUseOfThis this.M} true // error: cannot use "this" here + static function {:badUseOfThis this.M} SF(): int // error: cannot use "this" here + ensures {:badUseOfThis this.M} true // error: cannot use "this" here + } + + datatype Datatype = + | {:badUseOfThis this.K} DatatypeCtor // error: cannot use "this" here + { + const K: int + } +} diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 3e72702d07d..69244c870dd 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -159,7 +159,7 @@ ResolutionErrors.dfy(1138,13): Error: arguments must have comparable types (got ResolutionErrors.dfy(1139,13): Error: arguments must have comparable types (got P and P) ResolutionErrors.dfy(1150,10): Error: new can be applied only to class types (got JJ) ResolutionErrors.dfy(1158,31): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'o' may contain references (see documentation for 'older' parameters) -ResolutionErrors.dfy(1160,38): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'o' may contain references (see documentation for 'older' parameters) +ResolutionErrors.dfy(1159,38): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'o' may contain references (see documentation for 'older' parameters) ResolutionErrors.dfy(1165,27): 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(1173,15): Error: arguments to / must be numeric or bitvector types (got set) ResolutionErrors.dfy(1180,20): 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 @@ -236,7 +236,6 @@ ResolutionErrors.dfy(1647,10): Error: the type of the bound variable 't' could n ResolutionErrors.dfy(1647,10): Error: the type of the bound variable 't' could not be determined ResolutionErrors.dfy(1647,10): Error: the type of the bound variable 't' could not be determined ResolutionErrors.dfy(1647,10): Error: the type of the bound variable 't' could not be determined -ResolutionErrors.dfy(1647,10): Error: the type of the bound variable 't' could not be determined ResolutionErrors.dfy(1665,15): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) ResolutionErrors.dfy(1667,10): Error: assignment to non-ghost field is not allowed in this context, because this is a ghost method ResolutionErrors.dfy(1692,15): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) @@ -346,257 +345,285 @@ ResolutionErrors.dfy(2327,18): Error: a ghost const field is allowed only in spe ResolutionErrors.dfy(2343,9): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'i' ResolutionErrors.dfy(2346,9): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'i' ResolutionErrors.dfy(2352,24): Error: a set comprehension involved in a const field definition is not allowed to depend on the set of allocated references, but values of 'c' may contain references (see documentation for 'older' parameters) -ResolutionErrors.dfy(2352,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 'c' ResolutionErrors.dfy(2355,36): Error: a set comprehension involved in a newtype definition is not allowed to depend on the set of allocated references, but values of 'c' may contain references (see documentation for 'older' parameters) ResolutionErrors.dfy(2356,34): Error: a set comprehension involved in a subset type definition is not allowed to depend on the set of allocated references, but values of 'c' may contain references (see documentation for 'older' parameters) ResolutionErrors.dfy(2354,22): Error: a set comprehension involved in a const field definition is not allowed to depend on the set of allocated references, but values of 'c' may contain references (see documentation for 'older' parameters) -ResolutionErrors.dfy(2354,22): 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 'c' -ResolutionErrors.dfy(2361,19): Error: a set comprehension involved in a predicate definition is not allowed to depend on the set of allocated references, but values of 'c' may contain references (see documentation for 'older' parameters) -ResolutionErrors.dfy(2367,37): Error: a const field definition is not allowed to depend on the set of allocated references -ResolutionErrors.dfy(2370,49): Error: a newtype definition is not allowed to depend on the set of allocated references -ResolutionErrors.dfy(2371,47): Error: a subset type definition is not allowed to depend on the set of allocated references -ResolutionErrors.dfy(2369,35): Error: a const field definition is not allowed to depend on the set of allocated references -ResolutionErrors.dfy(2376,32): Error: a predicate definition is not allowed to depend on the set of allocated references -ResolutionErrors.dfy(2382,41): Error: a const field definition is not allowed to depend on the set of allocated references -ResolutionErrors.dfy(2385,53): Error: a newtype definition is not allowed to depend on the set of allocated references -ResolutionErrors.dfy(2386,51): Error: a subset type definition is not allowed to depend on the set of allocated references -ResolutionErrors.dfy(2384,39): Error: a const field definition is not allowed to depend on the set of allocated references -ResolutionErrors.dfy(2391,36): Error: a predicate definition is not allowed to depend on the set of allocated references -ResolutionErrors.dfy(2398,25): Error: the value returned by an abstemious function must come from invoking a co-constructor -ResolutionErrors.dfy(2434,25): Error: the value returned by an abstemious function must come from invoking a co-constructor -ResolutionErrors.dfy(2441,32): Error: an abstemious function is allowed to invoke a codatatype destructor only on its parameters -ResolutionErrors.dfy(2446,12): Error: an abstemious function is allowed to codatatype-match only on its parameters -ResolutionErrors.dfy(2453,9): Error: an abstemious function is not only allowed to check codatatype equality -ResolutionErrors.dfy(2455,14): Error: an abstemious function is not only allowed to check codatatype equality -ResolutionErrors.dfy(2480,19): Error: type parameter 'G' (passed in as 'ORDINAL') to function call 'F' is not allowed to use ORDINAL -ResolutionErrors.dfy(2481,13): Error: type parameter 'G' (passed in as 'ORDINAL') to function call 'F'' is not allowed to use ORDINAL -ResolutionErrors.dfy(2482,13): Error: type parameter 'G' (passed in as '(char, ORDINAL)') to function call 'F'' is not allowed to use ORDINAL -ResolutionErrors.dfy(2483,18): Error: type parameter 'G' (passed in as 'ORDINAL') to the function 'F'' is not allowed to use ORDINAL -ResolutionErrors.dfy(2488,17): Error: type of bound variable 'r' ('ORDINAL') is not allowed to use type ORDINAL -ResolutionErrors.dfy(2489,18): Error: type of bound variable 'r' ('ORDINAL') is not allowed to use type ORDINAL -ResolutionErrors.dfy(2490,24): Error: type of bound variable 'r' ('ORDINAL') is not allowed to use type ORDINAL -ResolutionErrors.dfy(2501,25): Error: an ORDINAL type is not allowed to be used as a type argument -ResolutionErrors.dfy(2502,17): Error: type of bound variable 'yt' ('ORDINAL') is not allowed to use type ORDINAL -ResolutionErrors.dfy(2499,8): Error: an ORDINAL type is not allowed to be used as a type argument +ResolutionErrors.dfy(2361,18): 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 'c' +ResolutionErrors.dfy(2362,18): 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 'c' +ResolutionErrors.dfy(2368,19): Error: a set comprehension involved in a predicate definition is not allowed to depend on the set of allocated references, but values of 'c' may contain references (see documentation for 'older' parameters) +ResolutionErrors.dfy(2374,37): Error: a const field definition is not allowed to depend on the set of allocated references +ResolutionErrors.dfy(2377,49): Error: a newtype definition is not allowed to depend on the set of allocated references +ResolutionErrors.dfy(2378,47): Error: a subset type definition is not allowed to depend on the set of allocated references +ResolutionErrors.dfy(2376,35): Error: a const field definition is not allowed to depend on the set of allocated references +ResolutionErrors.dfy(2383,32): Error: a predicate definition is not allowed to depend on the set of allocated references +ResolutionErrors.dfy(2389,41): Error: a const field definition is not allowed to depend on the set of allocated references +ResolutionErrors.dfy(2392,53): Error: a newtype definition is not allowed to depend on the set of allocated references +ResolutionErrors.dfy(2393,51): Error: a subset type definition is not allowed to depend on the set of allocated references +ResolutionErrors.dfy(2391,39): Error: a const field definition is not allowed to depend on the set of allocated references +ResolutionErrors.dfy(2398,36): Error: a predicate definition is not allowed to depend on the set of allocated references +ResolutionErrors.dfy(2405,25): Error: the value returned by an abstemious function must come from invoking a co-constructor +ResolutionErrors.dfy(2441,25): Error: the value returned by an abstemious function must come from invoking a co-constructor +ResolutionErrors.dfy(2448,32): Error: an abstemious function is allowed to invoke a codatatype destructor only on its parameters +ResolutionErrors.dfy(2453,12): Error: an abstemious function is allowed to codatatype-match only on its parameters +ResolutionErrors.dfy(2460,9): Error: an abstemious function is not only allowed to check codatatype equality +ResolutionErrors.dfy(2462,14): Error: an abstemious function is not only allowed to check codatatype equality +ResolutionErrors.dfy(2487,19): Error: type parameter 'G' (passed in as 'ORDINAL') to function call 'F' is not allowed to use ORDINAL +ResolutionErrors.dfy(2488,13): Error: type parameter 'G' (passed in as 'ORDINAL') to function call 'F'' is not allowed to use ORDINAL +ResolutionErrors.dfy(2489,13): Error: type parameter 'G' (passed in as '(char, ORDINAL)') to function call 'F'' is not allowed to use ORDINAL +ResolutionErrors.dfy(2490,18): Error: type parameter 'G' (passed in as 'ORDINAL') to the function 'F'' is not allowed to use ORDINAL +ResolutionErrors.dfy(2491,4): Error: type parameter 'G' (passed in as 'ORDINAL') to the lemma 'ParameterizedLemma' is not allowed to use ORDINAL +ResolutionErrors.dfy(2492,18): Error: type of bound variable 'r' ('ORDINAL') is not allowed to use type ORDINAL +ResolutionErrors.dfy(2493,18): Error: type of bound variable 'r' ('(ORDINAL, int)') is not allowed to use type ORDINAL +ResolutionErrors.dfy(2494,26): Error: type of bound variable 'r' ('ORDINAL') is not allowed to use type ORDINAL +ResolutionErrors.dfy(2495,17): Error: type of bound variable 'r' ('ORDINAL') is not allowed to use type ORDINAL +ResolutionErrors.dfy(2496,18): Error: type of bound variable 'r' ('ORDINAL') is not allowed to use type ORDINAL +ResolutionErrors.dfy(2497,24): Error: type of bound variable 'r' ('ORDINAL') is not allowed to use type ORDINAL +ResolutionErrors.dfy(2508,25): Error: an ORDINAL type is not allowed to be used as a type argument +ResolutionErrors.dfy(2509,17): Error: type of bound variable 'yt' ('ORDINAL') is not allowed to use type ORDINAL +ResolutionErrors.dfy(2506,8): Error: an ORDINAL type is not allowed to be used as a type argument +ResolutionErrors.dfy(2506,8): Error: an ORDINAL type is not allowed to be used as a type argument +ResolutionErrors.dfy(2505,8): Error: an ORDINAL type is not allowed to be used as a type argument +ResolutionErrors.dfy(2502,8): Error: an ORDINAL type is not allowed to be used as a type argument +ResolutionErrors.dfy(2500,8): Error: an ORDINAL type is not allowed to be used as a type argument ResolutionErrors.dfy(2499,8): Error: an ORDINAL type is not allowed to be used as a type argument ResolutionErrors.dfy(2498,8): Error: an ORDINAL type is not allowed to be used as a type argument +ResolutionErrors.dfy(2497,14): Error: an ORDINAL type is not allowed to be used as a type argument ResolutionErrors.dfy(2495,8): Error: an ORDINAL type is not allowed to be used as a type argument -ResolutionErrors.dfy(2493,8): Error: an ORDINAL type is not allowed to be used as a type argument -ResolutionErrors.dfy(2492,8): Error: an ORDINAL type is not allowed to be used as a type argument -ResolutionErrors.dfy(2491,8): Error: an ORDINAL type is not allowed to be used as a type argument -ResolutionErrors.dfy(2490,14): Error: an ORDINAL type is not allowed to be used as a type argument -ResolutionErrors.dfy(2488,8): Error: an ORDINAL type is not allowed to be used as a type argument -ResolutionErrors.dfy(2487,26): Error: type of bound variable 'r' ('ORDINAL') is not allowed to use type ORDINAL -ResolutionErrors.dfy(2486,18): Error: type of bound variable 'r' ('(ORDINAL, int)') is not allowed to use type ORDINAL -ResolutionErrors.dfy(2485,18): Error: type of bound variable 'r' ('ORDINAL') is not allowed to use type ORDINAL -ResolutionErrors.dfy(2484,4): Error: type parameter 'G' (passed in as 'ORDINAL') to the lemma 'ParameterizedLemma' is not allowed to use ORDINAL -ResolutionErrors.dfy(2478,8): Error: an ORDINAL type is not allowed to be used as a type argument -ResolutionErrors.dfy(2477,8): Error: an ORDINAL type is not allowed to be used as a type argument -ResolutionErrors.dfy(2617,23): Error: no label 'Treasure' in scope at this time -ResolutionErrors.dfy(2618,19): Error: no label 'WonderfulLabel' in scope at this time -ResolutionErrors.dfy(2620,23): Error: no label 'FutureLabel' in scope at this time -ResolutionErrors.dfy(2629,13): Error: no label 'Treasure' in scope at this time -ResolutionErrors.dfy(2630,13): Error: no label 'WonderfulLabel' in scope at this time -ResolutionErrors.dfy(2632,13): Error: no label 'FutureLabel' in scope at this time -ResolutionErrors.dfy(2641,13): Error: no label 'Treasure' in scope at this time -ResolutionErrors.dfy(2642,13): Error: no label 'WonderfulLabel' in scope at this time -ResolutionErrors.dfy(2644,13): Error: no label 'FutureLabel' in scope at this time -ResolutionErrors.dfy(2534,11): Error: no label 'L' in scope at this time -ResolutionErrors.dfy(2537,10): Error: label shadows a dominating label -ResolutionErrors.dfy(2545,10): Error: label shadows a dominating label -ResolutionErrors.dfy(2673,26): Error: type parameter (G) passed to method GimmieOne must support auto-initialization (got Yt) -ResolutionErrors.dfy(2686,50): Error: type of the receiver is not fully determined at this program point -ResolutionErrors.dfy(2712,11): Error: name of type (Cache) is used as a variable -ResolutionErrors.dfy(2712,17): Error: incorrect type for selection into ? (got X) -ResolutionErrors.dfy(2720,13): Warning: the quantifier has the form 'exists x :: A ==> B', which most often is a typo for 'exists x :: A && B'; if you think otherwise, rewrite as 'exists x :: (A ==> B)' or 'exists x :: !A || B' to suppress this warning -ResolutionErrors.dfy(2730,13): Warning: the quantifier has the form 'exists x :: A ==> B', which most often is a typo for 'exists x :: A && B'; if you think otherwise, rewrite as 'exists x :: (A ==> B)' or 'exists x :: !A || B' to suppress this warning -ResolutionErrors.dfy(2763,13): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function with 'function method') -ResolutionErrors.dfy(2764,13): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function with 'function method') -ResolutionErrors.dfy(2766,11): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(2787,4): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(2797,15): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function with 'function method') -ResolutionErrors.dfy(2798,22): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function with 'function method') +ResolutionErrors.dfy(2485,8): Error: an ORDINAL type is not allowed to be used as a type argument +ResolutionErrors.dfy(2484,8): Error: an ORDINAL type is not allowed to be used as a type argument +ResolutionErrors.dfy(2624,23): Error: no label 'Treasure' in scope at this time +ResolutionErrors.dfy(2625,19): Error: no label 'WonderfulLabel' in scope at this time +ResolutionErrors.dfy(2627,23): Error: no label 'FutureLabel' in scope at this time +ResolutionErrors.dfy(2636,13): Error: no label 'Treasure' in scope at this time +ResolutionErrors.dfy(2637,13): Error: no label 'WonderfulLabel' in scope at this time +ResolutionErrors.dfy(2639,13): Error: no label 'FutureLabel' in scope at this time +ResolutionErrors.dfy(2648,13): Error: no label 'Treasure' in scope at this time +ResolutionErrors.dfy(2649,13): Error: no label 'WonderfulLabel' in scope at this time +ResolutionErrors.dfy(2651,13): Error: no label 'FutureLabel' in scope at this time +ResolutionErrors.dfy(2541,11): Error: no label 'L' in scope at this time +ResolutionErrors.dfy(2544,10): Error: label shadows a dominating label +ResolutionErrors.dfy(2552,10): Error: label shadows a dominating label +ResolutionErrors.dfy(2680,26): Error: type parameter (G) passed to method GimmieOne must support auto-initialization (got Yt) +ResolutionErrors.dfy(2693,50): Error: type of the receiver is not fully determined at this program point +ResolutionErrors.dfy(2719,11): Error: name of type (Cache) is used as a variable +ResolutionErrors.dfy(2719,17): Error: incorrect type for selection into ? (got X) +ResolutionErrors.dfy(2727,13): Warning: the quantifier has the form 'exists x :: A ==> B', which most often is a typo for 'exists x :: A && B'; if you think otherwise, rewrite as 'exists x :: (A ==> B)' or 'exists x :: !A || B' to suppress this warning +ResolutionErrors.dfy(2737,13): Warning: the quantifier has the form 'exists x :: A ==> B', which most often is a typo for 'exists x :: A && B'; if you think otherwise, rewrite as 'exists x :: (A ==> B)' or 'exists x :: !A || B' to suppress this warning +ResolutionErrors.dfy(2770,13): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function with 'function method') +ResolutionErrors.dfy(2771,13): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function with 'function method') +ResolutionErrors.dfy(2773,11): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization. +ResolutionErrors.dfy(2794,4): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization. ResolutionErrors.dfy(2804,15): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function with 'function method') ResolutionErrors.dfy(2805,22): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function with 'function method') -ResolutionErrors.dfy(2822,23): Error: type of left argument to * (int) must agree with the result type (bool) -ResolutionErrors.dfy(2822,23): Error: type of * must be of a numeric type, bitvector type, or a set-like type (instead got bool) -ResolutionErrors.dfy(2821,13): Error: not resolving module 'V' because there were errors in resolving its nested module 'W' -ResolutionErrors.dfy(2831,21): Error: type of left argument to * (int) must agree with the result type (bool) -ResolutionErrors.dfy(2831,21): Error: type of * must be of a numeric type, bitvector type, or a set-like type (instead got bool) -ResolutionErrors.dfy(2830,11): Error: not resolving module 'V' because there were errors in resolving its nested module 'W' -ResolutionErrors.dfy(2817,9): Error: not resolving module 'ErrorsFromNestedModules' because there were errors in resolving its nested module 'U' -ResolutionErrors.dfy(2839,11): Error: duplicate name of top-level declaration: G -ResolutionErrors.dfy(2845,11): Error: duplicate name of top-level declaration: H -ResolutionErrors.dfy(2861,4): Error: ghost variables such as y are allowed only in specification contexts. y was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(2863,20): Error: ghost variables such as y are allowed only in specification contexts. y was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(2872,6): Error: ghost variables such as i are allowed only in specification contexts. i was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(2873,4): Error: ghost variables such as b are allowed only in specification contexts. b was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(2882,6): Error: ghost variables such as i are allowed only in specification contexts. i was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(2883,8): Error: ghost variables such as i are allowed only in specification contexts. i was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(2884,4): Error: ghost variables such as b are allowed only in specification contexts. b was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(2896,13): Error: expression is not allowed to refer to constant field x -ResolutionErrors.dfy(2898,22): Error: expression is not allowed to refer to constant field x -ResolutionErrors.dfy(2909,13): Error: arguments must be of a set or multiset type (got map) -ResolutionErrors.dfy(2919,4): Error: expect 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(2925,11): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'i' -ResolutionErrors.dfy(2926,21): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(2937,15): Error: RHS (of type X) not assignable to LHS (of type X) -ResolutionErrors.dfy(2941,10): Error: type of corresponding source/RHS (X) does not match type of bound variable (X) -ResolutionErrors.dfy(2969,16): Error: sequence update requires the value to have the element type of the sequence (got Trait) -ResolutionErrors.dfy(2973,11): Error: multiset update requires domain element to be of type Elem (got Trait) -ResolutionErrors.dfy(2978,13): Error: map update requires domain element to be of type Elem (got Trait) -ResolutionErrors.dfy(2980,18): Error: map update requires the value to have the range type Elem (got Trait) -ResolutionErrors.dfy(3005,5): Error: type parameter (F) passed to method Q must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 3000 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization) -ResolutionErrors.dfy(3008,5): Error: type parameter (F) passed to method Q must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 3000 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization) -ResolutionErrors.dfy(3009,5): Error: type parameter (G) passed to method P must support nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 3000 as 'Z(00)', which says it can only be instantiated with a nonempty type) -ResolutionErrors.dfy(3018,9): Error: type parameter (F) passed to function FQ must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 3013 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization) -ResolutionErrors.dfy(3021,9): Error: type parameter (F) passed to function FQ must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 3013 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization) -ResolutionErrors.dfy(3022,9): Error: type parameter (G) passed to function FP must support nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 3013 as 'Z(00)', which says it can only be instantiated with a nonempty type) -ResolutionErrors.dfy(3039,9): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function with 'function method') -ResolutionErrors.dfy(3040,9): Error: a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') -ResolutionErrors.dfy(3041,9): Error: a call to a least predicate is allowed only in specification contexts -ResolutionErrors.dfy(3042,9): Error: a call to a greatest predicate is allowed only in specification contexts -ResolutionErrors.dfy(3043,9): Error: a call to a twostate function is allowed only in specification contexts -ResolutionErrors.dfy(3044,9): Error: a call to a twostate predicate is allowed only in specification contexts -ResolutionErrors.dfy(3061,9): Error: function 'F0' expects 0 type arguments (got 1) -ResolutionErrors.dfy(3063,9): Error: function 'F2' expects 2 type arguments (got 1) -ResolutionErrors.dfy(3064,9): Error: function 'F0' expects 0 type arguments (got 2) -ResolutionErrors.dfy(3065,9): Error: function 'F1' expects 1 type argument (got 2) -ResolutionErrors.dfy(3073,4): Error: method 'M0' expects 0 type arguments (got 1) -ResolutionErrors.dfy(3075,4): Error: method 'M2' expects 2 type arguments (got 1) -ResolutionErrors.dfy(3076,4): Error: method 'M0' expects 0 type arguments (got 2) -ResolutionErrors.dfy(3077,4): Error: method 'M1' expects 1 type argument (got 2) -ResolutionErrors.dfy(3090,10): Error: ghost variables such as c are allowed only in specification contexts. c was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(3094,14): Error: ghost variables such as t are allowed only in specification contexts. t was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(3099,10): Error: ghost variables such as a' are allowed only in specification contexts. a' was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(3100,10): Error: ghost variables such as c' are allowed only in specification contexts. c' was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(3251,11): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) -ResolutionErrors.dfy(3252,11): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got PossiblyEmpty) -ResolutionErrors.dfy(3253,11): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got Nonempty) -ResolutionErrors.dfy(3254,11): Error: type parameter (T) passed to function MustSupportEquality must support equality (got NoEquality) -ResolutionErrors.dfy(3255,11): Error: type parameter (T) passed to function NoReferences must support no references (got Class?) -ResolutionErrors.dfy(3259,47): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) -ResolutionErrors.dfy(3260,12): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) -ResolutionErrors.dfy(3264,11): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) -ResolutionErrors.dfy(3265,11): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got PossiblyEmpty) -ResolutionErrors.dfy(3266,11): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got Nonempty) -ResolutionErrors.dfy(3267,11): Error: type parameter (T) passed to function MustSupportEquality must support equality (got NoEquality) -ResolutionErrors.dfy(3268,11): Error: type parameter (T) passed to function NoReferences must support no references (got Class?) -ResolutionErrors.dfy(3272,50): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) -ResolutionErrors.dfy(3273,12): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) -ResolutionErrors.dfy(3276,12): Error: type parameter (T) passed to function MustSupportEquality must support equality (got NoEquality) -ResolutionErrors.dfy(3280,12): Error: type parameter (T) passed to function MustSupportEquality must support equality (got NoEquality) -ResolutionErrors.dfy(3285,53): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) -ResolutionErrors.dfy(3288,63): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) -ResolutionErrors.dfy(3124,9): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) -ResolutionErrors.dfy(3129,9): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 3120 as 'Z(00)', which says it can only be instantiated with a nonempty type) -ResolutionErrors.dfy(3131,9): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got PossiblyEmpty) -ResolutionErrors.dfy(3132,9): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got Nonempty) -ResolutionErrors.dfy(3136,9): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 3120 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization) -ResolutionErrors.dfy(3140,9): Error: type parameter (T) passed to function MustSupportEquality must support equality (got NoEquality) -ResolutionErrors.dfy(3143,9): Error: type parameter (T) passed to function MustSupportEquality must support equality (got Z) (perhaps try declaring type parameter 'Z' on line 3120 as 'Z(==)', which says it can only be instantiated with a type that supports equality) -ResolutionErrors.dfy(3148,9): Error: type parameter (T) passed to function NoReferences must support no references (got Class?) -ResolutionErrors.dfy(3150,9): Error: type parameter (T) passed to function NoReferences must support no references (got Z) (perhaps try declaring type parameter 'Z' on line 3120 as 'Z(!new)', which says it can only be instantiated with a type that contains no references) -ResolutionErrors.dfy(3157,9): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) -ResolutionErrors.dfy(3163,9): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got PossiblyEmpty) -ResolutionErrors.dfy(3178,9): Error: type parameter (T) passed to function NoReferences must support no references (got Class?) -ResolutionErrors.dfy(3187,12): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 3185 as 'T(==)', which says it can only be instantiated with a type that supports equality) -ResolutionErrors.dfy(3189,7): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 3185 as 'T(==)', which says it can only be instantiated with a type that supports equality) -ResolutionErrors.dfy(3192,12): Error: type parameter (T) passed to function GetInt must support equality (got NoEquality) -ResolutionErrors.dfy(3194,7): Error: type parameter (T) passed to function GetInt must support equality (got NoEquality) -ResolutionErrors.dfy(3197,19): Error: type parameter (T) passed to function GetInt must support equality (got NoEquality) -ResolutionErrors.dfy(3205,13): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 3204 as 'T(==)', which says it can only be instantiated with a type that supports equality) -ResolutionErrors.dfy(3210,13): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 3204 as 'T(==)', which says it can only be instantiated with a type that supports equality) -ResolutionErrors.dfy(3212,23): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 3204 as 'T(==)', which says it can only be instantiated with a type that supports equality) -ResolutionErrors.dfy(3214,14): Error: type parameter 0 (T) passed to type QuadEq must support equality (got seq) -ResolutionErrors.dfy(3215,15): Error: type parameter 1 (U) passed to type QuadEq must support equality (got seq) -ResolutionErrors.dfy(3224,15): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 3221 as 'T(==)', which says it can only be instantiated with a type that supports equality) -ResolutionErrors.dfy(3233,15): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 3221 as 'T(==)', which says it can only be instantiated with a type that supports equality) -ResolutionErrors.dfy(3305,6): Error: ghost variables such as m are allowed only in specification contexts. m was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(3309,8): Error: non-ghost variable cannot be assigned a value that depends on a ghost -ResolutionErrors.dfy(3313,18): Error: ghost variables such as m are allowed only in specification contexts. m was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(3339,6): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) -ResolutionErrors.dfy(3345,6): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got PossiblyEmpty) -ResolutionErrors.dfy(3346,6): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got Nonempty) -ResolutionErrors.dfy(3353,6): Error: type parameter (T) passed to function MustSupportEquality must support equality (got NoEquality) -ResolutionErrors.dfy(3360,6): Error: type parameter (T) passed to function NoReferences must support no references (got Class?) -ResolutionErrors.dfy(3366,9): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) -ResolutionErrors.dfy(3372,9): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got PossiblyEmpty) -ResolutionErrors.dfy(3387,9): Error: type parameter (T) passed to function NoReferences must support no references (got Class?) -ResolutionErrors.dfy(3435,7): Error: ghost variables such as p are allowed only in specification contexts. p was inferred to be ghost based on its declaration or initialization. -ResolutionErrors.dfy(3449,21): Error: a loop in a hint is not allowed to use 'modifies' clauses +ResolutionErrors.dfy(2811,15): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function with 'function method') +ResolutionErrors.dfy(2812,22): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function with 'function method') +ResolutionErrors.dfy(2829,23): Error: type of left argument to * (int) must agree with the result type (bool) +ResolutionErrors.dfy(2829,23): Error: type of * must be of a numeric type, bitvector type, or a set-like type (instead got bool) +ResolutionErrors.dfy(2828,13): Error: not resolving module 'V' because there were errors in resolving its nested module 'W' +ResolutionErrors.dfy(2838,21): Error: type of left argument to * (int) must agree with the result type (bool) +ResolutionErrors.dfy(2838,21): Error: type of * must be of a numeric type, bitvector type, or a set-like type (instead got bool) +ResolutionErrors.dfy(2837,11): Error: not resolving module 'V' because there were errors in resolving its nested module 'W' +ResolutionErrors.dfy(2824,9): Error: not resolving module 'ErrorsFromNestedModules' because there were errors in resolving its nested module 'U' +ResolutionErrors.dfy(2846,11): Error: duplicate name of top-level declaration: G +ResolutionErrors.dfy(2852,11): Error: duplicate name of top-level declaration: H +ResolutionErrors.dfy(2868,4): Error: ghost variables such as y are allowed only in specification contexts. y was inferred to be ghost based on its declaration or initialization. +ResolutionErrors.dfy(2870,20): Error: ghost variables such as y are allowed only in specification contexts. y was inferred to be ghost based on its declaration or initialization. +ResolutionErrors.dfy(2879,6): Error: ghost variables such as i are allowed only in specification contexts. i was inferred to be ghost based on its declaration or initialization. +ResolutionErrors.dfy(2880,4): Error: ghost variables such as b are allowed only in specification contexts. b was inferred to be ghost based on its declaration or initialization. +ResolutionErrors.dfy(2889,6): Error: ghost variables such as i are allowed only in specification contexts. i was inferred to be ghost based on its declaration or initialization. +ResolutionErrors.dfy(2890,8): Error: ghost variables such as i are allowed only in specification contexts. i was inferred to be ghost based on its declaration or initialization. +ResolutionErrors.dfy(2891,4): Error: ghost variables such as b are allowed only in specification contexts. b was inferred to be ghost based on its declaration or initialization. +ResolutionErrors.dfy(2903,13): Error: expression is not allowed to refer to constant field x +ResolutionErrors.dfy(2905,22): Error: expression is not allowed to refer to constant field x +ResolutionErrors.dfy(2916,13): Error: arguments must be of a set or multiset type (got map) +ResolutionErrors.dfy(2926,4): Error: expect 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(2932,11): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'i' +ResolutionErrors.dfy(2933,21): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization. +ResolutionErrors.dfy(2944,15): Error: RHS (of type X) not assignable to LHS (of type X) +ResolutionErrors.dfy(2948,10): Error: type of corresponding source/RHS (X) does not match type of bound variable (X) +ResolutionErrors.dfy(2976,16): Error: sequence update requires the value to have the element type of the sequence (got Trait) +ResolutionErrors.dfy(2980,11): Error: multiset update requires domain element to be of type Elem (got Trait) +ResolutionErrors.dfy(2985,13): Error: map update requires domain element to be of type Elem (got Trait) +ResolutionErrors.dfy(2987,18): Error: map update requires the value to have the range type Elem (got Trait) +ResolutionErrors.dfy(3012,5): Error: type parameter (F) passed to method Q must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 3007 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization) +ResolutionErrors.dfy(3015,5): Error: type parameter (F) passed to method Q must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 3007 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization) +ResolutionErrors.dfy(3016,5): Error: type parameter (G) passed to method P must support nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 3007 as 'Z(00)', which says it can only be instantiated with a nonempty type) +ResolutionErrors.dfy(3025,9): Error: type parameter (F) passed to function FQ must support auto-initialization (got Y) (perhaps try declaring type parameter 'Y' on line 3020 as 'Y(0)', which says it can only be instantiated with a type that supports auto-initialization) +ResolutionErrors.dfy(3028,9): Error: type parameter (F) passed to function FQ must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 3020 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization) +ResolutionErrors.dfy(3029,9): Error: type parameter (G) passed to function FP must support nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 3020 as 'Z(00)', which says it can only be instantiated with a nonempty type) +ResolutionErrors.dfy(3046,9): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function with 'function method') +ResolutionErrors.dfy(3047,9): Error: a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') +ResolutionErrors.dfy(3048,9): Error: a call to a least predicate is allowed only in specification contexts +ResolutionErrors.dfy(3049,9): Error: a call to a greatest predicate is allowed only in specification contexts +ResolutionErrors.dfy(3050,9): Error: a call to a twostate function is allowed only in specification contexts +ResolutionErrors.dfy(3051,9): Error: a call to a twostate predicate is allowed only in specification contexts +ResolutionErrors.dfy(3068,9): Error: function 'F0' expects 0 type arguments (got 1) +ResolutionErrors.dfy(3070,9): Error: function 'F2' expects 2 type arguments (got 1) +ResolutionErrors.dfy(3071,9): Error: function 'F0' expects 0 type arguments (got 2) +ResolutionErrors.dfy(3072,9): Error: function 'F1' expects 1 type argument (got 2) +ResolutionErrors.dfy(3080,4): Error: method 'M0' expects 0 type arguments (got 1) +ResolutionErrors.dfy(3082,4): Error: method 'M2' expects 2 type arguments (got 1) +ResolutionErrors.dfy(3083,4): Error: method 'M0' expects 0 type arguments (got 2) +ResolutionErrors.dfy(3084,4): Error: method 'M1' expects 1 type argument (got 2) +ResolutionErrors.dfy(3097,10): Error: ghost variables such as c are allowed only in specification contexts. c was inferred to be ghost based on its declaration or initialization. +ResolutionErrors.dfy(3101,14): Error: ghost variables such as t are allowed only in specification contexts. t was inferred to be ghost based on its declaration or initialization. +ResolutionErrors.dfy(3106,10): Error: ghost variables such as a' are allowed only in specification contexts. a' was inferred to be ghost based on its declaration or initialization. +ResolutionErrors.dfy(3107,10): Error: ghost variables such as c' are allowed only in specification contexts. c' was inferred to be ghost based on its declaration or initialization. +ResolutionErrors.dfy(3258,11): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) +ResolutionErrors.dfy(3259,11): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got PossiblyEmpty) +ResolutionErrors.dfy(3260,11): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got Nonempty) +ResolutionErrors.dfy(3261,11): Error: type parameter (T) passed to function MustSupportEquality must support equality (got NoEquality) +ResolutionErrors.dfy(3262,11): Error: type parameter (T) passed to function NoReferences must support no references (got Class?) +ResolutionErrors.dfy(3266,47): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) +ResolutionErrors.dfy(3267,12): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) +ResolutionErrors.dfy(3271,11): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) +ResolutionErrors.dfy(3272,11): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got PossiblyEmpty) +ResolutionErrors.dfy(3273,11): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got Nonempty) +ResolutionErrors.dfy(3274,11): Error: type parameter (T) passed to function MustSupportEquality must support equality (got NoEquality) +ResolutionErrors.dfy(3275,11): Error: type parameter (T) passed to function NoReferences must support no references (got Class?) +ResolutionErrors.dfy(3279,50): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) +ResolutionErrors.dfy(3280,12): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) +ResolutionErrors.dfy(3283,12): Error: type parameter (T) passed to function MustSupportEquality must support equality (got NoEquality) +ResolutionErrors.dfy(3287,12): Error: type parameter (T) passed to function MustSupportEquality must support equality (got NoEquality) +ResolutionErrors.dfy(3292,53): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) +ResolutionErrors.dfy(3295,63): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) +ResolutionErrors.dfy(3131,9): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) +ResolutionErrors.dfy(3136,9): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got Z) (perhaps try declaring type parameter 'Z' on line 3127 as 'Z(00)', which says it can only be instantiated with a nonempty type) +ResolutionErrors.dfy(3138,9): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got PossiblyEmpty) +ResolutionErrors.dfy(3139,9): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got Nonempty) +ResolutionErrors.dfy(3143,9): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got Z) (perhaps try declaring type parameter 'Z' on line 3127 as 'Z(0)', which says it can only be instantiated with a type that supports auto-initialization) +ResolutionErrors.dfy(3147,9): Error: type parameter (T) passed to function MustSupportEquality must support equality (got NoEquality) +ResolutionErrors.dfy(3150,9): Error: type parameter (T) passed to function MustSupportEquality must support equality (got Z) (perhaps try declaring type parameter 'Z' on line 3127 as 'Z(==)', which says it can only be instantiated with a type that supports equality) +ResolutionErrors.dfy(3155,9): Error: type parameter (T) passed to function NoReferences must support no references (got Class?) +ResolutionErrors.dfy(3157,9): Error: type parameter (T) passed to function NoReferences must support no references (got Z) (perhaps try declaring type parameter 'Z' on line 3127 as 'Z(!new)', which says it can only be instantiated with a type that contains no references) +ResolutionErrors.dfy(3164,9): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) +ResolutionErrors.dfy(3170,9): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got PossiblyEmpty) +ResolutionErrors.dfy(3185,9): Error: type parameter (T) passed to function NoReferences must support no references (got Class?) +ResolutionErrors.dfy(3194,12): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 3192 as 'T(==)', which says it can only be instantiated with a type that supports equality) +ResolutionErrors.dfy(3196,7): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 3192 as 'T(==)', which says it can only be instantiated with a type that supports equality) +ResolutionErrors.dfy(3199,12): Error: type parameter (T) passed to function GetInt must support equality (got NoEquality) +ResolutionErrors.dfy(3201,7): Error: type parameter (T) passed to function GetInt must support equality (got NoEquality) +ResolutionErrors.dfy(3204,19): Error: type parameter (T) passed to function GetInt must support equality (got NoEquality) +ResolutionErrors.dfy(3212,13): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 3211 as 'T(==)', which says it can only be instantiated with a type that supports equality) +ResolutionErrors.dfy(3217,13): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 3211 as 'T(==)', which says it can only be instantiated with a type that supports equality) +ResolutionErrors.dfy(3219,23): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 3211 as 'T(==)', which says it can only be instantiated with a type that supports equality) +ResolutionErrors.dfy(3221,14): Error: type parameter 0 (T) passed to type QuadEq must support equality (got seq) +ResolutionErrors.dfy(3222,15): Error: type parameter 1 (U) passed to type QuadEq must support equality (got seq) +ResolutionErrors.dfy(3231,15): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 3228 as 'T(==)', which says it can only be instantiated with a type that supports equality) +ResolutionErrors.dfy(3240,15): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 3228 as 'T(==)', which says it can only be instantiated with a type that supports equality) +ResolutionErrors.dfy(3312,6): Error: ghost variables such as m are allowed only in specification contexts. m was inferred to be ghost based on its declaration or initialization. +ResolutionErrors.dfy(3316,8): Error: non-ghost variable cannot be assigned a value that depends on a ghost +ResolutionErrors.dfy(3320,18): Error: ghost variables such as m are allowed only in specification contexts. m was inferred to be ghost based on its declaration or initialization. +ResolutionErrors.dfy(3346,6): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) +ResolutionErrors.dfy(3352,6): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got PossiblyEmpty) +ResolutionErrors.dfy(3353,6): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got Nonempty) +ResolutionErrors.dfy(3360,6): Error: type parameter (T) passed to function MustSupportEquality must support equality (got NoEquality) +ResolutionErrors.dfy(3367,6): Error: type parameter (T) passed to function NoReferences must support no references (got Class?) +ResolutionErrors.dfy(3373,9): Error: type parameter (T) passed to function MustBeNonempty must support nonempty (got PossiblyEmpty) +ResolutionErrors.dfy(3379,9): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got PossiblyEmpty) +ResolutionErrors.dfy(3394,9): Error: type parameter (T) passed to function NoReferences must support no references (got Class?) +ResolutionErrors.dfy(3442,7): Error: ghost variables such as p are allowed only in specification contexts. p was inferred to be ghost based on its declaration or initialization. ResolutionErrors.dfy(3456,21): Error: a loop in a hint is not allowed to use 'modifies' clauses -ResolutionErrors.dfy(3485,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got multiset) -ResolutionErrors.dfy(3486,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got map) -ResolutionErrors.dfy(3487,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got map) -ResolutionErrors.dfy(3488,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got imap) -ResolutionErrors.dfy(3493,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got int) -ResolutionErrors.dfy(3494,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got set) -ResolutionErrors.dfy(3495,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got iset) -ResolutionErrors.dfy(3496,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got seq) -ResolutionErrors.dfy(3501,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got int -> int) -ResolutionErrors.dfy(3502,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got int -> object) -ResolutionErrors.dfy(3503,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got int -> set) -ResolutionErrors.dfy(3504,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got int -> seq) -ResolutionErrors.dfy(3505,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got set -> int) -ResolutionErrors.dfy(3524,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got map) -ResolutionErrors.dfy(3525,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got map) -ResolutionErrors.dfy(3526,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got imap) -ResolutionErrors.dfy(3531,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int) -ResolutionErrors.dfy(3532,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got set) -ResolutionErrors.dfy(3533,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got iset) -ResolutionErrors.dfy(3534,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got seq) -ResolutionErrors.dfy(3543,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> int) -ResolutionErrors.dfy(3544,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> object) -ResolutionErrors.dfy(3545,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> set) -ResolutionErrors.dfy(3546,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> iset) -ResolutionErrors.dfy(3547,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> seq) -ResolutionErrors.dfy(3548,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got set -> int) -ResolutionErrors.dfy(3549,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got bool -> multiset) -ResolutionErrors.dfy(3550,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got bool -> map) -ResolutionErrors.dfy(3565,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got map) -ResolutionErrors.dfy(3566,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got map) -ResolutionErrors.dfy(3567,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got imap) -ResolutionErrors.dfy(3572,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int) -ResolutionErrors.dfy(3573,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got set) -ResolutionErrors.dfy(3574,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got iset) -ResolutionErrors.dfy(3575,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got seq) -ResolutionErrors.dfy(3583,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> int) -ResolutionErrors.dfy(3584,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> object) -ResolutionErrors.dfy(3585,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> set) -ResolutionErrors.dfy(3586,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> iset) -ResolutionErrors.dfy(3587,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> seq) -ResolutionErrors.dfy(3588,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got set -> int) -ResolutionErrors.dfy(3589,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got bool -> multiset) -ResolutionErrors.dfy(3590,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got bool -> map) -ResolutionErrors.dfy(3606,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got map) -ResolutionErrors.dfy(3607,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got map) -ResolutionErrors.dfy(3608,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got imap) -ResolutionErrors.dfy(3614,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got int) -ResolutionErrors.dfy(3615,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got set) -ResolutionErrors.dfy(3616,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got iset) -ResolutionErrors.dfy(3617,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got seq) -ResolutionErrors.dfy(3626,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got int -> int) -ResolutionErrors.dfy(3627,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got int -> object) -ResolutionErrors.dfy(3631,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got set -> int) -ResolutionErrors.dfy(3633,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got bool -> map) -ResolutionErrors.dfy(3652,12): Error: a 'break break break continue' statement is allowed only in contexts with 4 enclosing loops, but the current context only has 3 -ResolutionErrors.dfy(3689,27): Error: continue label must designate a loop: X -ResolutionErrors.dfy(3691,27): Error: continue label must designate a loop: Y0 -ResolutionErrors.dfy(3693,27): Error: continue label must designate a loop: Y1 -ResolutionErrors.dfy(3695,27): Error: continue label must designate a loop: Z -ResolutionErrors.dfy(3705,4): Error: a non-labeled 'break' statement is allowed only in loops -ResolutionErrors.dfy(3709,4): Error: a non-labeled 'continue' statement is allowed only in loops -ResolutionErrors.dfy(3715,19): Error: a non-labeled 'break' statement is allowed only in loops -ResolutionErrors.dfy(3716,19): Error: a non-labeled 'continue' statement is allowed only in loops -ResolutionErrors.dfy(3718,28): Error: continue label must designate a loop: X -ResolutionErrors.dfy(3735,21): Error: a non-labeled 'break' statement is allowed only in loops -ResolutionErrors.dfy(3736,21): Error: a non-labeled 'continue' statement is allowed only in loops -ResolutionErrors.dfy(3737,27): Error: break label is undefined or not in scope: L -ResolutionErrors.dfy(3738,30): Error: continue label is undefined or not in scope: L -ResolutionErrors.dfy(3751,8): Error: ghost-context continue statement is not allowed to continue out of non-ghost loop -ResolutionErrors.dfy(3760,8): Error: ghost-context break statement is not allowed to break out of non-ghost loop -ResolutionErrors.dfy(3768,8): Error: ghost-context continue statement is not allowed to continue out of non-ghost loop -ResolutionErrors.dfy(3783,10): Error: ghost-context continue statement is not allowed to continue out of non-ghost loop -ResolutionErrors.dfy(3806,10): Error: ghost-context continue statement is not allowed to continue out of non-ghost loop -596 resolution/type errors detected in ResolutionErrors.dfy +ResolutionErrors.dfy(3463,21): Error: a loop in a hint is not allowed to use 'modifies' clauses +ResolutionErrors.dfy(3492,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got multiset) +ResolutionErrors.dfy(3493,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got map) +ResolutionErrors.dfy(3494,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got map) +ResolutionErrors.dfy(3495,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got imap) +ResolutionErrors.dfy(3500,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got int) +ResolutionErrors.dfy(3501,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got set) +ResolutionErrors.dfy(3502,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got iset) +ResolutionErrors.dfy(3503,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got seq) +ResolutionErrors.dfy(3508,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got int -> int) +ResolutionErrors.dfy(3509,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got int -> object) +ResolutionErrors.dfy(3510,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got int -> set) +ResolutionErrors.dfy(3511,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got int -> seq) +ResolutionErrors.dfy(3512,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got set -> int) +ResolutionErrors.dfy(3531,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got map) +ResolutionErrors.dfy(3532,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got map) +ResolutionErrors.dfy(3533,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got imap) +ResolutionErrors.dfy(3538,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int) +ResolutionErrors.dfy(3539,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got set) +ResolutionErrors.dfy(3540,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got iset) +ResolutionErrors.dfy(3541,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got seq) +ResolutionErrors.dfy(3550,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> int) +ResolutionErrors.dfy(3551,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> object) +ResolutionErrors.dfy(3552,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> set) +ResolutionErrors.dfy(3553,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> iset) +ResolutionErrors.dfy(3554,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> seq) +ResolutionErrors.dfy(3555,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got set -> int) +ResolutionErrors.dfy(3556,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got bool -> multiset) +ResolutionErrors.dfy(3557,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got bool -> map) +ResolutionErrors.dfy(3572,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got map) +ResolutionErrors.dfy(3573,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got map) +ResolutionErrors.dfy(3574,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got imap) +ResolutionErrors.dfy(3579,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int) +ResolutionErrors.dfy(3580,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got set) +ResolutionErrors.dfy(3581,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got iset) +ResolutionErrors.dfy(3582,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got seq) +ResolutionErrors.dfy(3590,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> int) +ResolutionErrors.dfy(3591,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> object) +ResolutionErrors.dfy(3592,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> set) +ResolutionErrors.dfy(3593,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> iset) +ResolutionErrors.dfy(3594,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> seq) +ResolutionErrors.dfy(3595,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got set -> int) +ResolutionErrors.dfy(3596,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got bool -> multiset) +ResolutionErrors.dfy(3597,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got bool -> map) +ResolutionErrors.dfy(3613,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got map) +ResolutionErrors.dfy(3614,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got map) +ResolutionErrors.dfy(3615,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got imap) +ResolutionErrors.dfy(3621,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got int) +ResolutionErrors.dfy(3622,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got set) +ResolutionErrors.dfy(3623,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got iset) +ResolutionErrors.dfy(3624,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got seq) +ResolutionErrors.dfy(3633,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got int -> int) +ResolutionErrors.dfy(3634,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got int -> object) +ResolutionErrors.dfy(3638,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got set -> int) +ResolutionErrors.dfy(3640,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got bool -> map) +ResolutionErrors.dfy(3659,12): Error: a 'break break break continue' statement is allowed only in contexts with 4 enclosing loops, but the current context only has 3 +ResolutionErrors.dfy(3696,27): Error: continue label must designate a loop: X +ResolutionErrors.dfy(3698,27): Error: continue label must designate a loop: Y0 +ResolutionErrors.dfy(3700,27): Error: continue label must designate a loop: Y1 +ResolutionErrors.dfy(3702,27): Error: continue label must designate a loop: Z +ResolutionErrors.dfy(3712,4): Error: a non-labeled 'break' statement is allowed only in loops +ResolutionErrors.dfy(3716,4): Error: a non-labeled 'continue' statement is allowed only in loops +ResolutionErrors.dfy(3722,19): Error: a non-labeled 'break' statement is allowed only in loops +ResolutionErrors.dfy(3723,19): Error: a non-labeled 'continue' statement is allowed only in loops +ResolutionErrors.dfy(3725,28): Error: continue label must designate a loop: X +ResolutionErrors.dfy(3742,21): Error: a non-labeled 'break' statement is allowed only in loops +ResolutionErrors.dfy(3743,21): Error: a non-labeled 'continue' statement is allowed only in loops +ResolutionErrors.dfy(3744,27): Error: break label is undefined or not in scope: L +ResolutionErrors.dfy(3745,30): Error: continue label is undefined or not in scope: L +ResolutionErrors.dfy(3758,8): Error: ghost-context continue statement is not allowed to continue out of non-ghost loop +ResolutionErrors.dfy(3767,8): Error: ghost-context break statement is not allowed to break out of non-ghost loop +ResolutionErrors.dfy(3775,8): Error: ghost-context continue statement is not allowed to continue out of non-ghost loop +ResolutionErrors.dfy(3790,10): Error: ghost-context continue statement is not allowed to continue out of non-ghost loop +ResolutionErrors.dfy(3813,10): Error: ghost-context continue statement is not allowed to continue out of non-ghost loop +ResolutionErrors.dfy(3869,13): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3869,18): Error: type of the receiver is not fully determined at this program point +ResolutionErrors.dfy(3878,13): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3878,18): Error: type of the receiver is not fully determined at this program point +ResolutionErrors.dfy(3896,22): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3864,22): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3864,27): Error: type of the receiver is not fully determined at this program point +ResolutionErrors.dfy(3870,12): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3870,17): Error: type of the receiver is not fully determined at this program point +ResolutionErrors.dfy(3868,25): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3868,30): Error: type of the receiver is not fully determined at this program point +ResolutionErrors.dfy(3875,22): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3875,27): Error: type of the receiver is not fully determined at this program point +ResolutionErrors.dfy(3879,12): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3879,17): Error: type of the receiver is not fully determined at this program point +ResolutionErrors.dfy(3877,22): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3877,27): Error: type of the receiver is not fully determined at this program point +ResolutionErrors.dfy(3881,23): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3881,28): Error: type of the receiver is not fully determined at this program point +ResolutionErrors.dfy(3895,32): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3898,29): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3897,33): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3900,29): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3899,35): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3885,23): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3885,28): Error: type of the receiver is not fully determined at this program point +ResolutionErrors.dfy(3904,21): Error: 'this' is not allowed in a 'static' context +ResolutionErrors.dfy(3904,26): Error: type of the receiver is not fully determined at this program point +623 resolution/type errors detected in ResolutionErrors.dfy diff --git a/Test/dafny0/RestrictedBoundedPools.dfy b/Test/dafny0/RestrictedBoundedPools.dfy index a6fcaaa731b..2ed2dcf3cb0 100644 --- a/Test/dafny0/RestrictedBoundedPools.dfy +++ b/Test/dafny0/RestrictedBoundedPools.dfy @@ -166,10 +166,6 @@ module OtherComprehensions { assert iset{} == iset o: OpaqueNoAlloc | R(o); // fine } - method M2() returns (s: iset) { - s := iset o: OpaqueNoAlloc | R(o); // error: not compilable (too awkward) - } - function F0(): int requires iset{} == iset o: Opaque | R(o) // error: may involve references { @@ -201,6 +197,16 @@ module OtherComprehensions { } } +module CompiledComprehensions { + predicate method R(y: Y) { true } + + type OpaqueNoAlloc(!new) + + method M2() returns (s: iset) { + s := iset o: OpaqueNoAlloc | R(o); // error: not compilable (too awkward) + } +} + module Allocated0 { class Cell { var data: int diff --git a/Test/dafny0/RestrictedBoundedPools.dfy.expect b/Test/dafny0/RestrictedBoundedPools.dfy.expect index 3185cd17fdd..cc902c20f14 100644 --- a/Test/dafny0/RestrictedBoundedPools.dfy.expect +++ b/Test/dafny0/RestrictedBoundedPools.dfy.expect @@ -7,18 +7,18 @@ RestrictedBoundedPools.dfy(113,4): Error: a forall expression involved in a pred RestrictedBoundedPools.dfy(123,4): Error: a forall expression involved in a predicate definition is not allowed to depend on the set of allocated references, but values of 'xs' may contain references (see documentation for 'older' parameters) RestrictedBoundedPools.dfy(133,4): Error: a forall expression involved in a predicate definition is not allowed to depend on the set of allocated references, but values of 'xs' may contain references (see documentation for 'older' parameters) RestrictedBoundedPools.dfy(155,17): Error: the result of a set comprehension must be finite, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o' -RestrictedBoundedPools.dfy(170,9): Error: iset 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' -RestrictedBoundedPools.dfy(174,23): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'o' may contain references (perhaps declare its type, 'Opaque', as 'Opaque(!new)') (see documentation for 'older' parameters) -RestrictedBoundedPools.dfy(186,23): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'xs' may contain references (see documentation for 'older' parameters) -RestrictedBoundedPools.dfy(192,17): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'xs' may contain references (see documentation for 'older' parameters) -RestrictedBoundedPools.dfy(198,23): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'xs' may contain references (see documentation for 'older' parameters) -RestrictedBoundedPools.dfy(218,9): 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 'c' -RestrictedBoundedPools.dfy(222,9): 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 'c' -RestrictedBoundedPools.dfy(236,18): Error: a function definition is not allowed to depend on the set of allocated references -RestrictedBoundedPools.dfy(241,4): Error: a function definition is not allowed to depend on the set of allocated references -RestrictedBoundedPools.dfy(246,4): Error: a twostate function definition is not allowed to depend on the set of allocated references +RestrictedBoundedPools.dfy(170,23): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'o' may contain references (perhaps declare its type, 'Opaque', as 'Opaque(!new)') (see documentation for 'older' parameters) +RestrictedBoundedPools.dfy(182,23): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'xs' may contain references (see documentation for 'older' parameters) +RestrictedBoundedPools.dfy(188,17): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'xs' may contain references (see documentation for 'older' parameters) +RestrictedBoundedPools.dfy(194,23): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'xs' may contain references (see documentation for 'older' parameters) +RestrictedBoundedPools.dfy(206,9): Error: iset 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' +RestrictedBoundedPools.dfy(224,9): 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 'c' +RestrictedBoundedPools.dfy(228,9): 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 'c' +RestrictedBoundedPools.dfy(242,18): Error: a function definition is not allowed to depend on the set of allocated references +RestrictedBoundedPools.dfy(247,4): Error: a function definition is not allowed to depend on the set of allocated references RestrictedBoundedPools.dfy(252,4): Error: a twostate function definition is not allowed to depend on the set of allocated references -RestrictedBoundedPools.dfy(271,18): 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 'x' -RestrictedBoundedPools.dfy(272,18): Error: map 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 'x' -RestrictedBoundedPools.dfy(286,4): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'zs' may contain references (see documentation for 'older' parameters) +RestrictedBoundedPools.dfy(258,4): Error: a twostate function definition is not allowed to depend on the set of allocated references +RestrictedBoundedPools.dfy(277,18): 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 'x' +RestrictedBoundedPools.dfy(278,18): Error: map 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 'x' +RestrictedBoundedPools.dfy(292,4): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'zs' may contain references (see documentation for 'older' parameters) 23 resolution/type errors detected in RestrictedBoundedPools.dfy diff --git a/Test/dafny0/SharedDestructorsResolution.dfy b/Test/dafny0/SharedDestructorsResolution.dfy index cdeca0474eb..48f992d6b3c 100644 --- a/Test/dafny0/SharedDestructorsResolution.dfy +++ b/Test/dafny0/SharedDestructorsResolution.dfy @@ -52,9 +52,9 @@ module Module1 { datatype Kt = Kt0(x: int) | - Kt1(ghost x: int) | // error: duplicated destructors must agree on ghost/non-ghost + Kt1(ghost x: int) | // (duplicated destructors must agree on ghost/non-ghost, but this is not report until a later pass; see Module2) Kt2(ghost g: int) | - Kt3(g: int) | // error: duplicated destructors must agree on ghost/non-ghost + Kt3(g: int) | // (duplicated destructors must agree on ghost/non-ghost, but this is not report until a later pass; see Module2) Kt4(k: Kt) | Kt5(k: SKt) | // fine, because SKt and Kt are synonyms Kt6(k: S'Kt) // fine, because S'Kt and Kt are synonyms @@ -98,3 +98,11 @@ module Module1 { | Same1(y: int, y: int) // error: duplicate destructor name in the same constructor | Same2(z: int, ghost z: bool) // error: duplicate destructor name in the same constructor } + +module Module2 { + datatype Kt = + Kt0(x: int) | + Kt1(ghost x: int) | // error: duplicated destructors must agree on ghost/non-ghost + Kt2(ghost g: int) | + Kt3(g: int) // error: duplicated destructors must agree on ghost/non-ghost +} diff --git a/Test/dafny0/SharedDestructorsResolution.dfy.expect b/Test/dafny0/SharedDestructorsResolution.dfy.expect index f949fee6e4b..78df34f29fd 100644 --- a/Test/dafny0/SharedDestructorsResolution.dfy.expect +++ b/Test/dafny0/SharedDestructorsResolution.dfy.expect @@ -13,8 +13,6 @@ SharedDestructorsResolution.dfy(46,31): Error: updated datatype members must bel SharedDestructorsResolution.dfy(97,6): Error: Duplicate use of deconstructor name in the same constructor: x SharedDestructorsResolution.dfy(98,6): Error: Duplicate use of deconstructor name in the same constructor: y SharedDestructorsResolution.dfy(99,6): Error: Duplicate use of deconstructor name in the same constructor: z -SharedDestructorsResolution.dfy(55,14): Error: shared destructors must agree on whether or not they are ghost, but 'x' is non-ghost in constructor 'Kt0' and ghost in constructor 'Kt1' -SharedDestructorsResolution.dfy(57,8): Error: shared destructors must agree on whether or not they are ghost, but 'g' is ghost in constructor 'Kt2' and non-ghost in constructor 'Kt3' SharedDestructorsResolution.dfy(64,8): Error: shared destructors must have the same type, but 'x' has type 'int' in constructor 'Lt0' and type 'real' in constructor 'Lt1' SharedDestructorsResolution.dfy(69,8): Error: shared destructors must have the same type, but 'y' has type 'A' in constructor 'Mt0' and type 'B' in constructor 'Mt2' SharedDestructorsResolution.dfy(71,8): Error: shared destructors must have the same type, but 'arr' has type 'array' in constructor 'Mt3' and type 'array' in constructor 'Mt4' @@ -22,4 +20,6 @@ SharedDestructorsResolution.dfy(72,8): Error: shared destructors must have the s SharedDestructorsResolution.dfy(76,8): Error: shared destructors must have the same type, but 'op' has type 'Opaque' in constructor 'Mt8' and type 'Opaque' in constructor 'Mt9' SharedDestructorsResolution.dfy(78,9): Error: shared destructors must have the same type, but 'oop' has type 'Opaque>' in constructor 'Mt10' and type 'Opaque>' in constructor 'Mt11' SharedDestructorsResolution.dfy(94,26): Error: shared destructors must have the same type, but 'u' has type 'int' in constructor 'Co2' and type 'real' in constructor 'Co3' +SharedDestructorsResolution.dfy(105,14): Error: shared destructors must agree on whether or not they are ghost, but 'x' is non-ghost in constructor 'Kt0' and ghost in constructor 'Kt1' +SharedDestructorsResolution.dfy(107,8): Error: shared destructors must agree on whether or not they are ghost, but 'g' is ghost in constructor 'Kt2' and non-ghost in constructor 'Kt3' 24 resolution/type errors detected in SharedDestructorsResolution.dfy diff --git a/Test/dafny0/TypeConstraints.dfy.expect b/Test/dafny0/TypeConstraints.dfy.expect index 213f1b3c9f4..a3a827c3842 100644 --- a/Test/dafny0/TypeConstraints.dfy.expect +++ b/Test/dafny0/TypeConstraints.dfy.expect @@ -30,7 +30,11 @@ module _System { * SCC at height 1: * RotateRight * SCC at height 0: + * array + * SCC at height 0: * nat + * SCC at height 0: + * object */ type string(==,0) = seq @@ -145,6 +149,8 @@ module Tests { * SCC at height 1: * CC.M * SCC at height 0: + * CC + * SCC at height 0: * CC.F * SCC at height 0: * CC.N @@ -403,6 +409,10 @@ module SimpleClassesAndTraits { * D * SCC at height 0: * K + * SCC at height 0: + * M + * SCC at height 0: + * R */ class C extends K, M { } /*-- non-null type @@ -535,6 +545,12 @@ module TraitStuff { * SCC at height 1: * Aggregate._ctor * SCC at height 0: + * Aggregate + * SCC at height 0: + * Motorized + * SCC at height 0: + * Part + * SCC at height 0: * PartX * SCC at height 0: * PartY @@ -790,8 +806,14 @@ module TypeArgumentPrintTests { * SCC at height 1: * Cl.M * SCC at height 0: + * A + * SCC at height 0: * A.F * SCC at height 0: + * B + * SCC at height 0: + * Cl + * SCC at height 0: * Tr */ trait Tr { } diff --git a/Test/dafny0/TypeConversions.dfy.expect b/Test/dafny0/TypeConversions.dfy.expect index da6ac8ce8c2..e74d8124f6e 100644 --- a/Test/dafny0/TypeConversions.dfy.expect +++ b/Test/dafny0/TypeConversions.dfy.expect @@ -8,7 +8,11 @@ module _System { * SCC at height 1: * RotateRight * SCC at height 0: + * array + * SCC at height 0: * nat + * SCC at height 0: + * object */ type string(==,0) = seq diff --git a/Test/dafny0/TypeConversionsCompile.dfy.expect b/Test/dafny0/TypeConversionsCompile.dfy.expect index d65f39bb479..863ecba2e2f 100644 --- a/Test/dafny0/TypeConversionsCompile.dfy.expect +++ b/Test/dafny0/TypeConversionsCompile.dfy.expect @@ -8,7 +8,11 @@ module _System { * SCC at height 1: * RotateRight * SCC at height 0: + * array + * SCC at height 0: * nat + * SCC at height 0: + * object */ type string(==,0) = seq diff --git a/Test/dafny2/CalcDefaultMainOperator.dfy.expect b/Test/dafny2/CalcDefaultMainOperator.dfy.expect index f8a27cff95c..ecc0861ad00 100644 --- a/Test/dafny2/CalcDefaultMainOperator.dfy.expect +++ b/Test/dafny2/CalcDefaultMainOperator.dfy.expect @@ -8,7 +8,11 @@ module _System { * SCC at height 1: * RotateRight * SCC at height 0: + * array + * SCC at height 0: * nat + * SCC at height 0: + * object */ type string(==,0) = seq diff --git a/Test/dafny4/git-issue228.dfy.expect b/Test/dafny4/git-issue228.dfy.expect index 143c72ca949..c2822c63989 100644 --- a/Test/dafny4/git-issue228.dfy.expect +++ b/Test/dafny4/git-issue228.dfy.expect @@ -67,7 +67,11 @@ module _System { * SCC at height 1: * RotateRight * SCC at height 0: + * array + * SCC at height 0: * nat + * SCC at height 0: + * object */ type string(==,0) = seq diff --git a/Test/git-issues/git-issue-1665.dfy.expect b/Test/git-issues/git-issue-1665.dfy.expect index 0a21a3c70d8..3d849808f94 100644 --- a/Test/git-issues/git-issue-1665.dfy.expect +++ b/Test/git-issues/git-issue-1665.dfy.expect @@ -8,7 +8,11 @@ module _System { * SCC at height 1: * RotateRight * SCC at height 0: + * array + * SCC at height 0: * nat + * SCC at height 0: + * object */ type string(==,0) = seq diff --git a/Test/git-issues/git-issue-2074.dfy.expect b/Test/git-issues/git-issue-2074.dfy.expect index dfee97eae30..f6450381332 100644 --- a/Test/git-issues/git-issue-2074.dfy.expect +++ b/Test/git-issues/git-issue-2074.dfy.expect @@ -1,6 +1,5 @@ git-issue-2074.dfy(5,6): Error: the type of this variable is underspecified git-issue-2074.dfy(5,25): Error: the type of this variable is underspecified git-issue-2074.dfy(5,21): Error: type of bound variable 'x' could not be determined; please specify the type explicitly -git-issue-2074.dfy(5,17): Error: the result of a set comprehension must be finite, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x' git-issue-2074.dfy(5,11): Error: type of bound variable 'st' could not be determined; please specify the type explicitly -5 resolution/type errors detected in git-issue-2074.dfy +4 resolution/type errors detected in git-issue-2074.dfy diff --git a/Test/git-issues/git-issue-2303.dfy b/Test/git-issues/git-issue-2303.dfy index 1c1ad4ae677..03c7bf5a1f9 100644 --- a/Test/git-issues/git-issue-2303.dfy +++ b/Test/git-issues/git-issue-2303.dfy @@ -1,5 +1,12 @@ // RUN: %exits-with 2 %dafny /compile:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" -newtype int0 = x | true // newtype's base type is not fully determined; add an explicit type for 'x' -const x: int0 := 0; // type for constant 'x' is 'int0', but its initialization value type is 'int' +module A { + newtype int0 = x | true // newtype's base type is not fully determined; add an explicit type for 'x' +} + +module B { + newtype int0 = x | true + const x: int0 := 0; // type for constant 'x' is 'int0', but its initialization value type is 'int' +} + diff --git a/Test/git-issues/git-issue-2303.dfy.expect b/Test/git-issues/git-issue-2303.dfy.expect index 1851b8a460f..7f709c06505 100644 --- a/Test/git-issues/git-issue-2303.dfy.expect +++ b/Test/git-issues/git-issue-2303.dfy.expect @@ -1,3 +1,3 @@ -git-issue-2303.dfy(4,8): Error: newtype's base type is not fully determined; add an explicit type for 'x' -git-issue-2303.dfy(5,6): Error: type for constant 'x' is 'int0', but its initialization value type is 'int' +git-issue-2303.dfy(5,10): Error: newtype's base type is not fully determined; add an explicit type for 'x' +git-issue-2303.dfy(10,8): Error: type for constant 'x' is 'int0', but its initialization value type is 'int' 2 resolution/type errors detected in git-issue-2303.dfy diff --git a/Test/git-issues/git-issue-283g.dfy b/Test/git-issues/git-issue-283g.dfy index e2783eb83d5..2e858df845f 100644 --- a/Test/git-issues/git-issue-283g.dfy +++ b/Test/git-issues/git-issue-283g.dfy @@ -28,11 +28,11 @@ datatype Cell = Cell(value: T) const Y := 1 // type of Y must be inferred method q() { var c: Cell; // note, type argument omitted; it will eventually be inferred - match c { - case Cell(Y) => // Y is int, so C is Cell + match c { // ERROR: expects Cell + case Cell(Y) => // ERROR: Y is int, which doesn't agree with the inferred type Cell of c case Cell(_) => // if Y is a const, then this case is not redundant } - c := Cell(1.2); // ERROR: type mismatch + c := Cell(1.2); // this determines the type of c to be Cell } method qq() { diff --git a/Test/git-issues/git-issue-283g.dfy.expect b/Test/git-issues/git-issue-283g.dfy.expect index 64d36aa0e79..927d2ee4ca0 100644 --- a/Test/git-issues/git-issue-283g.dfy.expect +++ b/Test/git-issues/git-issue-283g.dfy.expect @@ -1,7 +1,8 @@ git-issue-283g.dfy(20,21): Error: the type of the pattern (int) does not agree with the match expression (string) git-issue-283g.dfy(19,34): Error: arguments must have comparable types (got string and int) -git-issue-283g.dfy(35,7): Error: incorrect argument type for datatype constructor parameter 'value' (expected int, found real) +git-issue-283g.dfy(32,14): Error: the type of the pattern (int) does not agree with the match expression (real) +git-issue-283g.dfy(31,8): Error: arguments must have comparable types (got real and int) git-issue-283g.dfy(41,14): Error: the type of the pattern (int) does not agree with the match expression (real) git-issue-283g.dfy(40,8): Error: arguments must have comparable types (got real and int) git-issue-283g.dfy(50,4): Warning: this branch is redundant -5 resolution/type errors detected in git-issue-283g.dfy +6 resolution/type errors detected in git-issue-283g.dfy diff --git a/Test/git-issues/git-issue-3273.dfy b/Test/git-issues/git-issue-3273.dfy new file mode 100644 index 00000000000..01ee9b23537 --- /dev/null +++ b/Test/git-issues/git-issue-3273.dfy @@ -0,0 +1,54 @@ +// RUN: %exits-with 2 %dafny "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +iterator Iter(u: set) // this infers Y to be (==) + +method Repro() { + var iter: Iter; // error: K is not (==) +} + +iterator IterA() // this declares X to be (==) + +iterator IterB(u: set) // this infers Y to be (==) + +method Test() { + var a0: IterA; // error: K is not (==) + var a1: IterA; + var b0: IterB; // error: K is not (==) + var b1: IterB; + + var c0: IterA?; // error: K is not (==) + var c1: IterA?; + var d0: IterB?; // error: K is not (==) + var d1: IterB?; +} + +iterator EqIter(u: set, x: Y, y: Y) yields (eq: bool) + yield ensures eq == (x == y) + ensures false +{ + while true { + yield x == y; + } +} + +datatype Dt = Dt(a: int, ghost b: int) + +method Main() { + var d0 := Dt(0, 0); + var d1 := Dt(0, 1); + assert d0 != d1; // clearly + + // The following is error (but was not always detected by Dafny), because EqIter should take a (==) type argument. + var iter: EqIter
; // error: Dt is not an equality-supporting type + // The following does give an error, since the constructor lives in class EqIter whose + // type parameer has been inferred to be (==). + iter := new EqIter({}, d0, d1); // error: Dt is not an equality-supporting type + var more := iter.MoveNext(); + assert more; + assert iter.eq == (d0 == d1) == false; // according to the yield-ensures clause + print iter.eq, "\n"; + if iter.eq { + var ugh := 1 / 0; // according to the verifier, we never get here + } +} diff --git a/Test/git-issues/git-issue-3273.dfy.expect b/Test/git-issues/git-issue-3273.dfy.expect new file mode 100644 index 00000000000..384655391be --- /dev/null +++ b/Test/git-issues/git-issue-3273.dfy.expect @@ -0,0 +1,9 @@ +git-issue-3273.dfy(7,12): Error: type parameter (Y) passed to type Iter must support equality (got K) (perhaps try declaring type parameter 'K' on line 6 as 'K(==)', which says it can only be instantiated with a type that supports equality) +git-issue-3273.dfy(15,10): Error: type parameter (X) passed to type IterA must support equality (got K) (perhaps try declaring type parameter 'K' on line 14 as 'K(==)', which says it can only be instantiated with a type that supports equality) +git-issue-3273.dfy(17,10): Error: type parameter (Y) passed to type IterB must support equality (got K) (perhaps try declaring type parameter 'K' on line 14 as 'K(==)', which says it can only be instantiated with a type that supports equality) +git-issue-3273.dfy(20,10): Error: type parameter (X) passed to type IterA must support equality (got K) (perhaps try declaring type parameter 'K' on line 14 as 'K(==)', which says it can only be instantiated with a type that supports equality) +git-issue-3273.dfy(22,10): Error: type parameter (Y) passed to type IterB must support equality (got K) (perhaps try declaring type parameter 'K' on line 14 as 'K(==)', which says it can only be instantiated with a type that supports equality) +git-issue-3273.dfy(43,12): Error: type parameter (Y) passed to type EqIter must support equality (got Dt) +git-issue-3273.dfy(46,14): Error: type parameter (Y) passed to type EqIter must support equality (got Dt) +git-issue-3273.dfy(46,21): Error: set argument type must support equality (got Dt) +8 resolution/type errors detected in git-issue-3273.dfy diff --git a/Test/traits/TraitResolution0.dfy.expect b/Test/traits/TraitResolution0.dfy.expect index 38f519c72c7..3b513263201 100644 --- a/Test/traits/TraitResolution0.dfy.expect +++ b/Test/traits/TraitResolution0.dfy.expect @@ -8,7 +8,11 @@ module _System { * SCC at height 1: * RotateRight * SCC at height 0: + * array + * SCC at height 0: * nat + * SCC at height 0: + * object */ type string(==,0) = seq @@ -123,6 +127,8 @@ module M0 { * SCC at height 1: * Cl.M * SCC at height 0: + * Cl + * SCC at height 0: * Tr * SCC at height 0: * Tr.F @@ -157,6 +163,8 @@ module M1 { * M * SCC at height 0: * Cl + * SCC at height 0: + * Tr */ trait Tr { var w: X @@ -184,6 +192,8 @@ module M2 { * SCC at height 0: * Cl * SCC at height 0: + * Tr + * SCC at height 0: * Tr.F */ trait Tr { @@ -215,8 +225,12 @@ module P0 { * SCC at height 1: * Cl.M * SCC at height 0: + * Cl + * SCC at height 0: * Tr * SCC at height 0: + * TrX + * SCC at height 0: * TrX.F */ trait TrX { @@ -254,6 +268,10 @@ module P1 { * M * SCC at height 0: * Cl + * SCC at height 0: + * Tr + * SCC at height 0: + * TrX */ trait TrX { var w: X @@ -286,6 +304,10 @@ module P2 { * SCC at height 0: * Cl * SCC at height 0: + * Tr + * SCC at height 0: + * TrX + * SCC at height 0: * TrX.F */ trait TrX { diff --git a/docs/dev/news/3284.fix b/docs/dev/news/3284.fix new file mode 100644 index 00000000000..75ec3586e57 --- /dev/null +++ b/docs/dev/news/3284.fix @@ -0,0 +1 @@ +Any `(==)` inferred for a type parameter of an iterator is now also inferred for the corresponding non-null iterator type.