From 73c87c4a02c018533f0db8b9e6854f44c3562b48 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 1 Nov 2023 13:30:13 -0700 Subject: [PATCH 1/7] fix: Resolve the desugared :- expression --- .../PreType/PreTypeResolve.Expressions.cs | 1 + .../LitTest/git-issues/git-issue-4731.dfy | 29 +++++++++++++++++++ .../git-issues/git-issue-4731.dfy.expect | 2 ++ 3 files changed, 32 insertions(+) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4731.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4731.dfy.expect diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index e7207241f5e..67d2c575b30 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -611,6 +611,7 @@ resolutionContext.CodeContext is ConstantField || } else if (expr is LetOrFailExpr) { var e = (LetOrFailExpr)expr; e.ResolvedExpression = DesugarElephantExpr(e, resolutionContext); + ResolveExpression(e.ResolvedExpression, resolutionContext); e.PreType = e.ResolvedExpression.PreType; Constraints.AddGuardedConstraint(() => { if (e.Rhs.PreType.NormalizeWrtScope() is DPreType receiverPreType) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4731.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4731.dfy new file mode 100644 index 00000000000..b3dde284c23 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4731.dfy @@ -0,0 +1,29 @@ +// RUN: %testDafnyForEachResolver "%s" + +datatype Option = Some(val: T) | None { + predicate IsFailure() { + None? + } + + function PropagateFailure(): Option + requires None? + { + None + } + + function Extract(): T + requires Some? + { + val + } +} + +function Foo0(): Option { + var x: Option :- None; + None +} + +function Foo1(): Option { + var x: Option :- None; + None +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4731.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4731.dfy.expect new file mode 100644 index 00000000000..00a51f822da --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4731.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 3 verified, 0 errors From a09edd91e88bf73d01b9e62bbe925b5103ebb008 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 1 Nov 2023 13:32:08 -0700 Subject: [PATCH 2/7] Clean up comments in test file --- .../LitTest/dafny0/TypeInferenceRefresh.dfy | 19 ------------------- 1 file changed, 19 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy index ce5c1dfbf02..73e9494a485 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy @@ -1001,15 +1001,6 @@ datatype Tree = // has type nat, so it should hold — and in fact just uncommenting the definition of fn above solves the issue… even if fn isn’t used. -// ------------------ -// From Clement: - -method copy(a: array) returns (a': array) { - a' := new T[a.Length](k requires k < a.Length reads a => a[k]); -} - -// The lambda in a new T is supposed to take a nat, but Dafny infers k to be an int and rejects a[k] - // ------------------ // In this program, one has to write "n + d != 0" instead of "n != -d", because of a previously known problem with type inference @@ -1039,14 +1030,4 @@ predicate method downup_search'(n: int, d: nat) */ } -// ------------------------ -// From https://github.com/dafny-lang/dafny/issues/1292: - -datatype List = None | Cons (hd: T, tl: List) - -method m (x: List) { - match x - case None => {assert 4 > 3;} - case Cons(None, t) => {assert 4 > 3;} -} ****************************************************************************************/ From 919d36942caaa9014389069293ec88102a163373 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 1 Nov 2023 13:43:41 -0700 Subject: [PATCH 3/7] fix: Allow absence of Extract for void outcomes --- .../Resolver/PreType/PreTypeResolve.Expressions.cs | 12 ++++++++---- .../LitTest/exceptions/Exceptions1Expressions.dfy | 2 +- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index 67d2c575b30..9d6bd1fc76e 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -1030,7 +1030,7 @@ private void ConstrainOperandTypes(IToken tok, string opString, Expression e0, E /// "receiverPreType" is an unresolved proxy type and that, after solving more type constraints, "receiverPreType" /// eventually gets set to a type more specific than "tentativeReceiverType". /// - (MemberDecl/*?*/, DPreType/*?*/) FindMember(IToken tok, PreType receiverPreType, string memberName) { + (MemberDecl/*?*/, DPreType/*?*/) FindMember(IToken tok, PreType receiverPreType, string memberName, bool reportErrorOnMissingMember = true) { Contract.Requires(tok != null); Contract.Requires(receiverPreType != null); Contract.Requires(memberName != null); @@ -1046,7 +1046,9 @@ private void ConstrainOperandTypes(IToken tok, string opString, Expression e0, E // TODO: does this case need to do something like this? var cd = ctype?.AsTopLevelTypeWithMembersBypassInternalSynonym; if (!resolver.GetClassMembers(receiverDeclWithMembers).TryGetValue(memberName, out var member)) { - if (memberName == "_ctor") { + if (!reportErrorOnMissingMember) { + // don't report any error + } else if (memberName == "_ctor") { ReportError(tok, $"{receiverDecl.WhatKind} '{receiverDecl.Name}' does not have an anonymous constructor"); } else { ReportError(tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); @@ -1058,7 +1060,9 @@ private void ConstrainOperandTypes(IToken tok, string opString, Expression e0, E return (member, dReceiver); } } - ReportError(tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + if (reportErrorOnMissingMember) { + ReportError(tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } return (null, null); } @@ -2140,7 +2144,7 @@ private void EnsureSupportsErrorHandling(IToken tok, DPreType burritoPreType, bo var (memberIsFailure, _) = FindMember(tok, burritoPreType, "IsFailure"); var (memberPropagate, _) = FindMember(tok, burritoPreType, "PropagateFailure"); - var (memberExtract, _) = FindMember(tok, burritoPreType, "Extract"); + var (memberExtract, _) = FindMember(tok, burritoPreType, "Extract", reportErrorOnMissingMember: expectExtract); if (keyword != null) { if (memberIsFailure == null || (memberExtract != null) != expectExtract) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/Exceptions1Expressions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/Exceptions1Expressions.dfy index a57e5b78c7e..3b9aaf44de8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/Exceptions1Expressions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/Exceptions1Expressions.dfy @@ -1,4 +1,4 @@ -// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment +// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment include "./NatOutcomeDt.dfy" include "./VoidOutcomeDt.dfy" From 466269f3b6ee3cca41d9f9fecaa1548e7ad2ed7e Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 1 Nov 2023 14:50:22 -0700 Subject: [PATCH 4/7] Add method to apply advice for one specific pre-type proxy --- .../Resolver/PreType/PreTypeAdvice.cs | 48 ++++++++++++------- .../Resolver/PreType/PreTypeConstraints.cs | 9 ++++ 2 files changed, 40 insertions(+), 17 deletions(-) diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeAdvice.cs b/Source/DafnyCore/Resolver/PreType/PreTypeAdvice.cs index 782ee0ba2d6..1b49fb7b33d 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeAdvice.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeAdvice.cs @@ -33,26 +33,40 @@ public Advice(PreType preType, Target advice) { public bool Apply(PreTypeResolver preTypeResolver) { if (PreType.Normalize() is PreTypeProxy proxy) { - preTypeResolver.Constraints.DebugPrint($" DEBUG: acting on advice, setting {proxy} := {WhatString}"); - - Type StringDecl() { - var s = preTypeResolver.resolver.moduleInfo.TopLevels["string"]; - return new UserDefinedType(s.tok, s.Name, s, new List()); - } - - var target = What switch { - Target.Bool => preTypeResolver.Type2PreType(Type.Bool), - Target.Char => preTypeResolver.Type2PreType(Type.Char), - Target.Int => preTypeResolver.Type2PreType(Type.Int), - Target.Real => preTypeResolver.Type2PreType(Type.Real), - Target.String => preTypeResolver.Type2PreType(StringDecl()), - Target.Object => preTypeResolver.Type2PreType(preTypeResolver.resolver.SystemModuleManager.ObjectQ()), - _ => throw new cce.UnreachableException() // unexpected case - }; - proxy.Set(target); + ActOnAdvice(proxy, preTypeResolver); return true; } return false; } + + public bool ApplyFor(PreTypeProxy proxy, PreTypeResolver preTypeResolver) { + if (PreType.Normalize() == proxy) { + ActOnAdvice(proxy, preTypeResolver); + return true; + } + return false; + } + + private void ActOnAdvice(PreTypeProxy proxy, PreTypeResolver preTypeResolver) { + // Note, the following debug print may come out _before_ the "Type inference state ..." header, if ActOnAdvice is called + // during what is only a partial constraint solving round. + preTypeResolver.Constraints.DebugPrint($" DEBUG: acting on advice, setting {proxy} := {WhatString}"); + + Type StringDecl() { + var s = preTypeResolver.resolver.moduleInfo.TopLevels["string"]; + return new UserDefinedType(s.tok, s.Name, s, new List()); + } + + var target = What switch { + Target.Bool => preTypeResolver.Type2PreType(Type.Bool), + Target.Char => preTypeResolver.Type2PreType(Type.Char), + Target.Int => preTypeResolver.Type2PreType(Type.Int), + Target.Real => preTypeResolver.Type2PreType(Type.Real), + Target.String => preTypeResolver.Type2PreType(StringDecl()), + Target.Object => preTypeResolver.Type2PreType(preTypeResolver.resolver.SystemModuleManager.ObjectQ()), + _ => throw new cce.UnreachableException() // unexpected case + }; + proxy.Set(target); + } } } diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs b/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs index fc15b7b29d3..02614e40247 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs @@ -456,6 +456,15 @@ bool TryApplyDefaultAdvice() { return anythingChanged; } + bool TryApplyDefaultAdviceFor(PreTypeProxy proxy) { + foreach (var advice in defaultAdvice) { + if (advice.ApplyFor(proxy, PreTypeResolver)) { + return true; + } + } + return false; + } + public void AddConfirmation(CommonConfirmationBag check, PreType preType, IToken tok, string errorFormatString) { confirmations.Add(() => { if (!ConfirmConstraint(check, preType, null)) { From f0707a3f983acf8004a4a5c246dcbcf8b7937be3 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 1 Nov 2023 14:51:15 -0700 Subject: [PATCH 5/7] When resolving :- source type, be willing to look at sub/super constraints and advice --- Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs | 9 ++++++--- .../Resolver/PreType/PreTypeResolve.Expressions.cs | 2 +- .../Resolver/PreType/PreTypeResolve.Statements.cs | 2 +- 3 files changed, 8 insertions(+), 5 deletions(-) diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs b/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs index 02614e40247..47537846cfd 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs @@ -74,7 +74,7 @@ public DPreType ApproximateReceiverType(IToken tok, PreType preType, [CanBeNull] /// Expecting that "preType" is a type that does not involve traits, return that type, if possible. /// [CanBeNull] - public DPreType FindDefinedPreType(PreType preType) { + public DPreType FindDefinedPreType(PreType preType, bool applyAdvice) { Contract.Requires(preType != null); PartiallySolveTypeConstraints(); @@ -89,10 +89,13 @@ public DPreType FindDefinedPreType(PreType preType) { foreach (var super in AllSuperBounds(proxy, new HashSet())) { return super; } - return null; + + if (applyAdvice) { + TryApplyDefaultAdviceFor(proxy); + } } - return preType as DPreType; + return preType.Normalize() as DPreType; } /// diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index 9d6bd1fc76e..2f31502a6ba 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -1625,7 +1625,7 @@ ModuleResolver.MethodCallInformation ResolveApplySuffix(ApplySuffix e, Resolutio } if (r == null) { // e.Lhs denotes a function value, or at least it's used as if it were - var dp = Constraints.FindDefinedPreType(e.Lhs.PreType); + var dp = Constraints.FindDefinedPreType(e.Lhs.PreType, false); if (dp != null && DPreType.IsArrowType(dp.Decl)) { // e.Lhs does denote a function value // In the general case, we'll resolve this as an ApplyExpr, but in the more common case of the Lhs diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs index 083a9eedd01..e732d6b1eaa 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs @@ -1007,7 +1007,7 @@ private void ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ResolutionContext r } TopLevelDeclWithMembers failureSupportingType = null; if (firstPreType != null) { - Constraints.PartiallySolveTypeConstraints(); + Constraints.FindDefinedPreType(firstPreType, true); failureSupportingType = (firstPreType.Normalize() as DPreType)?.Decl as TopLevelDeclWithMembers; if (failureSupportingType != null) { if (failureSupportingType.Members.Find(x => x.Name == "IsFailure") == null) { From 8ecb21dcce161c8097298a089bfecdbbeaaca74f Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 1 Nov 2023 14:53:05 -0700 Subject: [PATCH 6/7] Convert tests to also use new resolver --- .../LitTests/LitTest/exceptions/ParseErrors.dfy | 4 ++-- .../exceptions/ParseErrors.dfy.refresh.expect | 4 ++++ .../LitTests/LitTest/exceptions/TypecheckErrors.dfy | 10 +++++----- .../LitTest/exceptions/TypecheckErrors.dfy.expect | 4 +--- .../exceptions/TypecheckErrors.dfy.refresh.expect | 12 ++++++++++++ .../LitTest/exceptions/VerificationErrors.dfy | 4 ++-- 6 files changed, 26 insertions(+), 12 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/ParseErrors.dfy.refresh.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy.refresh.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/ParseErrors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/ParseErrors.dfy index 1d433774461..6e21d5470f2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/ParseErrors.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/ParseErrors.dfy @@ -1,5 +1,5 @@ -// RUN: %exits-with 2 %dafny "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" + include "./NatOutcome.dfy" include "./VoidOutcome.dfy" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/ParseErrors.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/ParseErrors.dfy.refresh.expect new file mode 100644 index 00000000000..cafd7fee566 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/ParseErrors.dfy.refresh.expect @@ -0,0 +1,4 @@ +ParseErrors.dfy(9,15): Error: number of lhs (2) must match number of rhs (1) for a rhs type (NatOutcome) with member Extract +ParseErrors.dfy(10,15): Error: member IsFailure does not exist in int, in :- statement +ParseErrors.dfy(16,4): Error: number of lhs (0) must be one less than number of rhs (2) for a rhs type (VoidOutcome) without member Extract +3 resolution/type errors detected in ParseErrors.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy index 04e43d8da5c..a646da421d7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy @@ -1,5 +1,5 @@ -// RUN: %exits-with 2 %dafny "%s" /dprint:"%t.dprint" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" + include "./NatOutcome.dfy" include "./VoidOutcome.dfy" @@ -10,11 +10,11 @@ method TestTypecheckingInDesugaredTerm_Nat() returns (res: NatOutcome) { } method RedeclareVar_Nat() returns (res: NatOutcome) { - var a := MakeNatSuccess(42); + var x := MakeNatSuccess(42); var a :- MakeNatSuccess(43); var b :- MakeNatSuccess(44); - var b := MakeNatSuccess(45); - return a; + var y := MakeNatSuccess(45); + return x; } trait BadOutcome1 { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy.expect index 4e7c72dc7c0..62e9e41df03 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy.expect @@ -1,7 +1,5 @@ TypecheckErrors.dfy(7,28): Error: incorrect argument type for method in-parameter 'n' (expected nat, found string) TypecheckErrors.dfy(8,28): Error: incorrect argument type for method in-parameter 'n' (expected nat, found string) -TypecheckErrors.dfy(14,8): Error: Duplicate local-variable name: a -TypecheckErrors.dfy(16,8): Error: Duplicate local-variable name: b TypecheckErrors.dfy(39,10): Error: member IsFailure does not exist in BadOutcome1?, in :- statement TypecheckErrors.dfy(43,10): Error: member 'PropagateFailure' does not exist in trait 'BadOutcome2' TypecheckErrors.dfy(43,10): Error: The right-hand side of ':-', which is of type 'BadOutcome2?', must have functions 'IsFailure()', 'PropagateFailure()', and 'Extract()' @@ -11,4 +9,4 @@ TypecheckErrors.dfy(71,4): Error: member IsFailure does not exist in BadVoidOutc TypecheckErrors.dfy(75,4): Error: member 'PropagateFailure' does not exist in trait 'BadVoidOutcome2' TypecheckErrors.dfy(75,4): Error: The right-hand side of ':-', which is of type 'BadVoidOutcome2?', must have functions 'IsFailure()' and 'PropagateFailure()', but not 'Extract()' TypecheckErrors.dfy(79,4): Error: number of lhs (0) must match number of rhs (1) for a rhs type (BadVoidOutcome3?) with member Extract -13 resolution/type errors detected in TypecheckErrors.dfy +11 resolution/type errors detected in TypecheckErrors.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy.refresh.expect new file mode 100644 index 00000000000..bc5158e0762 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy.refresh.expect @@ -0,0 +1,12 @@ +TypecheckErrors.dfy(7,29): Error: string literal used as if it had type int +TypecheckErrors.dfy(8,29): Error: string literal used as if it had type int +TypecheckErrors.dfy(39,10): Error: member IsFailure does not exist in BadOutcome1, in :- statement +TypecheckErrors.dfy(43,10): Error: member 'PropagateFailure' does not exist in trait 'BadOutcome2' +TypecheckErrors.dfy(43,10): Error: The right-hand side of ':-', which is of type 'BadOutcome2', must have functions 'IsFailure()', 'PropagateFailure()', and 'Extract()' +TypecheckErrors.dfy(47,10): Error: number of lhs (1) must be one less than number of rhs (1) for a rhs type (BadOutcome3) without member Extract +TypecheckErrors.dfy(51,23): Error: integer literal used as if it had type seq +TypecheckErrors.dfy(71,4): Error: member IsFailure does not exist in BadVoidOutcome1, in :- statement +TypecheckErrors.dfy(75,4): Error: member 'PropagateFailure' does not exist in trait 'BadVoidOutcome2' +TypecheckErrors.dfy(75,4): Error: The right-hand side of ':-', which is of type 'BadVoidOutcome2', must have functions 'IsFailure()' and 'PropagateFailure()', but not 'Extract()' +TypecheckErrors.dfy(79,4): Error: number of lhs (0) must match number of rhs (1) for a rhs type (BadVoidOutcome3) with member Extract +11 resolution/type errors detected in TypecheckErrors.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/VerificationErrors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/VerificationErrors.dfy index a6db6261f7c..8fe9203c3fd 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/VerificationErrors.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/VerificationErrors.dfy @@ -1,5 +1,5 @@ -// RUN: %exits-with 4 %dafny "%s" /rprint:"%t.rprint" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" + include "./NatOutcome.dfy" include "./VoidOutcome.dfy" From a5dbf9ca6a1cb3cd31e1f6595119e241a10427ab Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 1 Nov 2023 15:02:46 -0700 Subject: [PATCH 7/7] Add release notes --- docs/dev/news/4734.fix | 1 + 1 file changed, 1 insertion(+) create mode 100644 docs/dev/news/4734.fix diff --git a/docs/dev/news/4734.fix b/docs/dev/news/4734.fix new file mode 100644 index 00000000000..82341d9eb4b --- /dev/null +++ b/docs/dev/news/4734.fix @@ -0,0 +1 @@ +Resolve :- expressions with void outcomes in new resolver