diff --git a/Source/DafnyCore/Resolver/PreType/PreType.cs b/Source/DafnyCore/Resolver/PreType/PreType.cs index c66619e94f3..ac762d91197 100644 --- a/Source/DafnyCore/Resolver/PreType/PreType.cs +++ b/Source/DafnyCore/Resolver/PreType/PreType.cs @@ -455,10 +455,13 @@ public class PreTypePlaceholderModule : PreTypePlaceholder { public class PreTypePlaceholderType : PreTypePlaceholder { } - public class UnusedPreType : PreTypePlaceholder { + /// Used for assigning a pre-type to MemberSelect expressions, such as "obj.method", + /// which is not considered an expression. This indicates that resolution has occurred, + /// even though the pre-type itself is not useful. + public class MethodPreType : PreTypePlaceholder { public readonly string Why; - public UnusedPreType(string why) { + public MethodPreType(string why) { Why = why; } diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index 6731dd391ec..fc798f3490e 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -1591,6 +1591,7 @@ Expression ResolveExprDotCall(IToken tok, Expression receiver, DPreType receiver if (!allowMethodCall) { // it's a method and method calls are not allowed in the given resolutionContext ReportError(tok, "expression is not allowed to invoke a {0} ({1})", member.WhatKind, member.Name); + return null; } int suppliedTypeArguments = optTypeArguments == null ? 0 : optTypeArguments.Count; if (optTypeArguments != null) { @@ -1608,7 +1609,7 @@ Expression ResolveExprDotCall(IToken tok, Expression receiver, DPreType receiver rr.PreTypeApplication_JustMember.Add(ta); subst.Add(method.TypeArgs[i], ta); } - rr.PreType = new UnusedPreType($"call to {method.WhatKind} {method.Name}"); // fill in this field, in order to make "rr" resolved + rr.PreType = new MethodPreType($"call to {method.WhatKind} {method.Name}"); // fill in this field, in order to make "rr" resolved } return rr; } diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs index 0067c8cdde3..41b041930fa 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs @@ -1590,7 +1590,7 @@ protected override void VisitOneExpr(Expression expr) { preTypeResolver.ReportError(expr.tok, $"SANITY CHECK FAILED: .PreType is '{expr.PreType}' but .Type is null"); } else if (PreType.Same(expr.PreType, preTypeResolver.Type2PreType(expr.Type))) { // all is cool - } else if (expr.PreType is UnusedPreType && expr.Type is TypeProxy) { + } else if (expr.PreType is MethodPreType && expr.Type is TypeProxy) { // this is expected } else { preTypeResolver.ReportError(expr.tok, $"SANITY CHECK FAILED: pre-type '{expr.PreType}' does not correspond to type '{expr.Type}'"); diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeToType.cs b/Source/DafnyCore/Resolver/PreType/PreTypeToType.cs index 21ddcdb908b..7f73b3737b0 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeToType.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeToType.cs @@ -140,7 +140,7 @@ protected override void PostVisitOneExpression(Expression expr, IASTVisitorConte return; } - if (expr.PreType is UnusedPreType) { + if (expr.PreType is MethodPreType) { expr.Type = new InferredTypeProxy(); return; } diff --git a/Source/DafnyCore/Resolver/ResolutionContext.cs b/Source/DafnyCore/Resolver/ResolutionContext.cs index 9a55e99999e..9cddc1297cc 100644 --- a/Source/DafnyCore/Resolver/ResolutionContext.cs +++ b/Source/DafnyCore/Resolver/ResolutionContext.cs @@ -36,6 +36,6 @@ public ResolutionContext WithGhost(bool isGhost) { if (CodeContext.IsGhost == isGhost) { return this; } - return new ResolutionContext(new CodeContextWrapper(CodeContext, isGhost), IsTwoState, InOld, InReveal, InFunctionPostcondition, InFirstPhaseConstructor); + return this with { CodeContext = new CodeContextWrapper(CodeContext, isGhost) }; } } \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5369.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5369.dfy new file mode 100644 index 00000000000..f21887b8a19 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5369.dfy @@ -0,0 +1,43 @@ +// RUN: %exits-with 2 %baredafny verify %args --type-system-refresh "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +ghost function f2(items: set): (r:nat) + requires |items| > 0 { + var item :| item in items; + item +} + +function f(items: set) : (r:nat) +requires |items| > 0 { + //assume exists item :: item in items && forall other <- items :: item == other || item < other; + //assert exists item Smallest() + var item :| IsSmallest(items, item); + item +} + +predicate IsSmallest(s: set, item: nat) + requires item in s { + m in s && forall y: nat :: y in s ==> m <= y +} + +lemma Smallest(s: set) returns (m: nat) + requires s != {} + ensures m in s && IsSmallest(s, m) + decreases s +{ + m :| m in s; + if y: nat :| y in s && y < m { + ghost var s' := s - {m}; + assert y in s'; + m := ThereIsASmallest(s'); + } +} + +function smallest(items: set): (r: nat) + requires |items| > 0 + +method m(items: set) returns (r:nat) +requires |items| > 0 { + var item :| item in items; + return item; +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5369.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5369.dfy.expect new file mode 100644 index 00000000000..c4144a73574 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5369.dfy.expect @@ -0,0 +1,4 @@ +git-issue-5369.dfy(20,2): Error: expression is not allowed to invoke a method (m) +git-issue-5369.dfy(20,40): Error: expression is not allowed to invoke a method (m) +git-issue-5369.dfy(32,9): Error: unresolved identifier: ThereIsASmallest +3 resolution/type errors detected in git-issue-5369.dfy diff --git a/docs/dev/news/5369.fix b/docs/dev/news/5369.fix new file mode 100644 index 00000000000..0f120ee253c --- /dev/null +++ b/docs/dev/news/5369.fix @@ -0,0 +1 @@ +Optional pre-type won't cause a crash anymore \ No newline at end of file