diff --git a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs index e1b5386d54..4d44483214 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs @@ -12,7 +12,7 @@ public class IdPattern : ExtendedPattern, IHasUsages { public bool HasParenthesis { get; } public String Id; public PreType PreType; - public Type Type; // This is the syntactic type, ExtendedPatterns dissapear during resolution. + public Type Type; // This is the syntactic type, ExtendedPatterns disappear during resolution. public IVariable BoundVar { get; set; } public List Arguments; // null if just an identifier; possibly empty argument list if a constructor call public LiteralExpr ResolvedLit; // null if just an identifier @@ -108,8 +108,9 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti }; BoundVar = localVariable; } else { - var boundVar = new BoundVar(Tok, Id, Type); - boundVar.IsGhost = isGhost; + var boundVar = new BoundVar(Tok, Id, Type) { + IsGhost = isGhost + }; BoundVar = boundVar; } diff --git a/Source/DafnyCore/AST/SubstitutingCloner.cs b/Source/DafnyCore/AST/SubstitutingCloner.cs index d1d7f18abb..e00dba7379 100644 --- a/Source/DafnyCore/AST/SubstitutingCloner.cs +++ b/Source/DafnyCore/AST/SubstitutingCloner.cs @@ -3,18 +3,18 @@ namespace Microsoft.Dafny; class SubstitutingCloner : Cloner { - private readonly Dictionary substitutions; + private readonly Dictionary substitutions; - public SubstitutingCloner(Dictionary substitutions, bool cloneResolvedFields) + public SubstitutingCloner(Dictionary substitutions, bool cloneResolvedFields) : base(false, cloneResolvedFields) { this.substitutions = substitutions; } public override Expression CloneExpr(Expression expr) { if (expr is IdentifierExpr identifierExpr) { - if (substitutions.TryGetValue(identifierExpr.Var, out var substitution)) { - // TODO consider using the code from Substitutor - return substitution; + if (substitutions.TryGetValue(identifierExpr.Var, out var variableReplacement)) { + // TODO consider using the code from Substituter + return new IdentifierExpr(expr.tok, variableReplacement); } } diff --git a/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs b/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs index cb01301960..416d2923b9 100644 --- a/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs +++ b/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs @@ -711,15 +711,17 @@ private PatternPath LetBind(IdPattern var, Expression genExpr, PatternPath bodyP return stmtPath; } - var caseLocal = new LocalVariable(var.RangeToken, name, type, isGhost); - caseLocal.type = type; + var caseLocal = new LocalVariable(var.RangeToken, name, type, isGhost) { + type = type + }; var casePattern = new CasePattern(caseLocal.RangeToken.EndToken, caseLocal); casePattern.AssembleExpr(new List()); - var caseLet = new VarDeclPattern(caseLocal.RangeToken, casePattern, expr, false); - caseLet.IsGhost = isGhost; + var caseLet = new VarDeclPattern(caseLocal.RangeToken, casePattern, expr, false) { + IsGhost = isGhost + }; - var substitutions = new Dictionary() { - { var.BoundVar, new IdentifierExpr(var.BoundVar.Tok, caseLocal)} + var substitutions = new Dictionary() { + { var.BoundVar, caseLocal } }; var cloner = new SubstitutingCloner(substitutions, true); diff --git a/Source/DafnyCore/Resolver/ExpressionTester.cs b/Source/DafnyCore/Resolver/ExpressionTester.cs index 01a732a3a5..4059a53857 100644 --- a/Source/DafnyCore/Resolver/ExpressionTester.cs +++ b/Source/DafnyCore/Resolver/ExpressionTester.cs @@ -7,7 +7,7 @@ namespace Microsoft.Dafny; public class ExpressionTester { - private DafnyOptions options; + private readonly DafnyOptions options; private bool ReportErrors => reporter != null; [CanBeNull] private readonly ErrorReporter reporter; // if null, no errors will be reported @@ -26,25 +26,35 @@ private ExpressionTester([CanBeNull] ModuleResolver resolver, [CanBeNull] ErrorR this.options = options; } - // Static call to CheckIsCompilable + /// + /// Determines whether or not "expr" is compilable, and returns the answer. + /// If "resolver" is non-null and "expr" is not compilable, then an error is reported. + /// Also, updates various bookkeeping information (see instance method CheckIsCompilable for more details). + /// public static bool CheckIsCompilable(DafnyOptions options, [CanBeNull] ModuleResolver resolver, Expression expr, ICodeContext codeContext) { return new ExpressionTester(resolver, resolver?.Reporter, options).CheckIsCompilable(expr, codeContext, true); } - public static bool CheckIsCompilable(ModuleResolver resolver, ErrorReporter reporter, Expression expr, ICodeContext codeContext) { - return new ExpressionTester(resolver, reporter, reporter.Options).CheckIsCompilable(expr, codeContext, true); + /// + /// Checks that "expr" is compilable and report an error if it is not. + /// Also, updates various bookkeeping information (see instance method CheckIsCompilable for more details). + /// + public static void CheckIsCompilable(ModuleResolver resolver, ErrorReporter reporter, Expression expr, ICodeContext codeContext) { + new ExpressionTester(resolver, reporter, reporter.Options).CheckIsCompilable(expr, codeContext, true); } - public void ReportError(ErrorId errorId, Expression e, string msg, params object[] args) { + private void ReportError(ErrorId errorId, Expression e, string msg, params object[] args) { reporter?.Error(MessageSource.Resolver, errorId, e, msg, args); } - public void ReportError(ErrorId errorId, IToken t, string msg, params object[] args) { + private void ReportError(ErrorId errorId, IToken t, string msg, params object[] args) { reporter?.Error(MessageSource.Resolver, errorId, t, msg, args); } /// - /// Checks that "expr" is compilable and reports an error if it is not. + /// Determines and returns whether or not "expr" is compilable. + /// If it is not, it calls ReportError. (Note, whether or not ReportError reports an error depends on if "reporter" is non-null.) + /// /// Also, updates bookkeeping information for the verifier to record the fact that "expr" is to be compiled. /// For example, this bookkeeping information keeps track of if the constraint of a let-such-that expression /// must determine the value uniquely. @@ -219,23 +229,21 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext, bool i } else if (expr is LetExpr letExpr) { if (letExpr.Exact) { Contract.Assert(letExpr.LHSs.Count == letExpr.RHSs.Count); - var i = 0; - foreach (var ee in letExpr.RHSs) { + for (var i = 0; i < letExpr.RHSs.Count; i++) { + var rhs = letExpr.RHSs[i]; var lhs = letExpr.LHSs[i]; // Make LHS vars ghost if the RHS is a ghost - if (UsesSpecFeatures(ee)) { + if (UsesSpecFeatures(rhs)) { foreach (var bv in lhs.Vars) { if (!bv.IsGhost) { bv.MakeGhost(); - isCompilable = false; } } } if (!lhs.Vars.All(bv => bv.IsGhost)) { - isCompilable = CheckIsCompilable(ee, codeContext) && isCompilable; + isCompilable = CheckIsCompilable(rhs, codeContext) && isCompilable; } - i++; } isCompilable = CheckIsCompilable(letExpr.Body, codeContext, insideBranchesOnly) && isCompilable; } else { @@ -247,13 +255,19 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext, bool i isCompilable = CheckIsCompilable(letExpr.Body, codeContext, insideBranchesOnly) && isCompilable; // fill in bounds for this to-be-compiled let-such-that expression - Contract.Assert(letExpr.RHSs.Count == 1); // if we got this far, the resolver will have checked this condition successfully + Contract.Assert(letExpr.RHSs.Count == 1); // if we got this far, the resolver will have checked this condition successfully var constraint = letExpr.RHSs[0]; if (resolver != null) { letExpr.Constraint_Bounds = ModuleResolver.DiscoverBestBounds_MultipleVars(letExpr.BoundVars.ToList(), constraint, true); } } return isCompilable; + + } else if (expr is NestedMatchExpr nestedMatchExpr) { + foreach (var kase in nestedMatchExpr.Cases) { + MakeGhostAsNeeded(kase.Pat, false); + } + } else if (expr is LambdaExpr lambdaExpr) { return CheckIsCompilable(lambdaExpr.Body, codeContext); } else if (expr is ComprehensionExpr comprehensionExpr) { @@ -653,6 +667,30 @@ static void MakeGhostAsNeeded(CasePattern arg, DatatypeDestructor d) { } } + public static void MakeGhostAsNeeded(ExtendedPattern extendedPattern, bool inGhostContext) { + if (extendedPattern is DisjunctivePattern disjunctivePattern) { + foreach (var alternative in disjunctivePattern.Alternatives) { + MakeGhostAsNeeded(alternative, inGhostContext); + } + } else if (extendedPattern is LitPattern) { + // nothing to do + } else if (extendedPattern is IdPattern idPattern) { + if (idPattern.BoundVar != null) { + if (inGhostContext && !idPattern.BoundVar.IsGhost) { + idPattern.BoundVar.MakeGhost(); + } + } else if (idPattern.Ctor != null) { + var argumentCount = idPattern.Ctor.Formals.Count; + Contract.Assert(argumentCount == (idPattern.Arguments?.Count ?? 0)); + for (var i = 0; i < argumentCount; i++) { + MakeGhostAsNeeded(idPattern.Arguments[i], inGhostContext || idPattern.Ctor.Formals[i].IsGhost); + } + } + } else { + Contract.Assert(false); // unexpected ExtendedPattern + } + } + /// /// Return the first ghost constructor listed in a case, or null, if there is none. /// diff --git a/Source/DafnyCore/Resolver/GhostInterestVisitor.cs b/Source/DafnyCore/Resolver/GhostInterestVisitor.cs index b9bd972044..386f3b85c4 100644 --- a/Source/DafnyCore/Resolver/GhostInterestVisitor.cs +++ b/Source/DafnyCore/Resolver/GhostInterestVisitor.cs @@ -448,6 +448,10 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC .OfType().Any(idPattern => idPattern.Ctor != null && idPattern.Ctor.IsGhost); nestedMatchStmt.IsGhost = mustBeErasable || ExpressionTester.UsesSpecFeatures(nestedMatchStmt.Source) || hasGhostPattern; + foreach (var kase in nestedMatchStmt.Cases) { + ExpressionTester.MakeGhostAsNeeded(kase.Pat, nestedMatchStmt.IsGhost); + } + if (!mustBeErasable && nestedMatchStmt.IsGhost) { reporter.Info(MessageSource.Resolver, nestedMatchStmt.Tok, "ghost match"); } diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 595a20eabc..ed5954e67e 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -3040,7 +3040,7 @@ public void CheckIsLvalue(Expression lhs, ResolutionContext resolutionContext) { ConstrainSubtypeRelation(ResolvedArrayType(ll.Seq.tok, 1, new InferredTypeProxy(), resolutionContext, true), ll.Seq.Type, ll.Seq, "LHS of array assignment must denote an array element (found {0})", ll.Seq.Type); if (!ll.SelectOne) { - reporter.Error(MessageSource.Resolver, ll.Seq, "cannot assign to a range of array elements (try the 'forall' statement)"); + reporter.Error(MessageSource.Resolver, ll, "cannot assign to a range of array elements (try the 'forall' statement)"); } } else if (lhs is MultiSelectExpr) { // nothing to check; this can only denote an array element diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs b/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs index f26cc72f43..900b0b6fcf 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs @@ -49,7 +49,10 @@ public DPreType ApproximateReceiverType(PreType preType, [CanBeNull] string memb if (preType is DPreType dPreType) { return dPreType; } - var proxy = (PreTypeProxy)preType; + if (preType is not PreTypeProxy proxy) { + // preType could be a PreTypePlaceholder, resulting from an error somewhere + return null; + } var approximateReceiverType = ApproximateReceiverTypeViaBounds(proxy, memberName, out var subProxies); if (approximateReceiverType != null) { diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index 44f304cc53..35eb02dece 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -162,10 +162,10 @@ public void ResolveExpression(Expression expr, ResolutionContext resolutionConte if (e.PreType is PreTypePlaceholderModule) { ReportError(e.tok, "name of module ({0}) is used as a variable", e.Name); - e.ResetTypeAssignment(); // the rest of type checking assumes actual types + ResetTypeAssignment(e); // the rest of type checking assumes actual types } else if (e.PreType is PreTypePlaceholderType) { ReportError(e.tok, "name of type ({0}) is used as a variable", e.Name); - e.ResetTypeAssignment(); // the rest of type checking assumes actual types + ResetTypeAssignment(e); // the rest of type checking assumes actual types } } else if (expr is ExprDotName) { @@ -173,10 +173,10 @@ public void ResolveExpression(Expression expr, ResolutionContext resolutionConte ResolveDotSuffix(e, true, null, resolutionContext, false); if (e.PreType is PreTypePlaceholderModule) { ReportError(e.tok, "name of module ({0}) is used as a variable", e.SuffixName); - e.ResetTypeAssignment(); // the rest of type checking assumes actual types + ResetTypeAssignment(e); // the rest of type checking assumes actual types } else if (e.PreType is PreTypePlaceholderType) { ReportError(e.tok, "name of type ({0}) is used as a variable", e.SuffixName); - e.ResetTypeAssignment(); // the rest of type checking assumes actual types + ResetTypeAssignment(e); // the rest of type checking assumes actual types } } else if (expr is ApplySuffix applySuffix) { @@ -282,9 +282,9 @@ public void ResolveExpression(Expression expr, ResolutionContext resolutionConte var familyDeclName = ancestorPreType?.Decl.Name; if (familyDeclName == PreType.TypeNameSeq) { var elementPreType = ancestorPreType.Arguments[0]; - ConstrainToIntFamilyOrBitvector(e.Index.PreType, e.Index.tok, "sequence update requires integer- or bitvector-based index (got {0})"); + ConstrainToIntFamilyOrBitvector(e.Index.PreType, e.Index.tok, "sequence update requires integer- or bitvector-based index (got {1})"); AddSubtypeConstraint(elementPreType, e.Value.PreType, e.Value.tok, - "sequence update requires the value to have the element type of the sequence (got {0})"); + "sequence update requires the value to have the element type of the sequence (got {1})"); return true; } else if (familyDeclName is PreType.TypeNameMap or PreType.TypeNameImap) { var domainPreType = ancestorPreType.Arguments[0]; diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs index 99d769fe8e..6b204f89f9 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs @@ -544,7 +544,9 @@ private void ResolveCalc(CalcStmt s, ResolutionContext resolutionContext) { #if SOON // reuse the error object if we're on the dummy line; this prevents a duplicate error message #endif - AddSubtypeConstraint(linePreType, e1.PreType, e1.tok, "all lines in a calculation must have the same type (got {1} after {0})"); + if (i < s.Lines.Count - 1) { + AddSubtypeConstraint(linePreType, e1.PreType, e1.tok, "all lines in a calculation must have the same type (got {1} after {0})"); + } var step = (s.StepOps[i - 1] ?? s.Op).StepExpr(e0, e1); // Use custom line operator ResolveExpression(step, resolutionContext); s.Steps.Add(step); @@ -1308,7 +1310,7 @@ public void CheckIsLvalue(Expression lhs, ResolutionContext resolutionContext) { var arrayType = resolver.ResolvedArrayType(ll.Seq.tok, 1, new InferredTypeProxy(), resolutionContext, true); AddSubtypeConstraint(Type2PreType(arrayType), ll.Seq.PreType, ll.Seq.tok, "LHS of array assignment must denote an array element (found {1})"); if (!ll.SelectOne) { - ReportError(ll.Seq, "cannot assign to a range of array elements (try the 'forall' statement)"); + ReportError(ll, "cannot assign to a range of array elements (try the 'forall' statement)"); } } else if (lhs is MultiSelectExpr) { // nothing to check; this can only denote an array element diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs index cf612d7274..3da77c20b1 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs @@ -174,6 +174,15 @@ public PreType CreatePreTypeProxy(string description = null) { return proxy; } + /// + /// This method can be used when .PreType has been found to be erroneous and its current value + /// would be unexpected by the rest of the resolver. This method then sets .Type and .PreType to neutral values. + /// + void ResetTypeAssignment(Expression expr) { + expr.PreType = CreatePreTypeProxy(); + expr.ResetTypeAssignment(); + } + public enum Type2PreTypeOption { GoodForInference, GoodForPrinting, GoodForBoth } public PreType Type2PreType(Type type, string description = null, Type2PreTypeOption option = Type2PreTypeOption.GoodForBoth) { @@ -884,14 +893,14 @@ void ComputePreTypeMethod(Method method) { // bitvector types. That's now handled in a different way, which does not use SelfType. } else { ComputePreTypeFunction(function); - if (function is ExtremePredicate extremePredicate) { - ComputePreTypeFunction(extremePredicate.PrefixPredicate); + if (function is ExtremePredicate { PrefixPredicate: { } prefixPredicate }) { + ComputePreTypeFunction(prefixPredicate); } } } else if (declaration is Method method) { ComputePreTypeMethod(method); - if (method is ExtremeLemma extremeLemma) { - ComputePreTypeMethod(extremeLemma.PrefixLemma); + if (method is ExtremeLemma { PrefixLemma: { } prefixLemma }) { + ComputePreTypeMethod(prefixLemma); } } else { Contract.Assert(false); // unexpected declaration diff --git a/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs b/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs index b1ce6ecb2f..b297073cfa 100644 --- a/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs +++ b/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs @@ -143,8 +143,8 @@ private void CheckMember(MemberDecl member) { CheckStatement(method.Body, context); } if (errorCount == ErrorCount) { - if (method is ExtremeLemma extremeLemma) { - CheckMember(extremeLemma.PrefixLemma); + if (method is ExtremeLemma { PrefixLemma: { } prefixLemma }) { + CheckMember(prefixLemma); } } @@ -158,8 +158,8 @@ private void CheckMember(MemberDecl member) { CheckExpression(function.Body, context); } if (errorCount == ErrorCount) { - if (function is ExtremePredicate extremePredicate) { - CheckMember(extremePredicate.PrefixPredicate); + if (function is ExtremePredicate { PrefixPredicate: { } prefixPredicate }) { + CheckMember(prefixPredicate); } else if (function.ByMethodDecl != null) { CheckMember(function.ByMethodDecl); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors0.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors0.dfy index 8e1312b5fa..27bad58ea5 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors0.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors0.dfy @@ -1,5 +1,5 @@ -// RUN: %exits-with 2 %verify --allow-axioms "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" + module Misc { //Should not verify, as ghost loops should not be allowed to diverge. @@ -126,7 +126,7 @@ module HereAreMoreGhostTests { case Cons(dd, tt, gg) => r := G(dd, dd); // fine r := G(dd, gg); // fine - r := G(gg, gg); // error: cannot pass ghost 'gg' as non-ghost parameter to 'G' + } var dd; dd := GhostDt.Nil(g); // fine @@ -139,11 +139,11 @@ module HereAreMoreGhostTests { function G(x: int, ghost y: int): int { y // error: cannot return a ghost from a non-ghost function } - function H(dt: GhostDt): int { - match dt - case Nil(gg) => gg // error: cannot return a ghost from a non-ghost function - case Cons(dd, tt, gg) => dd + gg // error: ditto - } + + + + + method N(x: int, ghost y: int) returns (r: int) { r := x; } @@ -514,3 +514,30 @@ module MiscAgain { // ghost -- and rightly so, since an assume is used } } // MiscAgain + +// ----- One more phase of HereAreMoreGhostTests from above + +module HereAreMoreGhostTests' { + datatype GhostDt = + Nil(ghost extraInfo: int) | + Cons(data: int, tail: GhostDt, ghost moreInfo: int) + + method M(dt: GhostDt) returns (r: int) { + ghost var g := 5; + match (dt) { + case Nil(gg) => + case Cons(dd, tt, gg) => + r := G(dd, dd); // fine + r := G(dd, gg); // fine + r := G(gg, gg); // error: cannot pass ghost 'gg' as non-ghost parameter to 'G' + } + } + + function G(x: int, ghost y: int): int + + function H(dt: GhostDt): int { + match dt + case Nil(gg) => gg // error: cannot return a ghost from a non-ghost function + case Cons(dd, tt, gg) => dd + gg // error: ditto + } +} // HereAreMoreGhostTests' diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors0.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors0.dfy.expect index 28211560fe..a9030966c2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors0.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors0.dfy.expect @@ -22,11 +22,8 @@ ResolutionErrors0.dfy(116,11): Error: ghost variables such as g are allowed only ResolutionErrors0.dfy(117,11): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) ResolutionErrors0.dfy(121,13): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization. ResolutionErrors0.dfy(122,12): Error: actual out-parameter is required to be a ghost variable -ResolutionErrors0.dfy(129,17): Error: ghost variables such as gg are allowed only in specification contexts. gg was inferred to be ghost based on its declaration or initialization. ResolutionErrors0.dfy(133,25): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization. ResolutionErrors0.dfy(140,6): Error: ghost variables such as y are allowed only in specification contexts. y was inferred to be ghost based on its declaration or initialization. -ResolutionErrors0.dfy(144,23): Error: ghost variables such as gg are allowed only in specification contexts. gg was inferred to be ghost based on its declaration or initialization. -ResolutionErrors0.dfy(145,37): Error: ghost variables such as gg are allowed only in specification contexts. gg was inferred to be ghost based on its declaration or initialization. ResolutionErrors0.dfy(154,12): Error: only ghost methods can be called from this context ResolutionErrors0.dfy(244,29): Error: ghost-context break statement is not allowed to break out of non-ghost structure ResolutionErrors0.dfy(267,14): Error: ghost-context break statement is not allowed to break out of non-ghost loop @@ -67,4 +64,7 @@ ResolutionErrors0.dfy(445,10): Error: a hint is not allowed to make heap updates ResolutionErrors0.dfy(447,10): Error: a hint is not allowed to update a variable it doesn't declare ResolutionErrors0.dfy(468,4): Error: More than one anonymous constructor ResolutionErrors0.dfy(481,15): Error: class Lamb does not have an anonymous constructor +ResolutionErrors0.dfy(532,15): Error: ghost variables such as gg are allowed only in specification contexts. gg was inferred to be ghost based on its declaration or initialization. +ResolutionErrors0.dfy(540,21): Error: ghost variables such as gg are allowed only in specification contexts. gg was inferred to be ghost based on its declaration or initialization. +ResolutionErrors0.dfy(541,35): Error: ghost variables such as gg are allowed only in specification contexts. gg was inferred to be ghost based on its declaration or initialization. 68 resolution/type errors detected in ResolutionErrors0.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors0.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors0.dfy.refresh.expect new file mode 100644 index 0000000000..a41828425e --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors0.dfy.refresh.expect @@ -0,0 +1,65 @@ +ResolutionErrors0.dfy(323,33): Warning: constructors no longer need 'this' to be listed in modifies clauses +ResolutionErrors0.dfy(13,18): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating +ResolutionErrors0.dfy(25,13): Error: array selection requires an array2? (got array3) +ResolutionErrors0.dfy(27,13): Error: array selection requires an array4? (got array) +ResolutionErrors0.dfy(26,14): Error: element selection requires a sequence, array, multiset, or map (got array3) +ResolutionErrors0.dfy(57,16): Error: accessing member 'X' requires an instance expression +ResolutionErrors0.dfy(58,9): Error: unresolved identifier: F +ResolutionErrors0.dfy(59,16): Error: accessing member 'F' requires an instance expression +ResolutionErrors0.dfy(60,9): Error: unresolved identifier: G +ResolutionErrors0.dfy(62,9): Error: unresolved identifier: M +ResolutionErrors0.dfy(63,16): Error: accessing member 'M' requires an instance expression +ResolutionErrors0.dfy(64,9): Error: unresolved identifier: N +ResolutionErrors0.dfy(67,10): Error: non-function expression (of type int) is called with parameters +ResolutionErrors0.dfy(68,16): Error: member 'z' does not exist in non-null type 'Global' +ResolutionErrors0.dfy(51,15): Error: 'this' is not allowed in a 'static' context +ResolutionErrors0.dfy(88,16): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny') +ResolutionErrors0.dfy(93,16): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David') +ResolutionErrors0.dfy(94,16): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David') +ResolutionErrors0.dfy(96,16): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David') +ResolutionErrors0.dfy(98,20): Error: wrong number of arguments (datatype constructor 'David' expects 1, got 2) +ResolutionErrors0.dfy(116,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. +ResolutionErrors0.dfy(117,11): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword) +ResolutionErrors0.dfy(121,13): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization. +ResolutionErrors0.dfy(122,12): Error: actual out-parameter is required to be a ghost variable +ResolutionErrors0.dfy(133,25): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization. +ResolutionErrors0.dfy(140,6): Error: ghost variables such as y are allowed only in specification contexts. y was inferred to be ghost based on its declaration or initialization. +ResolutionErrors0.dfy(154,12): Error: only ghost methods can be called from this context +ResolutionErrors0.dfy(244,29): Error: ghost-context break statement is not allowed to break out of non-ghost structure +ResolutionErrors0.dfy(267,14): Error: ghost-context break statement is not allowed to break out of non-ghost loop +ResolutionErrors0.dfy(281,14): Error: ghost-context break statement is not allowed to break out of non-ghost loop +ResolutionErrors0.dfy(286,10): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) +ResolutionErrors0.dfy(306,12): Error: label shadows an enclosing label +ResolutionErrors0.dfy(311,10): Error: duplicate label +ResolutionErrors0.dfy(313,10): Error: label shadows a dominating label +ResolutionErrors0.dfy(329,11): Error: a constructor is allowed to be called only when an object is being allocated +ResolutionErrors0.dfy(343,18): Error: arguments must have comparable types (got int and DTD_List) +ResolutionErrors0.dfy(344,18): Error: arguments must have comparable types (got DTD_List and int) +ResolutionErrors0.dfy(345,27): Error: arguments must have comparable types (got bool and int) +ResolutionErrors0.dfy(358,17): Error: ghost variables such as b are allowed only in specification contexts. b was inferred to be ghost based on its declaration or initialization. +ResolutionErrors0.dfy(384,11): Error: RHS (of type int) not assignable to LHS (of type bool) +ResolutionErrors0.dfy(385,21): Error: integer literal used as if it had type bool +ResolutionErrors0.dfy(396,19): Error: integer literal used as if it had type _T0 +ResolutionErrors0.dfy(397,15): Error: integer literal used as if it had type _T0 +ResolutionErrors0.dfy(406,8): Error: all lines in a calculation must have the same type (got int after bool) +ResolutionErrors0.dfy(410,8): Error: all lines in a calculation must have the same type (got int after bool) +ResolutionErrors0.dfy(405,8): 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) +ResolutionErrors0.dfy(405,8): Error: arguments must have comparable types (got bool and int) +ResolutionErrors0.dfy(405,8): Error: arguments must have comparable types (got bool and int) +ResolutionErrors0.dfy(409,8): Error: arguments must have comparable types (got bool and int) +ResolutionErrors0.dfy(409,8): Error: arguments must have comparable types (got bool and int) +ResolutionErrors0.dfy(413,8): Error: type of ==> must be a boolean (got int) +ResolutionErrors0.dfy(414,12): Error: type of ==> must be a boolean (got int) +ResolutionErrors0.dfy(415,12): Error: type of ==> must be a boolean (got int) +ResolutionErrors0.dfy(413,8): Error: type of ==> must be a boolean (got int) +ResolutionErrors0.dfy(419,12): Error: type of ==> must be a boolean (got int) +ResolutionErrors0.dfy(418,8): Error: type of ==> must be a boolean (got int) +ResolutionErrors0.dfy(443,13): Error: in a hint, calls are allowed only to lemmas +ResolutionErrors0.dfy(445,10): Error: a hint is not allowed to make heap updates +ResolutionErrors0.dfy(447,10): Error: a hint is not allowed to update a variable it doesn't declare +ResolutionErrors0.dfy(468,4): Error: More than one anonymous constructor +ResolutionErrors0.dfy(481,15): Error: class 'Lamb' does not have an anonymous constructor +ResolutionErrors0.dfy(532,15): Error: ghost variables such as gg are allowed only in specification contexts. gg was inferred to be ghost based on its declaration or initialization. +ResolutionErrors0.dfy(540,21): Error: ghost variables such as gg are allowed only in specification contexts. gg was inferred to be ghost based on its declaration or initialization. +ResolutionErrors0.dfy(541,35): Error: ghost variables such as gg are allowed only in specification contexts. gg was inferred to be ghost based on its declaration or initialization. +63 resolution/type errors detected in ResolutionErrors0.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors1.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors1.dfy index 38f344cf63..86d1c05b71 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors1.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors1.dfy @@ -1,5 +1,5 @@ -// RUN: %exits-with 2 %verify --allow-axioms "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --allow-axioms + // ------------------------ inferred type arguments ---------------------------- @@ -156,7 +156,7 @@ module UnderspecifiedTypes { var n, p, T0 :| 12 <= n && n in T0 && 10 <= p && p in T0 && T0 <= S && p % 2 != n % 2; var T1 :| 12 in T1 && T1 <= S; var T2 :| T2 <= S && 12 in T2; - var T3 :| 120 in T3; // error: underspecified type + var T3'0: set :| 120 in T3'0; var T3'1: multiset :| 120 in T3'1; var T3'2: map :| 120 in T3'2; @@ -166,6 +166,12 @@ module UnderspecifiedTypes { } } +module UnderspecifiedTypes' { + method M() { + var T3 :| 120 in T3; // error: underspecified type + } +} + // ------------------------- lemmas ------------------------------ module MiscLemma { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors1.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors1.dfy.expect index 9e74df5f97..8f2753f626 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors1.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors1.dfy.expect @@ -16,6 +16,6 @@ ResolutionErrors1.dfy(141,14): Error: new allocation not supported in aggregate ResolutionErrors1.dfy(148,14): Error: a forall statement is not allowed to use 'new' ResolutionErrors1.dfy(148,11): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression ResolutionErrors1.dfy(164,26): Error: second argument to "in" must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got bool) -ResolutionErrors1.dfy(159,18): Error: second argument to "in" must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got ?) -ResolutionErrors1.dfy(177,13): Error: lemmas are not allowed to have modifies clauses +ResolutionErrors1.dfy(171,18): Error: second argument to "in" must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got ?) +ResolutionErrors1.dfy(183,13): Error: lemmas are not allowed to have modifies clauses 20 resolution/type errors detected in ResolutionErrors1.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors1.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors1.dfy.refresh.expect new file mode 100644 index 0000000000..14a17a6e76 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors1.dfy.refresh.expect @@ -0,0 +1,19 @@ +ResolutionErrors1.dfy(20,7): Error: RHS (of type List) not assignable to LHS (of type List) (covariant type parameter 'T' would require B :> A) +ResolutionErrors1.dfy(25,7): Error: RHS (of type List) not assignable to LHS (of type List) (covariant type parameter 'T' would require B :> A) +ResolutionErrors1.dfy(39,23): Error: type of case bodies do not agree (found Tree<_T1, _T0>, previous types Tree<_T0, _T1>) (covariant type parameter 'A' would require _T0 :> _T1) +ResolutionErrors1.dfy(39,23): Error: type of case bodies do not agree (found Tree<_T1, _T0>, previous types Tree<_T0, _T1>) (covariant type parameter 'B' would require _T1 :> _T0) +ResolutionErrors1.dfy(51,30): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree +ResolutionErrors1.dfy(66,20): Error: unresolved identifier: w +ResolutionErrors1.dfy(86,33): Error: arguments must have comparable types (got ?8 and ?7) +ResolutionErrors1.dfy(99,13): Error: a lemma is not allowed to use 'new' +ResolutionErrors1.dfy(100,9): Error: a lemma is not allowed to use 'new' +ResolutionErrors1.dfy(109,16): Error: only ghost methods can be called from this context +ResolutionErrors1.dfy(116,15): Error: only ghost methods can be called from this context +ResolutionErrors1.dfy(126,17): Error: a hint is not allowed to use 'new' +ResolutionErrors1.dfy(141,14): Error: new allocation not supported in aggregate assignments +ResolutionErrors1.dfy(148,14): Error: a forall statement is not allowed to use 'new' +ResolutionErrors1.dfy(148,11): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +ResolutionErrors1.dfy(164,26): Error: second argument to 'in' must be a set, a multiset, a sequence with elements of type ?43, or a map with domain ?43 (instead got bool) +ResolutionErrors1.dfy(171,21): Error: the type of this variable is underspecified +ResolutionErrors1.dfy(183,13): Error: lemmas are not allowed to have modifies clauses +18 resolution/type errors detected in ResolutionErrors1.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors2.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors2.dfy index 7ebfece166..205a7387d6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors2.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors2.dfy @@ -1,5 +1,5 @@ -// RUN: %exits-with 2 %verify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" + // ------------------------- statements in expressions ------------------------------ @@ -226,6 +226,26 @@ module ModifyStatementClass_More { } module LhsLvalue { + datatype MyRecord = Make(x: int, y: int) + + method MyMethod() returns (w: int) + + method M0() returns (mySeq: seq) { + mySeq[0] := 5; // error: cannot assign to a sequence element + } + + method M1() returns (mySeq: seq) { + mySeq[0] := MyMethod(); // error: cannot assign to a sequence element + } + + method M2() returns (mySeq: seq) { + mySeq[0..4] := 5; // error: cannot assign to a range + } + + method M3() returns (mySeq: seq) { + mySeq[0..4] := MyMethod(); // error: cannot assign to a range + } + method M() { var mySeq: seq; @@ -233,23 +253,15 @@ module LhsLvalue { var b := new int[100, 200]; var c := new MyRecord[29]; - mySeq[0] := 5; // error: cannot assign to a sequence element - mySeq[0] := MyMethod(); // error: ditto a[0] := 5; a[0] := MyMethod(); b[20, 18] := 5; b[20, 18] := MyMethod(); c[25].x := 5; // error: cannot assign to a destructor c[25].x := MyMethod(); // error: ditto - mySeq[0..4] := 5; // error: cannot assign to a range - mySeq[0..4] := MyMethod(); // error: ditto a[0..4] := 5; // error: cannot assign to a range a[0..4] := MyMethod(); // error: ditto } - - datatype MyRecord = Make(x: int, y: int) - - method MyMethod() returns (w: int) } // ------------------- dirty loops ------------------- diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors2.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors2.dfy.expect index 00c2486635..9144d802d5 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors2.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors2.dfy.expect @@ -15,59 +15,59 @@ ResolutionErrors2.dfy(188,14): Error: in a ghost context, only ghost fields can ResolutionErrors2.dfy(197,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) ResolutionErrors2.dfy(208,20): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) ResolutionErrors2.dfy(220,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) -ResolutionErrors2.dfy(242,10): Error: LHS of assignment must denote a mutable field -ResolutionErrors2.dfy(243,10): Error: LHS of assignment must denote a mutable field -ResolutionErrors2.dfy(244,9): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors2.dfy(245,9): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors2.dfy(246,5): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors2.dfy(247,5): Error: cannot assign to a range of array elements (try the 'forall' statement) -ResolutionErrors2.dfy(236,4): Error: LHS of array assignment must denote an array element (found seq) -ResolutionErrors2.dfy(237,4): Error: LHS of array assignment must denote an array element (found seq) -ResolutionErrors2.dfy(260,11): Error: unresolved identifier: s -ResolutionErrors2.dfy(279,18): Error: member '3' does not exist in datatype '_tuple#3' -ResolutionErrors2.dfy(279,28): Error: member 'x' does not exist in datatype '_tuple#2' -ResolutionErrors2.dfy(278,18): Error: condition is expected to be of type bool, but is int -ResolutionErrors2.dfy(272,39): Error: RHS (of type (int, real, int)) not assignable to LHS (of type (int, real, int, real)) -ResolutionErrors2.dfy(271,34): Error: RHS (of type (int, int, real)) not assignable to LHS (of type (int, real, int)) (covariant type parameter 1 would require int <: real) -ResolutionErrors2.dfy(271,34): Error: RHS (of type (int, int, real)) not assignable to LHS (of type (int, real, int)) (covariant type parameter 2 would require real <: int) -ResolutionErrors2.dfy(303,12): Error: type of left argument to % (int) must agree with the result type (real) -ResolutionErrors2.dfy(303,12): Error: arguments to % must be integer-numeric or bitvector types (got real) -ResolutionErrors2.dfy(302,19): Error: type of right argument to / (int) must agree with the result type (real) -ResolutionErrors2.dfy(330,11): Error: Wrong number of type arguments (2 instead of 1) passed to non-null type: array3 -ResolutionErrors2.dfy(331,11): Error: Wrong number of type arguments (2 instead of 1) passed to non-null type: C -ResolutionErrors2.dfy(342,7): Error: duplicate name of top-level declaration: BadSyn2 -ResolutionErrors2.dfy(341,7): Related location -ResolutionErrors2.dfy(339,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List -ResolutionErrors2.dfy(340,17): Error: Type or type parameter is not declared in this scope: badName (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) -ResolutionErrors2.dfy(341,22): Error: Type or type parameter is not declared in this scope: X (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) -ResolutionErrors2.dfy(348,7): Error: type-synonym cycle: A -> A -ResolutionErrors2.dfy(352,7): Error: cycle among redirecting types (newtypes, subset types, type synonyms): A -> B -> A -ResolutionErrors2.dfy(357,7): Error: cycle among redirecting types (newtypes, subset types, type synonyms): A -> B -> A -ResolutionErrors2.dfy(367,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed -ResolutionErrors2.dfy(364,8): Error: class 'C' with fields without known initializers, like 'a' of type 'A', must declare a constructor -ResolutionErrors2.dfy(371,7): Error: cycle among redirecting types (newtypes, subset types, type synonyms): A -> B -> A -ResolutionErrors2.dfy(377,7): Error: cycle among redirecting types (newtypes, subset types, type synonyms): A -> B -> A -ResolutionErrors2.dfy(383,7): Error: type-synonym cycle: A -> A -ResolutionErrors2.dfy(390,25): Error: unresolved identifier: x -ResolutionErrors2.dfy(393,22): Error: unresolved identifier: x -ResolutionErrors2.dfy(396,25): Error: unresolved identifier: x -ResolutionErrors2.dfy(398,21): Error: unresolved identifier: x -ResolutionErrors2.dfy(400,21): Error: unresolved identifier: x -ResolutionErrors2.dfy(403,21): Error: unresolved identifier: x -ResolutionErrors2.dfy(410,35): Error: Wrong number of type arguments (2 instead of 1) passed to abstract type: P -ResolutionErrors2.dfy(422,13): Error: Type or type parameter is not declared in this scope: BX (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) -ResolutionErrors2.dfy(432,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require bool = int) -ResolutionErrors2.dfy(437,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require B = A) -ResolutionErrors2.dfy(442,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require int = A) -ResolutionErrors2.dfy(443,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require A = int) -ResolutionErrors2.dfy(448,13): Error: arguments must have comparable types (got P and P) -ResolutionErrors2.dfy(449,13): Error: arguments must have comparable types (got P and P) -ResolutionErrors2.dfy(450,13): Error: arguments must have comparable types (got P and P) -ResolutionErrors2.dfy(461,13): Error: new can be applied only to class types (got JJ) -ResolutionErrors2.dfy(469,37): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'o' (of type 'object') may contain references (see documentation for 'older' parameters) -ResolutionErrors2.dfy(470,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' (of type 'object') may contain references (see documentation for 'older' parameters) -ResolutionErrors2.dfy(477,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' -ResolutionErrors2.dfy(485,15): Error: arguments to / must be numeric or bitvector types (got set) -ResolutionErrors2.dfy(492,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 -ResolutionErrors2.dfy(507,16): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating +ResolutionErrors2.dfy(234,4): Error: LHS of array assignment must denote an array element (found seq) +ResolutionErrors2.dfy(238,4): Error: LHS of array assignment must denote an array element (found seq) +ResolutionErrors2.dfy(242,9): Error: cannot assign to a range of array elements (try the 'forall' statement) +ResolutionErrors2.dfy(246,9): Error: cannot assign to a range of array elements (try the 'forall' statement) +ResolutionErrors2.dfy(260,10): Error: LHS of assignment must denote a mutable field +ResolutionErrors2.dfy(261,10): Error: LHS of assignment must denote a mutable field +ResolutionErrors2.dfy(262,5): Error: cannot assign to a range of array elements (try the 'forall' statement) +ResolutionErrors2.dfy(263,5): Error: cannot assign to a range of array elements (try the 'forall' statement) +ResolutionErrors2.dfy(272,11): Error: unresolved identifier: s +ResolutionErrors2.dfy(291,18): Error: member '3' does not exist in datatype '_tuple#3' +ResolutionErrors2.dfy(291,28): Error: member 'x' does not exist in datatype '_tuple#2' +ResolutionErrors2.dfy(290,18): Error: condition is expected to be of type bool, but is int +ResolutionErrors2.dfy(284,39): Error: RHS (of type (int, real, int)) not assignable to LHS (of type (int, real, int, real)) +ResolutionErrors2.dfy(283,34): Error: RHS (of type (int, int, real)) not assignable to LHS (of type (int, real, int)) (covariant type parameter 1 would require int <: real) +ResolutionErrors2.dfy(283,34): Error: RHS (of type (int, int, real)) not assignable to LHS (of type (int, real, int)) (covariant type parameter 2 would require real <: int) +ResolutionErrors2.dfy(315,12): Error: type of left argument to % (int) must agree with the result type (real) +ResolutionErrors2.dfy(315,12): Error: arguments to % must be integer-numeric or bitvector types (got real) +ResolutionErrors2.dfy(314,19): Error: type of right argument to / (int) must agree with the result type (real) +ResolutionErrors2.dfy(342,11): Error: Wrong number of type arguments (2 instead of 1) passed to non-null type: array3 +ResolutionErrors2.dfy(343,11): Error: Wrong number of type arguments (2 instead of 1) passed to non-null type: C +ResolutionErrors2.dfy(354,7): Error: duplicate name of top-level declaration: BadSyn2 +ResolutionErrors2.dfy(353,7): Related location +ResolutionErrors2.dfy(351,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List +ResolutionErrors2.dfy(352,17): Error: Type or type parameter is not declared in this scope: badName (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +ResolutionErrors2.dfy(353,22): Error: Type or type parameter is not declared in this scope: X (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +ResolutionErrors2.dfy(360,7): Error: type-synonym cycle: A -> A +ResolutionErrors2.dfy(364,7): Error: cycle among redirecting types (newtypes, subset types, type synonyms): A -> B -> A +ResolutionErrors2.dfy(369,7): Error: cycle among redirecting types (newtypes, subset types, type synonyms): A -> B -> A +ResolutionErrors2.dfy(379,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed +ResolutionErrors2.dfy(376,8): Error: class 'C' with fields without known initializers, like 'a' of type 'A', must declare a constructor +ResolutionErrors2.dfy(383,7): Error: cycle among redirecting types (newtypes, subset types, type synonyms): A -> B -> A +ResolutionErrors2.dfy(389,7): Error: cycle among redirecting types (newtypes, subset types, type synonyms): A -> B -> A +ResolutionErrors2.dfy(395,7): Error: type-synonym cycle: A -> A +ResolutionErrors2.dfy(402,25): Error: unresolved identifier: x +ResolutionErrors2.dfy(405,22): Error: unresolved identifier: x +ResolutionErrors2.dfy(408,25): Error: unresolved identifier: x +ResolutionErrors2.dfy(410,21): Error: unresolved identifier: x +ResolutionErrors2.dfy(412,21): Error: unresolved identifier: x +ResolutionErrors2.dfy(415,21): Error: unresolved identifier: x +ResolutionErrors2.dfy(422,35): Error: Wrong number of type arguments (2 instead of 1) passed to abstract type: P +ResolutionErrors2.dfy(434,13): Error: Type or type parameter is not declared in this scope: BX (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +ResolutionErrors2.dfy(444,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require bool = int) +ResolutionErrors2.dfy(449,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require B = A) +ResolutionErrors2.dfy(454,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require int = A) +ResolutionErrors2.dfy(455,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require A = int) +ResolutionErrors2.dfy(460,13): Error: arguments must have comparable types (got P and P) +ResolutionErrors2.dfy(461,13): Error: arguments must have comparable types (got P and P) +ResolutionErrors2.dfy(462,13): Error: arguments must have comparable types (got P and P) +ResolutionErrors2.dfy(473,13): Error: new can be applied only to class types (got JJ) +ResolutionErrors2.dfy(481,37): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'o' (of type 'object') may contain references (see documentation for 'older' parameters) +ResolutionErrors2.dfy(482,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' (of type 'object') may contain references (see documentation for 'older' parameters) +ResolutionErrors2.dfy(489,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' +ResolutionErrors2.dfy(497,15): Error: arguments to / must be numeric or bitvector types (got set) +ResolutionErrors2.dfy(504,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 +ResolutionErrors2.dfy(519,16): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating 70 resolution/type errors detected in ResolutionErrors2.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors2.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors2.dfy.refresh.expect new file mode 100644 index 0000000000..a4397ec7c5 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors2.dfy.refresh.expect @@ -0,0 +1,81 @@ +ResolutionErrors2.dfy(24,22): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating +ResolutionErrors2.dfy(57,22): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating +ResolutionErrors2.dfy(90,17): Error: wrong number of method result arguments (got 0, expected 1) +ResolutionErrors2.dfy(111,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. +ResolutionErrors2.dfy(122,40): Error: ghost variables such as y are allowed only in specification contexts. y was inferred to be ghost based on its declaration or initialization. +ResolutionErrors2.dfy(144,6): Error: RHS (of type B) not assignable to LHS (of type object) +ResolutionErrors2.dfy(151,6): Error: RHS (of type G) not assignable to LHS (of type object) +ResolutionErrors2.dfy(152,6): Error: RHS (of type Dt) not assignable to LHS (of type object) +ResolutionErrors2.dfy(153,6): Error: RHS (of type CoDt) not assignable to LHS (of type object) +ResolutionErrors2.dfy(146,6): Error: RHS (of type B) not assignable to LHS (of type object) +ResolutionErrors2.dfy(145,9): Error: integer literal used as if it had type object? +ResolutionErrors2.dfy(164,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int) +ResolutionErrors2.dfy(175,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) +ResolutionErrors2.dfy(188,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) +ResolutionErrors2.dfy(197,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) +ResolutionErrors2.dfy(208,20): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) +ResolutionErrors2.dfy(220,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) +ResolutionErrors2.dfy(234,4): Error: LHS of array assignment must denote an array element (found seq) +ResolutionErrors2.dfy(238,4): Error: LHS of array assignment must denote an array element (found seq) +ResolutionErrors2.dfy(242,9): Error: cannot assign to a range of array elements (try the 'forall' statement) +ResolutionErrors2.dfy(242,4): Error: LHS of array assignment must denote an array element (found seq) +ResolutionErrors2.dfy(242,19): Error: integer literal used as if it had type seq +ResolutionErrors2.dfy(246,9): Error: cannot assign to a range of array elements (try the 'forall' statement) +ResolutionErrors2.dfy(246,4): Error: LHS of array assignment must denote an array element (found seq) +ResolutionErrors2.dfy(246,9): Error: index-range selection used as if it had type int +ResolutionErrors2.dfy(246,9): Error: resulting sequence (int) type does not agree with source sequence type (seq) +ResolutionErrors2.dfy(260,10): Error: LHS of assignment must denote a mutable field +ResolutionErrors2.dfy(261,10): Error: LHS of assignment must denote a mutable field +ResolutionErrors2.dfy(262,5): Error: cannot assign to a range of array elements (try the 'forall' statement) +ResolutionErrors2.dfy(263,5): Error: cannot assign to a range of array elements (try the 'forall' statement) +ResolutionErrors2.dfy(263,5): Error: index-range selection used as if it had type int +ResolutionErrors2.dfy(262,12): Error: RHS (of type int) not assignable to LHS (of type seq) +ResolutionErrors2.dfy(272,11): Error: unresolved identifier: s +ResolutionErrors2.dfy(284,39): Error: RHS (of type (?17, ?18, ?19)) not assignable to LHS (of type (int, real, int, real)) +ResolutionErrors2.dfy(283,34): Error: RHS (of type (int, int, real)) not assignable to LHS (of type (int, real, int)) (covariant type parameter 'T1' would require real :> int) +ResolutionErrors2.dfy(283,34): Error: RHS (of type (int, int, real)) not assignable to LHS (of type (int, real, int)) (covariant type parameter 'T2' would require int :> real) +ResolutionErrors2.dfy(291,18): Error: member '3' does not exist in datatype '_tuple#3' +ResolutionErrors2.dfy(291,28): Error: member 'x' does not exist in datatype '_tuple#2' +ResolutionErrors2.dfy(290,18): Error: condition is expected to be of type bool, but is int +ResolutionErrors2.dfy(291,20): Error: arguments must have comparable types (got ?23 and ?24) +ResolutionErrors2.dfy(314,21): Error: integer literal used as if it had type real +ResolutionErrors2.dfy(315,9): Error: integer literal used as if it had type real +ResolutionErrors2.dfy(315,12): Error: type of % must be integer-numeric or bitvector types (got real) +ResolutionErrors2.dfy(342,11): Error: Wrong number of type arguments (2 instead of 1) passed to non-null type: array3 +ResolutionErrors2.dfy(343,11): Error: Wrong number of type arguments (2 instead of 1) passed to non-null type: C +ResolutionErrors2.dfy(354,7): Error: duplicate name of top-level declaration: BadSyn2 +ResolutionErrors2.dfy(353,7): Related location +ResolutionErrors2.dfy(351,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List +ResolutionErrors2.dfy(352,17): Error: Type or type parameter is not declared in this scope: badName (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +ResolutionErrors2.dfy(353,22): Error: Type or type parameter is not declared in this scope: X (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +ResolutionErrors2.dfy(360,7): Error: type-synonym cycle: A -> A +ResolutionErrors2.dfy(364,7): Error: cycle among redirecting types (newtypes, subset types, type synonyms): A -> B -> A +ResolutionErrors2.dfy(369,7): Error: cycle among redirecting types (newtypes, subset types, type synonyms): A -> B -> A +ResolutionErrors2.dfy(379,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed +ResolutionErrors2.dfy(376,8): Error: class 'C' with fields without known initializers, like 'a' of type 'A', must declare a constructor +ResolutionErrors2.dfy(383,7): Error: cycle among redirecting types (newtypes, subset types, type synonyms): A -> B -> A +ResolutionErrors2.dfy(389,7): Error: cycle among redirecting types (newtypes, subset types, type synonyms): A -> B -> A +ResolutionErrors2.dfy(395,7): Error: type-synonym cycle: A -> A +ResolutionErrors2.dfy(402,25): Error: unresolved identifier: x +ResolutionErrors2.dfy(405,22): Error: unresolved identifier: x +ResolutionErrors2.dfy(408,25): Error: unresolved identifier: x +ResolutionErrors2.dfy(410,21): Error: unresolved identifier: x +ResolutionErrors2.dfy(412,21): Error: unresolved identifier: x +ResolutionErrors2.dfy(415,21): Error: unresolved identifier: x +ResolutionErrors2.dfy(422,35): Error: Wrong number of type arguments (2 instead of 1) passed to abstract type: P +ResolutionErrors2.dfy(434,13): Error: Type or type parameter is not declared in this scope: BX (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +ResolutionErrors2.dfy(444,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter 'A' would require bool = int) +ResolutionErrors2.dfy(449,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter 'A' would require B = A) +ResolutionErrors2.dfy(454,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter 'A' would require int = A) +ResolutionErrors2.dfy(455,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter 'A' would require A = int) +ResolutionErrors2.dfy(460,13): Error: arguments must have comparable types (got P and P) +ResolutionErrors2.dfy(461,13): Error: arguments must have comparable types (got P and P) +ResolutionErrors2.dfy(462,13): Error: arguments must have comparable types (got P and P) +ResolutionErrors2.dfy(473,13): Error: new can be applied only to class types (got JJ) +ResolutionErrors2.dfy(481,37): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references, but values of 'o' (of type 'object') may contain references (see documentation for 'older' parameters) +ResolutionErrors2.dfy(482,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' (of type 'object') may contain references (see documentation for 'older' parameters) +ResolutionErrors2.dfy(489,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' +ResolutionErrors2.dfy(497,15): Error: arguments to / must be numeric or bitvector types (got set) +ResolutionErrors2.dfy(504,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 +ResolutionErrors2.dfy(519,16): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating +78 resolution/type errors detected in ResolutionErrors2.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors3.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors3.dfy index 8ae780553d..beda4a9fcf 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors3.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors3.dfy @@ -1,5 +1,5 @@ -// RUN: %exits-with 2 %verify --allow-axioms "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --allow-axioms + // ------------ type variables whose values are not inferred ---------- @@ -63,9 +63,9 @@ module NonInferredTypeVariables { method MoreBadClient() { - var b0 := forall s :: s <= {} ==> s == {}; // error: type of s underspecified - var b1 := forall s: set :: s <= {} ==> s == {}; // error: type of s underspecified - var b2 := forall c: C? :: c in {null} ==> c == null; // error: type parameter of c underspecified + + + // In the following, the type of the bound variable is completely determined. var S: set>; @@ -544,3 +544,26 @@ module UnderspecifiedTypesInAttributes { } } } + +module NonInferredTypeVariables' { + class C { + var f: CT + } + + method MoreBadClient0() + { + var b0 := forall s :: s <= {} ==> s == {}; // error: type of s underspecified + var b1 := forall s: set :: s <= {} ==> s == {}; // error: type of s underspecified + } +} + +module NonInferredTypeVariables'' { + class C { + var f: CT + } + + method MoreBadClient1() + { + var b2 := forall c: C? :: c in {null} ==> c == null; // error: type parameter of c underspecified + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors3.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors3.dfy.expect index c7f3e547e1..a5c7a7d045 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors3.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors3.dfy.expect @@ -10,12 +10,6 @@ ResolutionErrors3.dfy(58,8): Error: the type of this variable is underspecified ResolutionErrors3.dfy(59,8): Error: the type of this local variable is underspecified ResolutionErrors3.dfy(60,8): Error: the type of this variable is underspecified ResolutionErrors3.dfy(61,8): Error: the type of this local variable is underspecified -ResolutionErrors3.dfy(66,26): Error: the type of this variable is underspecified -ResolutionErrors3.dfy(66,21): Error: type of bound variable 's' could not be determined; please specify the type explicitly -ResolutionErrors3.dfy(67,31): Error: the type of this variable is underspecified -ResolutionErrors3.dfy(67,21): Error: type of bound variable 's' could not be determined; please specify the type explicitly -ResolutionErrors3.dfy(68,30): Error: the type of this variable is underspecified -ResolutionErrors3.dfy(68,21): Error: type of bound variable 'c' could not be determined; please specify the type explicitly ResolutionErrors3.dfy(75,8): Error: the type of this local variable is underspecified ResolutionErrors3.dfy(78,29): Error: type of bound variable 'c' could not be determined; please specify the type explicitly ResolutionErrors3.dfy(89,21): Error: Type or type parameter is not declared in this scope: X (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) @@ -84,4 +78,10 @@ ResolutionErrors3.dfy(532,23): Error: the type of the bound variable 'u' could n ResolutionErrors3.dfy(535,27): Error: the type of the bound variable 'u' could not be determined ResolutionErrors3.dfy(539,40): Error: the type of the bound variable 'u' could not be determined ResolutionErrors3.dfy(541,38): Error: the type of the bound variable 'u' could not be determined +ResolutionErrors3.dfy(555,26): Error: the type of this variable is underspecified +ResolutionErrors3.dfy(555,21): Error: type of bound variable 's' could not be determined; please specify the type explicitly +ResolutionErrors3.dfy(556,31): Error: the type of this variable is underspecified +ResolutionErrors3.dfy(556,21): Error: type of bound variable 's' could not be determined; please specify the type explicitly +ResolutionErrors3.dfy(567,30): Error: the type of this variable is underspecified +ResolutionErrors3.dfy(567,21): Error: type of bound variable 'c' could not be determined; please specify the type explicitly 86 resolution/type errors detected in ResolutionErrors3.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors3.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors3.dfy.refresh.expect new file mode 100644 index 0000000000..6aff850b5d --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors3.dfy.refresh.expect @@ -0,0 +1,90 @@ +ResolutionErrors3.dfy(53,13): Error: type parameter 'PT' (inferred to be '?40') in the function call to 'P' could not be determined +ResolutionErrors3.dfy(54,14): Error: the type of this variable is underspecified +ResolutionErrors3.dfy(54,19): Error: type parameter 'QT' (inferred to be '?42') in the function call to 'Q' could not be determined +ResolutionErrors3.dfy(54,20): Error: the type of this expression is underspecified +ResolutionErrors3.dfy(55,4): Error: type parameter 'MT' (inferred to be '?44') to the method 'M' could not be determined +ResolutionErrors3.dfy(56,8): Error: the type of this variable is underspecified +ResolutionErrors3.dfy(56,13): Error: type parameter 'NT' (inferred to be '?45') to the method 'N' could not be determined +ResolutionErrors3.dfy(57,8): Error: the type ('array?') of this variable is underspecified +ResolutionErrors3.dfy(58,8): Error: the type ('C?') of this variable is underspecified +ResolutionErrors3.dfy(59,8): Error: the type ('set') of this local variable is underspecified +ResolutionErrors3.dfy(60,8): Error: the type ('array?>') of this variable is underspecified +ResolutionErrors3.dfy(61,8): Error: the type of this local variable is underspecified +ResolutionErrors3.dfy(75,8): Error: the type ('C') of this local variable is underspecified +ResolutionErrors3.dfy(78,29): Error: type of bound variable 'c' could not be determined ('C?'); please specify the type explicitly +ResolutionErrors3.dfy(89,21): Error: Type or type parameter is not declared in this scope: X (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +ResolutionErrors3.dfy(90,24): Error: Type or type parameter is not declared in this scope: X (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules) +ResolutionErrors3.dfy(127,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y) +ResolutionErrors3.dfy(144,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) +ResolutionErrors3.dfy(174,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name) +ResolutionErrors3.dfy(184,29): Error: ghost variables such as tmp are allowed only in specification contexts. tmp was inferred to be ghost based on its declaration or initialization. +ResolutionErrors3.dfy(186,49): Error: ghost variables such as a0 are allowed only in specification contexts. a0 was inferred to be ghost based on its declaration or initialization. +ResolutionErrors3.dfy(186,54): Error: ghost variables such as a1 are allowed only in specification contexts. a1 was inferred to be ghost based on its declaration or initialization. +ResolutionErrors3.dfy(195,33): Error: set argument type must support equality (got (int, int -> bool)) +ResolutionErrors3.dfy(207,11): Error: name of type (X) is used as a variable +ResolutionErrors3.dfy(207,16): Error: name of type (X) is used as a variable +ResolutionErrors3.dfy(208,11): Error: name of module (Y) is used as a variable +ResolutionErrors3.dfy(208,16): Error: name of module (Y) is used as a variable +ResolutionErrors3.dfy(209,11): Error: name of type (X) is used as a variable +ResolutionErrors3.dfy(210,11): Error: name of module (Y) is used as a variable +ResolutionErrors3.dfy(207,13): Error: arguments must have comparable types (got ?0 and ?1) +ResolutionErrors3.dfy(208,13): Error: arguments must have comparable types (got ?3 and ?4) +ResolutionErrors3.dfy(215,16): Error: name of type (X) is used as a variable +ResolutionErrors3.dfy(216,16): Error: name of module (Y) is used as a variable +ResolutionErrors3.dfy(217,4): Error: name of type (X) is used as a variable +ResolutionErrors3.dfy(218,4): Error: name of module (Y) is used as a variable +ResolutionErrors3.dfy(227,11): Error: type of left argument to + (int) must agree with the result type (bool) +ResolutionErrors3.dfy(227,11): Error: type of right argument to + (int) must agree with the result type (bool) +ResolutionErrors3.dfy(227,11): 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) +ResolutionErrors3.dfy(228,9): Error: type of RHS of assign-such-that statement must be boolean (got int) +ResolutionErrors3.dfy(229,13): Error: type of RHS of assign-such-that statement must be boolean (got int) +ResolutionErrors3.dfy(232,15): Error: type of left argument to + (int) must agree with the result type (bool) +ResolutionErrors3.dfy(232,15): Error: type of right argument to + (int) must agree with the result type (bool) +ResolutionErrors3.dfy(232,15): 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) +ResolutionErrors3.dfy(248,29): Error: in a hint, calls are allowed only to lemmas +ResolutionErrors3.dfy(250,17): Error: in a hint, calls are allowed only to lemmas +ResolutionErrors3.dfy(275,20): Error: in a hint, calls are allowed only to lemmas +ResolutionErrors3.dfy(285,24): Error: in a hint, calls are allowed only to lemmas +ResolutionErrors3.dfy(298,18): Error: assignment to non-ghost field is not allowed in this context, because this is a ghost function +ResolutionErrors3.dfy(299,10): Error: a hint is not allowed to make heap updates +ResolutionErrors3.dfy(300,20): Error: in a hint, calls are allowed only to lemmas +ResolutionErrors3.dfy(303,21): Error: a loop in a hint is not allowed to use 'modifies' clauses +ResolutionErrors3.dfy(322,24): Error: in a hint, calls are allowed only to lemmas +ResolutionErrors3.dfy(329,18): Error: assignment to non-ghost field is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +ResolutionErrors3.dfy(330,10): Error: a hint is not allowed to make heap updates +ResolutionErrors3.dfy(331,11): Error: in a hint, calls are allowed only to lemmas +ResolutionErrors3.dfy(334,21): Error: a loop in a hint is not allowed to use 'modifies' clauses +ResolutionErrors3.dfy(360,29): Error: in a statement expression, calls are allowed only to lemmas +ResolutionErrors3.dfy(372,16): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating +ResolutionErrors3.dfy(391,12): Error: a 'break break break' statement is allowed only in contexts with 3 enclosing loops, but the current context only has 2 +ResolutionErrors3.dfy(403,20): Error: a ghost field is allowed only in specification contexts +ResolutionErrors3.dfy(411,9): Error: ghost variables such as g are allowed only in specification contexts. g was inferred to be ghost based on its declaration or initialization. +ResolutionErrors3.dfy(417,4): Error: non-ghost variable cannot be assigned a value that depends on a ghost +ResolutionErrors3.dfy(434,8): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +ResolutionErrors3.dfy(443,29): Error: ghost variables such as z are allowed only in specification contexts. z was inferred to be ghost based on its declaration or initialization. +ResolutionErrors3.dfy(451,10): Error: type of bound variable 't' could not be determined; please specify the type explicitly +ResolutionErrors3.dfy(451,10): Error: type of bound variable 't' could not be determined; please specify the type explicitly +ResolutionErrors3.dfy(451,10): Error: type of bound variable 't' could not be determined; please specify the type explicitly +ResolutionErrors3.dfy(451,10): Error: type of bound variable 't' could not be determined; please specify the type explicitly +ResolutionErrors3.dfy(451,10): Error: type of bound variable 't' could not be determined; please specify the type explicitly +ResolutionErrors3.dfy(451,10): Error: type of bound variable 't' could not be determined; please specify the type explicitly +ResolutionErrors3.dfy(468,15): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) +ResolutionErrors3.dfy(470,10): Error: assignment to non-ghost field is not allowed in this context, because this is a ghost method +ResolutionErrors3.dfy(493,15): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) +ResolutionErrors3.dfy(495,25): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +ResolutionErrors3.dfy(496,35): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +ResolutionErrors3.dfy(505,4): Error: 'decreases *' is not allowed on ghost loops +ResolutionErrors3.dfy(509,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +ResolutionErrors3.dfy(518,4): Error: 'decreases *' is not allowed on ghost loops +ResolutionErrors3.dfy(522,29): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +ResolutionErrors3.dfy(531,21): Error: type of bound variable 'u' could not be determined; please specify the type explicitly +ResolutionErrors3.dfy(532,23): Error: type of bound variable 'u' could not be determined; please specify the type explicitly +ResolutionErrors3.dfy(535,27): Error: type of bound variable 'u' could not be determined; please specify the type explicitly +ResolutionErrors3.dfy(539,40): Error: type of bound variable 'u' could not be determined; please specify the type explicitly +ResolutionErrors3.dfy(541,38): Error: type of bound variable 'u' could not be determined; please specify the type explicitly +ResolutionErrors3.dfy(541,38): Error: type of bound variable 'u' could not be determined; please specify the type explicitly +ResolutionErrors3.dfy(555,40): Error: arguments must have comparable types (got set and set) +ResolutionErrors3.dfy(556,45): Error: arguments must have comparable types (got set and set) +ResolutionErrors3.dfy(567,30): Error: the type ('C?') of this variable is underspecified +ResolutionErrors3.dfy(567,21): Error: type of bound variable 'c' could not be determined ('C?'); please specify the type explicitly +89 resolution/type errors detected in ResolutionErrors3.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors8.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors8.dfy index 452110e9b2..b904094f3c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors8.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors8.dfy @@ -1,5 +1,5 @@ -// RUN: %exits-with 2 %verify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" + // --------------- let-such-that ghost regressions ------------------------------ diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors8.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors8.dfy.refresh.expect new file mode 100644 index 0000000000..8f3e096dc9 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors8.dfy.refresh.expect @@ -0,0 +1,77 @@ +ResolutionErrors8.dfy(47,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. +ResolutionErrors8.dfy(61,21): Error: a loop in a hint is not allowed to use 'modifies' clauses +ResolutionErrors8.dfy(68,21): Error: a loop in a hint is not allowed to use 'modifies' clauses +ResolutionErrors8.dfy(97,15): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got multiset) +ResolutionErrors8.dfy(98,15): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got map) +ResolutionErrors8.dfy(99,15): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got map) +ResolutionErrors8.dfy(100,15): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got imap) +ResolutionErrors8.dfy(105,15): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got int) +ResolutionErrors8.dfy(106,15): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got set) +ResolutionErrors8.dfy(107,15): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got iset) +ResolutionErrors8.dfy(108,15): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got seq) +ResolutionErrors8.dfy(113,15): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got int -> int) +ResolutionErrors8.dfy(114,15): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got int -> object) +ResolutionErrors8.dfy(115,15): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got int -> set) +ResolutionErrors8.dfy(116,15): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got int -> seq) +ResolutionErrors8.dfy(117,15): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got set -> int) +ResolutionErrors8.dfy(136,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got map) +ResolutionErrors8.dfy(137,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got map) +ResolutionErrors8.dfy(138,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got imap) +ResolutionErrors8.dfy(143,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int) +ResolutionErrors8.dfy(144,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got set) +ResolutionErrors8.dfy(145,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got iset) +ResolutionErrors8.dfy(146,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got seq) +ResolutionErrors8.dfy(155,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> int) +ResolutionErrors8.dfy(156,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> object) +ResolutionErrors8.dfy(157,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> set) +ResolutionErrors8.dfy(158,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> iset) +ResolutionErrors8.dfy(159,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> seq) +ResolutionErrors8.dfy(160,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got set -> int) +ResolutionErrors8.dfy(161,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got bool -> multiset) +ResolutionErrors8.dfy(162,19): Error: an unchanged expression must denote an object or a set/iset/multiset/seq of objects (instead got bool -> map) +ResolutionErrors8.dfy(177,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got map) +ResolutionErrors8.dfy(178,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got map) +ResolutionErrors8.dfy(179,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got imap) +ResolutionErrors8.dfy(184,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int) +ResolutionErrors8.dfy(185,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got set) +ResolutionErrors8.dfy(186,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got iset) +ResolutionErrors8.dfy(187,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got seq) +ResolutionErrors8.dfy(195,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> int) +ResolutionErrors8.dfy(196,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> object) +ResolutionErrors8.dfy(197,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> set) +ResolutionErrors8.dfy(198,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> iset) +ResolutionErrors8.dfy(199,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int -> seq) +ResolutionErrors8.dfy(200,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got set -> int) +ResolutionErrors8.dfy(201,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got bool -> multiset) +ResolutionErrors8.dfy(202,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got bool -> map) +ResolutionErrors8.dfy(218,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) +ResolutionErrors8.dfy(219,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) +ResolutionErrors8.dfy(220,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) +ResolutionErrors8.dfy(226,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) +ResolutionErrors8.dfy(227,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) +ResolutionErrors8.dfy(228,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) +ResolutionErrors8.dfy(229,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) +ResolutionErrors8.dfy(238,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) +ResolutionErrors8.dfy(239,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) +ResolutionErrors8.dfy(243,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) +ResolutionErrors8.dfy(245,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) +ResolutionErrors8.dfy(264,12): Error: a 'break break break continue' statement is allowed only in contexts with 4 enclosing loops, but the current context only has 3 +ResolutionErrors8.dfy(301,27): Error: continue label must designate a loop: X +ResolutionErrors8.dfy(303,27): Error: continue label must designate a loop: Y0 +ResolutionErrors8.dfy(305,27): Error: continue label must designate a loop: Y1 +ResolutionErrors8.dfy(307,27): Error: continue label must designate a loop: Z +ResolutionErrors8.dfy(317,4): Error: a non-labeled 'break' statement is allowed only in loops +ResolutionErrors8.dfy(321,4): Error: a non-labeled 'continue' statement is allowed only in loops +ResolutionErrors8.dfy(327,19): Error: a non-labeled 'break' statement is allowed only in loops +ResolutionErrors8.dfy(328,19): Error: a non-labeled 'continue' statement is allowed only in loops +ResolutionErrors8.dfy(330,28): Error: continue label must designate a loop: X +ResolutionErrors8.dfy(347,21): Error: a non-labeled 'break' statement is allowed only in loops +ResolutionErrors8.dfy(348,21): Error: a non-labeled 'continue' statement is allowed only in loops +ResolutionErrors8.dfy(349,27): Error: break label is undefined or not in scope: L +ResolutionErrors8.dfy(350,30): Error: continue label is undefined or not in scope: L +ResolutionErrors8.dfy(363,8): Error: ghost-context continue statement is not allowed to continue out of non-ghost loop +ResolutionErrors8.dfy(372,8): Error: ghost-context break statement is not allowed to break out of non-ghost loop +ResolutionErrors8.dfy(380,8): Error: ghost-context continue statement is not allowed to continue out of non-ghost loop +ResolutionErrors8.dfy(395,10): Error: ghost-context continue statement is not allowed to continue out of non-ghost loop +ResolutionErrors8.dfy(418,10): Error: ghost-context continue statement is not allowed to continue out of non-ghost loop +76 resolution/type errors detected in ResolutionErrors8.dfy