diff --git a/Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs b/Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs index f78a07109b..63e5eb3937 100644 --- a/Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs @@ -5,7 +5,7 @@ namespace Microsoft.Dafny; -public class HideRevealStmt : Statement, ICloneable, ICanFormat { +public class HideRevealStmt : Statement, ICloneable, ICanFormat, ICanResolveNewAndOld { public const string RevealLemmaPrefix = "reveal_"; public string Kind => Mode == HideRevealCmd.Modes.Hide ? "hide" : "reveal"; @@ -72,7 +72,7 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { return formatter.SetIndentPrintRevealStmt(indentBefore, OwnedTokens); } - public void Resolve(PreTypeResolver resolver, ResolutionContext resolutionContext) { + public override void GenResolve(INewOrOldResolver resolver, ResolutionContext resolutionContext) { ((ICodeContainer)resolutionContext.CodeContext).ContainsHide |= Mode == HideRevealCmd.Modes.Hide; if (Wildcard) { @@ -93,33 +93,38 @@ public void Resolve(PreTypeResolver resolver, ResolutionContext resolutionContex effectiveExpr = applySuffix.Lhs; } if (effectiveExpr is NameSegment or ExprDotName) { - if (effectiveExpr is NameSegment) { - resolver.ResolveNameSegment((NameSegment)effectiveExpr, true, null, resolutionContext, true); + if (effectiveExpr is NameSegment segment) { + resolver.ResolveNameSegment(segment, true, null, resolutionContext, true); } else { resolver.ResolveDotSuffix((ExprDotName)effectiveExpr, true, true, null, resolutionContext, true); } - var callee = (MemberSelectExpr)((ConcreteSyntaxExpression)effectiveExpr).ResolvedExpression; - if (callee == null) { + + if (effectiveExpr.Resolved == null) { // error from resolving child + } else if (effectiveExpr.Resolved is not MemberSelectExpr callee) { + resolver.Reporter.Error(MessageSource.Resolver, effectiveExpr.Tok, + $"cannot reveal '{name}' because no revealable constant, function, assert label, or requires label in the current scope is named '{name}'"); } else { if (callee.Member is Function or ConstantField) { OffsetMembers.Add(callee.Member); - if (callee.Member.IsOpaque && Mode == HideRevealCmd.Modes.Reveal) { - var revealResolutionContext = resolutionContext with { InReveal = true }; - var exprClone = new Cloner().CloneExpr(effectiveExpr); - if (exprClone is NameSegment) { - resolver.ResolveNameSegment((NameSegment)exprClone, true, null, revealResolutionContext, true); - } else { - resolver.ResolveDotSuffix((ExprDotName)exprClone, true, true, null, revealResolutionContext, true); - } - - var revealCallee = ((MemberSelectExpr)((ConcreteSyntaxExpression)exprClone).ResolvedExpression); - if (revealCallee != null) { - var call = new CallStmt(RangeToken, new List(), - revealCallee, - new List(), effectiveExpr.tok); - ResolvedStatements.Add(call); - } + if (!BoogieGenerator.IsOpaque(callee.Member, resolver.Options) || Mode != HideRevealCmd.Modes.Reveal) { + continue; + } + + var revealResolutionContext = resolutionContext with { InReveal = true }; + var exprClone = new Cloner().CloneExpr(effectiveExpr); + if (exprClone is NameSegment nameSegment) { + resolver.ResolveNameSegment(nameSegment, true, null, revealResolutionContext, true); + } else { + resolver.ResolveDotSuffix((ExprDotName)exprClone, true, true, null, revealResolutionContext, true); + } + + var revealCallee = ((MemberSelectExpr)((ConcreteSyntaxExpression)exprClone).ResolvedExpression); + if (revealCallee != null) { + var call = new CallStmt(RangeToken, new List(), + revealCallee, + new List(), effectiveExpr.tok); + ResolvedStatements.Add(call); } } else { resolver.Reporter.Error(MessageSource.Resolver, effectiveExpr.Tok, diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index d5f65401db..e505db5121 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -544,7 +544,7 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont } else if (expr is ExprDotName) { var e = (ExprDotName)expr; - ResolveDotSuffix(e, true, null, resolutionContext, false); + ResolveDotSuffix(e, false, true, null, resolutionContext, false); if (e.Type is Resolver_IdentifierExpr.ResolverType_Module) { reporter.Error(MessageSource.Resolver, e.tok, "name of module ({0}) is used as a variable", e.SuffixName); e.ResetTypeAssignment(); // the rest of type checking assumes actual types @@ -3500,50 +3500,7 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext s.Args.ForEach(e => ResolveExpression(e, resolutionContext)); } else if (stmt is HideRevealStmt hideRevealStmt) { - foreach (var expr in hideRevealStmt.Exprs) { - var name = HideRevealStmt.SingleName(expr); - var labeledAssert = name == null ? null : DominatingStatementLabels.Find(name) as AssertLabel; - if (labeledAssert != null) { - hideRevealStmt.LabeledAsserts.Add(labeledAssert); - } else { - var revealResolutionContext = resolutionContext with { InReveal = true }; - if (expr is ApplySuffix) { - var e = (ApplySuffix)expr; - var methodCallInfo = ResolveApplySuffix(e, revealResolutionContext, true); - if (methodCallInfo == null) { - // error has already been reported - } else if (methodCallInfo.Callee.Member is TwoStateLemma && !revealResolutionContext.IsTwoState) { - reporter.Error(MessageSource.Resolver, methodCallInfo.Tok, "a two-state function can only be revealed in a two-state context"); - } else if (methodCallInfo.Callee.AtLabel != null) { - Contract.Assert(methodCallInfo.Callee.Member is TwoStateLemma); - reporter.Error(MessageSource.Resolver, methodCallInfo.Tok, "to reveal a two-state function, do not list any parameters or @-labels"); - } else { - var call = new CallStmt(hideRevealStmt.RangeToken, new List(), methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok); - hideRevealStmt.ResolvedStatements.Add(call); - } - } else if (expr is NameSegment or ExprDotName) { - if (expr is NameSegment) { - ResolveNameSegment((NameSegment)expr, true, null, revealResolutionContext, true); - } else { - ResolveDotSuffix((ExprDotName)expr, true, null, revealResolutionContext, true); - } - MemberSelectExpr callee = (MemberSelectExpr)((ConcreteSyntaxExpression)expr).ResolvedExpression; - if (callee == null) { - } else if (callee.Member is Lemma or TwoStateLemma && Attributes.Contains(callee.Member.Attributes, "axiom")) { - //The revealed member is a function - reporter.Error(MessageSource.Resolver, callee.tok, "to reveal a function ({0}), append parentheses", callee.Member.ToString().Substring(7)); - } else { - var call = new CallStmt(hideRevealStmt.RangeToken, new List(), callee, new List(), expr.tok); - hideRevealStmt.ResolvedStatements.Add(call); - } - } else { - ResolveExpression(expr, revealResolutionContext); - } - } - } - foreach (var a in hideRevealStmt.ResolvedStatements) { - ResolveStatement(a, resolutionContext); - } + stmt.GenResolve(this, resolutionContext); } else if (stmt is BreakStmt) { var s = (BreakStmt)stmt; if (s.TargetLabel != null) { @@ -4448,7 +4405,7 @@ public void ResolveTypeRhs(TypeRhs rr, Statement stmt, ResolutionContext resolut // type, create a dot-suffix expression around this receiver, and then resolve it in the usual way for dot-suffix expressions. var lhs = new ImplicitThisExpr_ConstructorCall(initCallTok) { Type = rr.EType }; var callLhs = new ExprDotName(((UserDefinedType)rr.EType).tok, lhs, initCallName, ret == null ? null : ret.LastComponent.OptTypeArguments); - ResolveDotSuffix(callLhs, true, rr.Bindings.ArgumentBindings, resolutionContext, true); + ResolveDotSuffix(callLhs, false, true, rr.Bindings.ArgumentBindings, resolutionContext, true); if (prevErrorCount == reporter.Count(ErrorLevel.Error)) { Contract.Assert(callLhs.ResolvedExpression is MemberSelectExpr); // since ResolveApplySuffix succeeded and call.Lhs denotes an expression (not a module or a type) var methodSel = (MemberSelectExpr)callLhs.ResolvedExpression; @@ -5604,7 +5561,7 @@ void ResolveNameSegment_Type(NameSegment expr, ResolutionContext resolutionConte /// /// If false, generates an error if the name denotes a method. If true and the name denotes a method, returns /// a Resolver_MethodCall. - Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List args, ResolutionContext resolutionContext, bool allowMethodCall) { + public Expression ResolveDotSuffix(ExprDotName expr, bool allowStaticReferenceToInstance, bool isLastNameSegment, List args, ResolutionContext resolutionContext, bool allowMethodCall) { Contract.Requires(expr != null); Contract.Requires(!expr.WasResolved()); Contract.Requires(resolutionContext != null); @@ -5617,7 +5574,7 @@ Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List args, + ResolutionContext resolutionContext, bool allowMethodCall, bool complain = true); + + public Expression ResolveDotSuffix(ExprDotName expr, bool allowStaticReferenceToInstance, bool isLastNameSegment, List args, + ResolutionContext resolutionContext, bool allowMethodCall); } \ No newline at end of file diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index 0c452ce41d..8603af3763 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -1164,6 +1164,11 @@ private void ReportMemberNotFoundError(IToken tok, string memberName, [CanBeNull } } + public Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List args, + ResolutionContext resolutionContext, bool allowMethodCall, bool complain = true) { + return ResolveNameSegment(expr, isLastNameSegment, args, resolutionContext, allowMethodCall, complain, false); + } + /// /// Look up expr.Name in the following order: /// 0. Local variable, parameter, or bound variable. @@ -1192,7 +1197,7 @@ private void ReportMemberNotFoundError(IToken tok, string memberName, [CanBeNull /// there is no "this" in scope. This seems like a terrible hack, because it breaks scope invariants about the AST. But, for now, it's here /// to mimic what the legacy resolver does. public Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List args, - ResolutionContext resolutionContext, bool allowMethodCall, bool complain = true, bool specialOpaqueHackAllowance = false) { + ResolutionContext resolutionContext, bool allowMethodCall, bool complain, bool specialOpaqueHackAllowance) { Contract.Requires(expr != null); Contract.Requires(!expr.WasResolved()); Contract.Requires(resolutionContext != null); diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs index 8992a33b3d..21a5938ab9 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs @@ -112,8 +112,6 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext ResolveExpression(e, resolutionContext); } - } else if (stmt is HideRevealStmt hideRevealStmt) { - hideRevealStmt.Resolve(this, resolutionContext); } else if (stmt is BreakStmt) { var s = (BreakStmt)stmt; if (s.TargetLabel != null) { diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs index 8f064443a2..0260f67214 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs @@ -1023,7 +1023,7 @@ public void ResolveAttributes(IAttributeBearingDeclaration attributeHost, Resolu if (attr.Args != null) { foreach (var arg in attr.Args) { if (Attributes.Contains(attributeHost.Attributes, "opaque_reveal") && attr.Name is "revealedFunction" && arg is NameSegment nameSegment) { - ResolveNameSegment(nameSegment, true, null, opts, false, specialOpaqueHackAllowance: true); + ResolveNameSegment(nameSegment, true, null, opts, false, complain: true, specialOpaqueHackAllowance: true); } else { ResolveExpression(arg, opts); } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs index 85eaa55d10..f6fe288ec9 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs @@ -118,7 +118,7 @@ Bpl.Function GetReadonlyField(Field f) { var cf = (ConstantField)f; if (cf.Rhs != null && RevealedInScope(cf)) { var etran = new ExpressionTranslator(this, predef, NewOneHeapExpr(f.tok), null); - if (!IsOpaque(cf)) { + if (!IsOpaque(cf, options)) { var definitionAxiom = ff.CreateDefinitionAxiom(etran.TrExpr(cf.Rhs)); definitionAxiom.CanHide = true; sink.AddTopLevelDeclaration(definitionAxiom); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index 0652b8baeb..33e24efc17 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -1378,9 +1378,9 @@ public Bpl.Expr GetArrayIndexFieldName(IToken tok, List indices) { bool FunctionBodyIsAvailable(Function f, ModuleDefinition context, VisibilityScope scope, bool revealProtectedBody) { Contract.Requires(f != null); Contract.Requires(context != null); - return f.Body != null && !IsOpaque(f) && f.IsRevealedInScope(scope); + return f.Body != null && !IsOpaque(f, options) && f.IsRevealedInScope(scope); } - bool IsOpaque(MemberDecl f) { + public static bool IsOpaque(MemberDecl f, DafnyOptions options) { Contract.Requires(f != null); if (f is Function f1) { return Attributes.Contains(f.Attributes, "opaque") || f.IsOpaque || f1.IsMadeImplicitlyOpaque(options); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAssertsResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAssertsResolution.dfy.expect index 83f1d8d241..0c054459d6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAssertsResolution.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAssertsResolution.dfy.expect @@ -7,7 +7,7 @@ LabeledAssertsResolution.dfy(34,24): Error: assert label shadows a dominating la LabeledAssertsResolution.dfy(73,12): Error: break label is undefined or not in scope: ABC LabeledAssertsResolution.dfy(81,17): Error: cannot reveal 'C' because no revealable constant, function, assert label, or requires label in the current scope is named 'C' LabeledAssertsResolution.dfy(94,17): Error: no label 'XYZ' in scope at this time -LabeledAssertsResolution.dfy(115,14): Error: cannot reveal 'X' because no revealable constant, function, assert label, or requires label in the current scope is named 'X' +LabeledAssertsResolution.dfy(115,14): Error: unresolved identifier: X LabeledAssertsResolution.dfy(52,11): Error: assert label shadows a dominating label LabeledAssertsResolution.dfy(54,11): Error: assert label shadows a dominating label LabeledAssertsResolution.dfy(125,6): Error: an assert-by body is not allowed to update a variable it doesn't declare diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/OpaqueConstants.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/OpaqueConstants.dfy index bd287c7ae5..005addb482 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/OpaqueConstants.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/OpaqueConstants.dfy @@ -12,7 +12,7 @@ module Module { } else { reveal M.Five; assert M.Five == 5; - } + } } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Resolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Resolution.dfy index 15ee7dbf73..f710c4e20c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Resolution.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Resolution.dfy @@ -478,13 +478,13 @@ module TwoStateAt { method UseOrdinaryOpaque() { label L: reveal OrdinaryOpaque(); - reveal OrdinaryOpaque; // error: missing parentheses + reveal OrdinaryOpaque; reveal OrdinaryOpaque@K(); // error: label K not in scope reveal OrdinaryOpaque@L(); // error: @ can only be applied to something two-state (error message can be improved) } ghost function FuncUseOrdinaryOpaque(): int { reveal OrdinaryOpaque(); - reveal OrdinaryOpaque; // error: missing parentheses + reveal OrdinaryOpaque; reveal OrdinaryOpaque@K(); // error: label K not in scope 10 } @@ -492,7 +492,7 @@ module TwoStateAt { method UseOpaque() { label L: reveal Opaque(); - reveal Opaque; // error: missing parentheses + reveal Opaque; reveal Opaque@K(); // error: label K not in scope reveal Opaque@L(); // error: all parameters in a reveal must be implicit, including labels } @@ -504,7 +504,7 @@ module TwoStateAt { } twostate function TwoFuncUseOpaque(): int { reveal Opaque(); - reveal Opaque; // error: missing parentheses + reveal Opaque; reveal Opaque@K(); // error: label K not in scope 10 } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Resolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Resolution.dfy.expect index 78d376ea73..2de5f62f28 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Resolution.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Resolution.dfy.expect @@ -743,20 +743,16 @@ Twostate-Resolution.dfy(445,20): Error: no label 'After' in scope at this time Twostate-Resolution.dfy(452,17): Error: an @-label can only be applied to a two-state function Twostate-Resolution.dfy(453,14): Error: an @-label can only be applied to a two-state lemma Twostate-Resolution.dfy(459,19): Error: an @-label can only be applied to a two-state function -Twostate-Resolution.dfy(481,11): Error: to reveal a function (OrdinaryOpaque), append parentheses -Twostate-Resolution.dfy(482,26): Error: no label 'K' in scope at this time -Twostate-Resolution.dfy(483,26): Error: an @-label can only be applied to a two-state lemma -Twostate-Resolution.dfy(487,11): Error: to reveal a function (OrdinaryOpaque), append parentheses -Twostate-Resolution.dfy(488,26): Error: no label 'K' in scope at this time -Twostate-Resolution.dfy(495,11): Error: to reveal a function (Opaque), append parentheses -Twostate-Resolution.dfy(496,18): Error: no label 'K' in scope at this time -Twostate-Resolution.dfy(497,19): Error: to reveal a two-state function, do not list any parameters or @-labels -Twostate-Resolution.dfy(500,17): Error: a two-state function can only be revealed in a two-state context -Twostate-Resolution.dfy(501,11): Error: to reveal a function (Opaque), append parentheses -Twostate-Resolution.dfy(502,18): Error: no label 'K' in scope at this time -Twostate-Resolution.dfy(502,19): Error: a two-state function can only be revealed in a two-state context -Twostate-Resolution.dfy(507,11): Error: to reveal a function (Opaque), append parentheses -Twostate-Resolution.dfy(508,18): Error: no label 'K' in scope at this time +Twostate-Resolution.dfy(482,27): Error: an @-label can not be used in a hide or reveal statement +Twostate-Resolution.dfy(483,27): Error: an @-label can not be used in a hide or reveal statement +Twostate-Resolution.dfy(488,27): Error: an @-label can not be used in a hide or reveal statement +Twostate-Resolution.dfy(496,19): Error: an @-label can not be used in a hide or reveal statement +Twostate-Resolution.dfy(497,19): Error: an @-label can not be used in a hide or reveal statement +Twostate-Resolution.dfy(500,11): Error: two-state function ('Opaque') can only be called in a two-state context +Twostate-Resolution.dfy(501,11): Error: two-state function ('Opaque') can only be called in a two-state context +Twostate-Resolution.dfy(502,19): Error: an @-label can not be used in a hide or reveal statement +Twostate-Resolution.dfy(502,11): Error: two-state function ('Opaque') can only be called in a two-state context +Twostate-Resolution.dfy(508,19): Error: an @-label can not be used in a hide or reveal statement Twostate-Resolution.dfy(515,11): Error: two-state lemmas can only be used in two-state contexts Twostate-Resolution.dfy(535,28): Error: parameter 'a' of function P cannot be changed, compared to in the overridden function, from non-older to older Twostate-Resolution.dfy(536,22): Error: parameter 'a' of function Q cannot be changed, compared to in the overridden function, from older to non-older @@ -766,4 +762,4 @@ Twostate-Resolution.dfy(558,26): Error: parameter 'a' of function P cannot be ch Twostate-Resolution.dfy(559,20): Error: parameter 'a' of function Q cannot be changed, compared to the corresponding function in the module it refines, from older to non-older Twostate-Resolution.dfy(560,27): Error: parameter 'a' of function X cannot be changed, compared to the corresponding function in the module it refines, from non-new to new Twostate-Resolution.dfy(561,23): Error: parameter 'a' of function Y cannot be changed, compared to the corresponding function in the module it refines, from new to non-new -73 resolution/type errors detected in Twostate-Resolution.dfy +69 resolution/type errors detected in Twostate-Resolution.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1618.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1618.dfy index ab80357224..308a964257 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1618.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1618.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %resolve "%s" > "%t" +// RUN: %resolve "%s" > "%t" // RUN: %diff "%s.expect" "%t" function {:opaque} mul(a: int, b: int): int diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1618.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1618.dfy.expect index 731250eaf6..f829807e3d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1618.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1618.dfy.expect @@ -1,2 +1,2 @@ -git-issue-1618.dfy(11,9): Error: to reveal a function (mul), append parentheses -1 resolution/type errors detected in git-issue-1618.dfy + +Dafny program verifier did not attempt verification diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804d.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804d.dfy.expect index 9396a9549b..b6ef85407e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804d.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804d.dfy.expect @@ -1,5 +1,5 @@ -git-issue-3804d.dfy(12,37): Error: cannot reveal 'q' because no revealable constant, function, assert label, or requires label in the current scope is named 'q' -git-issue-3804d.dfy(16,34): Error: cannot reveal 'p' because no revealable constant, function, assert label, or requires label in the current scope is named 'p' -git-issue-3804d.dfy(18,9): Error: cannot reveal 'q' because no revealable constant, function, assert label, or requires label in the current scope is named 'q' -git-issue-3804d.dfy(18,12): Error: cannot reveal 'p' because no revealable constant, function, assert label, or requires label in the current scope is named 'p' +git-issue-3804d.dfy(12,37): Error: unresolved identifier: q +git-issue-3804d.dfy(16,34): Error: unresolved identifier: p +git-issue-3804d.dfy(18,9): Error: unresolved identifier: q +git-issue-3804d.dfy(18,12): Error: unresolved identifier: p 4 resolution/type errors detected in git-issue-3804d.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.expect index b0a74d69a3..0e903fbdd6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.expect @@ -9,18 +9,14 @@ git-issue-5017b.dfy(94,13): Error: predicate 'Valid' cannot be revealed, because git-issue-5017b.dfy(132,11): Error: unresolved identifier: x git-issue-5017b.dfy(133,13): Error: member 'UnknownFunction' does not exist in trait 'A' git-issue-5017b.dfy(134,13): Error: member 'UnknownFunction' does not exist in trait 'A' -git-issue-5017b.dfy(135,13): Error: a method ('Method') cannot be revealed; only opaque constants and functions can be revealed -git-issue-5017b.dfy(136,13): Error: a method ('Method') cannot be revealed; only opaque constants and functions can be revealed -git-issue-5017b.dfy(137,13): Error: const field 'm' cannot be revealed, because it is not opaque +git-issue-5017b.dfy(135,13): Error: only functions and constants can be revealed +git-issue-5017b.dfy(136,13): Error: only functions and constants can be revealed git-issue-5017b.dfy(140,13): Error: predicate 'Valid' cannot be revealed, because it has no body in trait 'A' git-issue-5017b.dfy(141,13): Error: predicate 'Valid' cannot be revealed, because it has no body in trait 'A' -git-issue-5017b.dfy(143,13): Error: to reveal a function (WithBody), append parentheses -git-issue-5017b.dfy(117,13): Error: cannot reveal 'UnknownFunction' because no revealable constant, function, assert label, or requires label in the current scope is named 'UnknownFunction' -git-issue-5017b.dfy(118,13): Error: cannot reveal 'UnknownFunction' because no revealable constant, function, assert label, or requires label in the current scope is named 'UnknownFunction' -git-issue-5017b.dfy(119,13): Error: cannot reveal 'Method' because no revealable constant, function, assert label, or requires label in the current scope is named 'Method' -git-issue-5017b.dfy(120,13): Error: cannot reveal 'Method' because no revealable constant, function, assert label, or requires label in the current scope is named 'Method' -git-issue-5017b.dfy(121,13): Error: cannot reveal 'm' because no revealable constant, function, assert label, or requires label in the current scope is named 'm' +git-issue-5017b.dfy(117,13): Error: unresolved identifier: UnknownFunction +git-issue-5017b.dfy(118,13): Error: unresolved identifier: UnknownFunction +git-issue-5017b.dfy(119,13): Error: only functions and constants can be revealed +git-issue-5017b.dfy(120,13): Error: only functions and constants can be revealed git-issue-5017b.dfy(124,13): Error: cannot reveal 'Valid' because no revealable constant, function, assert label, or requires label in the current scope is named 'Valid' git-issue-5017b.dfy(125,13): Error: cannot reveal 'Valid' because no revealable constant, function, assert label, or requires label in the current scope is named 'Valid' -git-issue-5017b.dfy(127,13): Error: to reveal a function (WithBody), append parentheses -25 resolution/type errors detected in git-issue-5017b.dfy +21 resolution/type errors detected in git-issue-5017b.dfy