diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index 03a2961bd80..1376e0e7721 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -435,26 +435,23 @@ public bool Resolve(ModuleSignature sig, ModuleResolver resolver, string exportS sig.VisibilityScope.Augment(resolver.ProgramResolver.SystemModuleManager.systemNameInfo.VisibilityScope); // make sure all imported modules were successfully resolved foreach (var d in TopLevelDecls) { - if (d is AliasModuleDecl || d is AbstractModuleDecl) { - ModuleSignature importSig; - if (d is AliasModuleDecl) { - var alias = (AliasModuleDecl)d; - importSig = alias.TargetQId.Root != null ? alias.TargetQId.Root.Signature : alias.Signature; - } else { - importSig = ((AbstractModuleDecl)d).OriginalSignature; + if (d is AliasModuleDecl importDecl) { + var importSig = importDecl.TargetQId.Root != null ? importDecl.TargetQId.Root.Signature : importDecl.Signature; + if (importSig is not { ModuleDef: { SuccessfullyResolved: true } }) { + return false; } - + } else if (d is AbstractModuleDecl abstractImportDecl) { + var importSig = abstractImportDecl.OriginalSignature; if (importSig is not { ModuleDef: { SuccessfullyResolved: true } }) { return false; } - } else if (d is LiteralModuleDecl) { - var nested = (LiteralModuleDecl)d; - if (!nested.ModuleDef.SuccessfullyResolved) { + } else if (d is LiteralModuleDecl nestedModuleDecl) { + if (!nestedModuleDecl.ModuleDef.SuccessfullyResolved) { if (!IsEssentiallyEmptyModuleBody()) { // say something only if this will cause any testing to be omitted - resolver.reporter.Error(MessageSource.Resolver, nested, + resolver.reporter.Error(MessageSource.Resolver, nestedModuleDecl, "not resolving module '{0}' because there were errors in resolving its nested module '{1}'", Name, - nested.Name); + nestedModuleDecl.Name); } return false; @@ -952,6 +949,7 @@ private void DetermineReferenceTypes(ModuleResolver resolver, ModuleSignature si // In the following dictionary, a TraitDecl not being present among the keys means it has not been visited in the InheritsFromObject traversal. // If a TraitDecl is a key and maps to "false", then it is currently being visited. // If a TraitDecl is a key and maps to "true", then its .IsReferenceTypeDecl has been computed and is ready to be used. + var openedImports = TopLevelDecls.OfType().Where(d => d.Opened).ToList(); var traitsProgress = new Dictionary(); foreach (var decl in TopLevelDecls.Where(d => d is TraitDecl)) { // Resolve a "path" to a top-level declaration, if possible. On error, return null. @@ -969,9 +967,22 @@ TopLevelDecl ResolveNamePath(Expression path) { // For "object" and other reference-type declarations from other modules, we're picking up the NonNullTypeDecl; if so, return // the original declaration. return topLevelDecl is NonNullTypeDecl nntd ? nntd.ViewAsClass : topLevelDecl; - } else { - return null; } + // Look through opened imports (which haven't yet been added to the module's signature). There may be ambiguities among the declarations + // of these opened imports. Still, we'll just pick the first declaration that matches, if any. If this declaration turns out to be + // ambiguous, then an error will be reported later; in the meantime, all that would have happened is that the resolved name path here + // is referring to some top-level declaration that won't accurately answer the question of whether "path" is referring to a reference + // type or not. + foreach (var importDecl in openedImports) { + Contract.Assert(importDecl is AliasModuleDecl or AbstractModuleDecl); // only these ModuleDecl's can be .Opened + if (importDecl.AccessibleSignature(false).TopLevels.TryGetValue(nameSegment.Name, out topLevelDecl)) { + // For "object" and other reference-type declarations from other modules, we're picking up the NonNullTypeDecl; if so, return + // the original declaration. + return topLevelDecl is NonNullTypeDecl nntd ? nntd.ViewAsClass : topLevelDecl; + } + } + // We didn't find "path" + return null; } // convert the ExprDotName to a list of strings diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index b4a60bff93f..9c8f34e5191 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -408,8 +408,7 @@ public void ResolveModuleExport(LiteralModuleDecl literalDecl, ModuleSignature s foreach (var s in sigs) { foreach (var decl in s.TopLevels) { - if (decl.Value is ModuleDecl && !(decl.Value is ModuleExportDecl)) { - var modDecl = (ModuleDecl)decl.Value; + if (decl.Value is ModuleDecl modDecl and not ModuleExportDecl) { s.VisibilityScope.Augment(modDecl.AccessibleSignature().VisibilityScope); } } @@ -428,7 +427,7 @@ public void ResolveModuleExport(LiteralModuleDecl literalDecl, ModuleSignature s } } - if (e.Opaque && (decl is DatatypeDecl || decl is TypeSynonymDecl)) { + if (e.Opaque && (decl is DatatypeDecl or TypeSynonymDecl)) { // Datatypes and type synonyms are marked as _provided when they appear in any provided export. If a // declaration is never provided, then either it isn't visible outside the module at all or its whole // definition is. Datatype and type-synonym declarations undergo some inference from their definitions. diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs index adca8fbdbac..77f255a84a6 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs @@ -893,17 +893,18 @@ public Boogie.Expr TrExpr(Expression expr) { e0 = BoxIfNecessary(expr.tok, e0, e.E0.Type); oe0 = BoxIfNecessary(expr.tok, oe0, e.E0.Type); } - var cot = e.E0.Type.AsCoDatatype; - if (cot != null) { + if (e.E0.Type.IsCoDatatype && e.E1.Type.IsCoDatatype) { var e0args = e.E0.Type.NormalizeExpand().TypeArgs; var e1args = e.E1.Type.NormalizeExpand().TypeArgs; - return BoogieGenerator.CoEqualCall(cot, e0args, e1args, null, this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e0, e1, GetToken(binaryExpr)); + return BoogieGenerator.CoEqualCall(e.E0.Type.AsCoDatatype, e0args, e1args, null, + this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e0, e1, GetToken(binaryExpr)); } - if (e.E0.Type.IsIndDatatype) { + if (e.E0.Type.IsIndDatatype && e.E1.Type.IsIndDatatype) { return BoogieGenerator.TypeSpecificEqual(GetToken(binaryExpr), e.E0.Type, e0, e1); } typ = Boogie.Type.Bool; - bOpcode = BinaryOperator.Opcode.Eq; break; + bOpcode = BinaryOperator.Opcode.Eq; + break; case BinaryExpr.ResolvedOpcode.NeqCommon: if (ModeledAsBoxType(e.E0.Type)) { e1 = BoxIfNecessary(expr.tok, e1, e.E1.Type); @@ -912,19 +913,20 @@ public Boogie.Expr TrExpr(Expression expr) { e0 = BoxIfNecessary(expr.tok, e0, e.E0.Type); oe0 = BoxIfNecessary(expr.tok, oe0, e.E0.Type); } - var cotx = e.E0.Type.AsCoDatatype; - if (cotx != null) { + if (e.E0.Type.IsCoDatatype && e.E1.Type.IsCoDatatype) { var e0args = e.E0.Type.NormalizeExpand().TypeArgs; var e1args = e.E1.Type.NormalizeExpand().TypeArgs; - var eq = BoogieGenerator.CoEqualCall(cotx, e0args, e1args, null, this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e0, e1, GetToken(binaryExpr)); + var eq = BoogieGenerator.CoEqualCall(e.E0.Type.AsCoDatatype, e0args, e1args, null, + this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e0, e1, GetToken(binaryExpr)); return Boogie.Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, eq); } - if (e.E0.Type.IsIndDatatype) { + if (e.E0.Type.IsIndDatatype && e.E1.Type.IsIndDatatype) { var eq = BoogieGenerator.TypeSpecificEqual(GetToken(binaryExpr), e.E0.Type, e0, e1); return Boogie.Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, eq); } typ = Boogie.Type.Bool; - bOpcode = BinaryOperator.Opcode.Neq; break; + bOpcode = BinaryOperator.Opcode.Neq; + break; case BinaryExpr.ResolvedOpcode.Lt: if (0 <= bvWidth) { return TrToFunctionCall(GetToken(binaryExpr), "lt_bv" + bvWidth, Boogie.Type.Bool, e0, e1, liftLit); @@ -2112,15 +2114,13 @@ public Expr CanCallAssumption(Expression expr) { case BinaryExpr.ResolvedOpcode.EqCommon: case BinaryExpr.ResolvedOpcode.NeqCommon: { Boogie.Expr r = Boogie.Expr.True; - var dt = e.E0.Type.AsDatatype; - if (dt != null) { - var funcID = new Boogie.FunctionCall(new Boogie.IdentifierExpr(expr.tok, "$IsA#" + dt.FullSanitizedName, Boogie.Type.Bool)); - if (!(e.E0.Resolved is DatatypeValue)) { - r = BplAnd(r, new Boogie.NAryExpr(expr.tok, funcID, new List { TrExpr(e.E0) })); - } - if (!(e.E1.Resolved is DatatypeValue)) { - r = BplAnd(r, new Boogie.NAryExpr(expr.tok, funcID, new List { TrExpr(e.E1) })); - } + if (e.E0 is { Type: { AsDatatype: { } dt0 }, Resolved: not DatatypeValue }) { + var funcID = new Boogie.FunctionCall(new Boogie.IdentifierExpr(expr.tok, "$IsA#" + dt0.FullSanitizedName, Boogie.Type.Bool)); + r = BplAnd(r, new Boogie.NAryExpr(expr.tok, funcID, new List { TrExpr(e.E0) })); + } + if (e.E1 is { Type: { AsDatatype: { } dt1 }, Resolved: not DatatypeValue }) { + var funcID = new Boogie.FunctionCall(new Boogie.IdentifierExpr(expr.tok, "$IsA#" + dt1.FullSanitizedName, Boogie.Type.Bool)); + r = BplAnd(r, new Boogie.NAryExpr(expr.tok, funcID, new List { TrExpr(e.E1) })); } return BplAnd(r, BplAnd(t0, t1)); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936a.dfy new file mode 100644 index 00000000000..d04391b9792 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936a.dfy @@ -0,0 +1,16 @@ +// RUN: %testDafnyForEachResolver "%s" -- --general-traits:datatype + +module X { + trait {:termination false} A extends object {} +} + +module Y { + import opened X + + trait B extends A { + function GetIndex(): nat + // The following once gave an error, complaining that B is not a reference type. The problem had been that + // the opened import A was, effectively, hiding the information that A is a reference type. + reads this + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936a.dfy.expect new file mode 100644 index 00000000000..012f5b99379 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936a.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936b.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936b.dfy new file mode 100644 index 00000000000..d7f947ee136 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936b.dfy @@ -0,0 +1,19 @@ +// RUN: %testDafnyForEachResolver "%s" -- --general-traits:datatype + +module X { + trait K { } + trait {:termination false} A extends object, K {} +} + +module Y { + import opened X + + trait B extends A { } + + method Test(b: B) returns (a: A) { + // The following assignment once caused malformed Boogie to be generated. The reason had been that + // the resolver had not determined B to be a reference type. And that, in turn, had been caused by + // that the opened import, effectively, had lost the "extends object" information. + a := b; + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936b.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936b.dfy.expect new file mode 100644 index 00000000000..823a60a105c --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936b.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 1 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936c.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936c.dfy new file mode 100644 index 00000000000..f4f1dfdeafc --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936c.dfy @@ -0,0 +1,97 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits:datatype + +// The early-resolver code that figures out if a trait is a reference type or not is operating so early +// in the resolver pipeline that opened imports have not yet been resolved into the importing module. +// Thus, this early-resolver code looks directly into the top-level members of opened imports, but does +// so without consideration for possible ambiguities. This means that the early-resolver code may not +// properly figure out if a trait is a reference type or not. But if it gets it wrong, the ambiguity +// will still be reported as an error later in the resolver pipeline. +// +// This test file makes sure that the ambiguous-import errors are indeed being reported and that the +// resolver doesn't crash until then. + +module X0 { + // Here, A is a reference type + trait {:termination false} A extends object {} +} + +module X1 { + // Here, A is not a reference type + trait {:termination false} A {} +} + +module X2 { + // Here, A is not a reference type; in fact, it isn't even a type + const A: object? +} + +module Y01 { + import opened X0 + import opened X1 + + trait B extends A { // error: A is ambiguous + function GetIndex(): nat + reads this + } +} + +module Y10 { + import opened X1 + import opened X0 + + trait B extends A { // error: A is ambiguous + function GetIndex(): nat + reads this + } +} + +module Y0123 { + import opened X0 + import opened X1 + import opened X2 + + trait B extends A { // error: A is ambiguous + function GetIndex(): nat + reads this + } +} + +module Y210 { + import opened X2 + import opened X1 + import opened X0 + + trait B extends A { // error: A is ambiguous + function GetIndex(): nat + reads this + } +} + +module Z { + import opened X0 + import opened X1 + import opened X2 + +} + +module Z1 { + import opened X0 + import opened X1 + import opened X2 + + trait B extends X0.A { // no problem, since X0.A is fully qualified + function GetIndex(): nat + reads this // no problem, since B is a reference type + } +} + +module Z2 { + import opened X0 + import opened X1 + import opened X2 + + trait B extends X1.A { // no problem, since X1.A is fully qualified + function GetIndex(): nat + reads this // error: B is not a reference type + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936c.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936c.dfy.expect new file mode 100644 index 00000000000..db24a819468 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936c.dfy.expect @@ -0,0 +1,6 @@ +git-issue-4936c.dfy(32,18): Error: The name A ambiguously refers to a type in one of the modules X0, X1 (try qualifying the type name with the module name) +git-issue-4936c.dfy(42,18): Error: The name A ambiguously refers to a type in one of the modules X1, X0 (try qualifying the type name with the module name) +git-issue-4936c.dfy(53,18): Error: The name A ambiguously refers to a type in one of the modules X0, X1 (try qualifying the type name with the module name) +git-issue-4936c.dfy(64,18): Error: The name A ambiguously refers to a type in one of the modules X1, X0 (try qualifying the type name with the module name) +git-issue-4936c.dfy(95,12): 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 B) +5 resolution/type errors detected in git-issue-4936c.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936d.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936d.dfy new file mode 100644 index 00000000000..214864f6dbf --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936d.dfy @@ -0,0 +1,58 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits:datatype + +module X { + export Public + provides A + export Friends + reveals A + + trait {:termination false} A extends object {} +} + +module Y0 { + import opened X`Public + + trait B extends A { // error: A is not even known to be a trait + function GetIndex(): nat + reads this + } +} + +module Y1 { + import opened X`Friends + + trait B extends A { + function GetIndex(): nat + reads this // fine, since B is known to be a reference type + } +} + +module Y2 { + import opened I = X`Friends + import opened J = X`Public + + trait B extends A { + function GetIndex(): nat + reads this // fine, since B is known to be a reference type + } +} + +module Y3 { + import opened X`Friends + import opened J = X`Public + + trait B extends J.A { // fine, since the module also imports X`Friends + function GetIndex(): nat + reads this // fine, since B is known to be a reference type + } +} + +module Y4 { + import I = X`Friends + import J = X`Public + + trait B extends J.A { // fine, since the module also imports X`Friends + function GetIndex(): nat + reads this // fine, since B is known to be a reference type + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936d.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936d.dfy.expect new file mode 100644 index 00000000000..8be963e3829 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936d.dfy.expect @@ -0,0 +1,2 @@ +git-issue-4936d.dfy(15,18): Error: a trait can only extend traits (found 'A') +1 resolution/type errors detected in git-issue-4936d.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4983.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4983.dfy new file mode 100644 index 00000000000..dd426e8fd3e --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4983.dfy @@ -0,0 +1,27 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=2 --refresh-exit-code=0 "%s" -- --general-traits:datatype + +trait Parent {} + +datatype Dt extends Parent = Dt { + function GetParent(): Parent { + // The implicit conversion in the following line once caused malformed Boogie to be generated + this // error (in the legacy resolver): legacy resolver does not understand subtyping relationship with Parent + } +} + +function GetDtAsParent(): Parent { + // The implicit conversion in the following line once caused malformed Boogie to be generated + Dt // error (in the legacy resolver): legacy resolver does not understand subtyping relationship with Parent +} + +type Abstract extends Parent { + function GetParent(): Parent { + this // error (in the legacy resolver): legacy resolver does not understand subtyping relationship with Parent + } +} + +function GetAbstract(): Abstract + +function GetAbstractAsParent(): Parent { + GetAbstract() // error (in the legacy resolver): legacy resolver does not understand subtyping relationship with Parent +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4983.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4983.dfy.expect new file mode 100644 index 00000000000..e78aafeff32 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4983.dfy.expect @@ -0,0 +1,5 @@ +git-issue-4983.dfy(12,9): Error: Function body type mismatch (expected Parent, got Dt) +git-issue-4983.dfy(25,9): Error: Function body type mismatch (expected Parent, got Abstract) +git-issue-4983.dfy(6,11): Error: Function body type mismatch (expected Parent, got Dt) +git-issue-4983.dfy(18,11): Error: Function body type mismatch (expected Parent, got Abstract) +4 resolution/type errors detected in git-issue-4983.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4983.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4983.dfy.refresh.expect new file mode 100644 index 00000000000..012f5b99379 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4983.dfy.refresh.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4994.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4994.dfy new file mode 100644 index 00000000000..7a2803ecda1 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4994.dfy @@ -0,0 +1,46 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=2 --refresh-exit-code=4 "%s" -- --general-traits=datatype + +trait Parent {} + +datatype D extends Parent = D +codatatype Co extends Parent = Co + +method TestAEq(d: D, co: Co, p: Parent) { + // The expressions in these assertions once caused malformed Boogie + if + case true => + assert p == d; // error: possible assertion violation + case true => + assert d == p; // error: possible assertion violation + case true => + assert p == co; // error: possible assertion violation + case true => + assert co == p; // error: possible assertion violation +} + +method TestANeq(d: D, co: Co, p: Parent) { + // The expressions in these assertions once caused malformed Boogie + if + case true => + assert p != d; // error: possible assertion violation + case true => + assert d != p; // error: possible assertion violation + case true => + assert p != co; // error: possible assertion violation + case true => + assert co != p; // error: possible assertion violation +} + +method TestB(d: D, co: Co, p: Parent) returns (ghost b: bool) { + b := p == d; + b := d == p; + + b := p == co; + b := co == p; + + b := p != d; + b := d != p; + + b := p != co; + b := co != p; +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4994.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4994.dfy.expect new file mode 100644 index 00000000000..5cc0f6c6612 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4994.dfy.expect @@ -0,0 +1,17 @@ +git-issue-4994.dfy(12,13): Error: arguments must have comparable types (got Parent and D) +git-issue-4994.dfy(14,13): Error: arguments must have comparable types (got D and Parent) +git-issue-4994.dfy(16,13): Error: arguments must have comparable types (got Parent and Co) +git-issue-4994.dfy(18,14): Error: arguments must have comparable types (got Co and Parent) +git-issue-4994.dfy(25,13): Error: arguments must have comparable types (got Parent and D) +git-issue-4994.dfy(27,13): Error: arguments must have comparable types (got D and Parent) +git-issue-4994.dfy(29,13): Error: arguments must have comparable types (got Parent and Co) +git-issue-4994.dfy(31,14): Error: arguments must have comparable types (got Co and Parent) +git-issue-4994.dfy(35,9): Error: arguments must have comparable types (got Parent and D) +git-issue-4994.dfy(36,9): Error: arguments must have comparable types (got D and Parent) +git-issue-4994.dfy(38,9): Error: arguments must have comparable types (got Parent and Co) +git-issue-4994.dfy(39,10): Error: arguments must have comparable types (got Co and Parent) +git-issue-4994.dfy(41,9): Error: arguments must have comparable types (got Parent and D) +git-issue-4994.dfy(42,9): Error: arguments must have comparable types (got D and Parent) +git-issue-4994.dfy(44,9): Error: arguments must have comparable types (got Parent and Co) +git-issue-4994.dfy(45,10): Error: arguments must have comparable types (got Co and Parent) +16 resolution/type errors detected in git-issue-4994.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4994.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4994.dfy.refresh.expect new file mode 100644 index 00000000000..f3d13863946 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4994.dfy.refresh.expect @@ -0,0 +1,10 @@ +git-issue-4994.dfy(12,13): Error: assertion might not hold +git-issue-4994.dfy(14,13): Error: assertion might not hold +git-issue-4994.dfy(16,13): Error: assertion might not hold +git-issue-4994.dfy(18,14): Error: assertion might not hold +git-issue-4994.dfy(25,13): Error: assertion might not hold +git-issue-4994.dfy(27,13): Error: assertion might not hold +git-issue-4994.dfy(29,13): Error: assertion might not hold +git-issue-4994.dfy(31,14): Error: assertion might not hold + +Dafny program verifier finished with 1 verified, 8 errors diff --git a/docs/dev/news/5058.fix b/docs/dev/news/5058.fix new file mode 100644 index 00000000000..f87fbc2386c --- /dev/null +++ b/docs/dev/news/5058.fix @@ -0,0 +1,5 @@ +A parent trait that is a reference type can now be named via `import opened`. + +Implicit conversions between a datatype and its parent traits no longer crashes the verifier. + +(Dis)equality expressions of a (co)datatype and its parent traits no longer crashes the verifier.