From 4a1108c85b1e7fb162702a10074e3f00755ea10b Mon Sep 17 00:00:00 2001 From: Nathan Taylor Date: Tue, 29 Nov 2022 11:04:51 -0600 Subject: [PATCH 1/4] Do not refer to an implicit assignment in error messages on return statements Previously, a type error in a method `return` statement refers to an assignment, because the Resolver treats a return as an implicit update to the named return variable. This patch checks whether an assignment is updating a formal outparameter and produces a more specific error message if so. --- Source/DafnyCore/Resolver/Resolver.cs | 17 ++++++++++++++- Test/dafny0/BitvectorResolution.dfy.expect | 8 ++++---- Test/dafny0/ByMethodResolution.dfy.expect | 4 ++-- Test/dafny0/ConstantErrors.dfy.expect | 2 +- Test/dafny0/DisplayExpressions.dfy.expect | 2 +- Test/dafny0/ForLoops-Resolution.dfy.expect | 4 ++-- Test/dafny0/NewtypesResolution.dfy.expect | 4 ++-- Test/dafny0/ResolutionErrors.dfy.expect | 24 +++++++++++----------- Test/dafny0/SubsetTypesERR.dfy.expect | 4 ++-- Test/dafny0/TypeConstraints.dfy.expect | 12 +++++------ Test/exports/ExportResolve.dfy.expect | 10 ++++----- Test/git-issues/git-issue-3125.dfy | 10 +++++++++ Test/git-issues/git-issue-3125.dfy.expect | 3 +++ Test/traits/TraitPolymorphism.dfy.expect | 2 +- docs/dev/news/3125.fix | 1 + 15 files changed, 68 insertions(+), 39 deletions(-) create mode 100644 Test/git-issues/git-issue-3125.dfy create mode 100644 Test/git-issues/git-issue-3125.dfy.expect create mode 100644 docs/dev/news/3125.fix diff --git a/Source/DafnyCore/Resolver/Resolver.cs b/Source/DafnyCore/Resolver/Resolver.cs index 4fcb1be2677..3cdad94d608 100644 --- a/Source/DafnyCore/Resolver/Resolver.cs +++ b/Source/DafnyCore/Resolver/Resolver.cs @@ -9742,7 +9742,22 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext ExprRhs rr = (ExprRhs)s.Rhs; ResolveExpression(rr.Expr, resolutionContext); Contract.Assert(rr.Expr.Type != null); // follows from postcondition of ResolveExpression - AddAssignableConstraint(stmt.Tok, lhsType, rr.Expr.Type, "RHS (of type {1}) not assignable to LHS (of type {0})"); + + bool isHiddenUpdateToOutVar = false; + if (s.Lhs is IdentifierExpr) { + IdentifierExpr ie = (IdentifierExpr)s.Lhs; + if (ie.Var is Formal) { + Formal f = ((Formal)ie.Var); + if (!f.InParam) { + isHiddenUpdateToOutVar = true; + } + } + } + if (isHiddenUpdateToOutVar) { + AddAssignableConstraint(stmt.Tok, lhsType, rr.Expr.Type, "Method return value mismatch (expecting {0}, got {1})"); + } else { + AddAssignableConstraint(stmt.Tok, lhsType, rr.Expr.Type, "RHS (of type {1}) not assignable to LHS (of type {0})"); + } } else if (s.Rhs is TypeRhs) { TypeRhs rr = (TypeRhs)s.Rhs; Type t = ResolveTypeRhs(rr, stmt, resolutionContext); diff --git a/Test/dafny0/BitvectorResolution.dfy.expect b/Test/dafny0/BitvectorResolution.dfy.expect index 2b3b55d42be..1bfc561e691 100644 --- a/Test/dafny0/BitvectorResolution.dfy.expect +++ b/Test/dafny0/BitvectorResolution.dfy.expect @@ -2,10 +2,10 @@ BitvectorResolution.dfy(9,13): Error: literal (5000) is too large for the bitvec BitvectorResolution.dfy(15,9): Error: literal (1) is too large for the bitvector type bv0 BitvectorResolution.dfy(18,9): Error: literal (4294967296) is too large for the bitvector type bv32 BitvectorResolution.dfy(24,12): Error: literal (1) is too large for the bitvector type bv0 -BitvectorResolution.dfy(35,6): Error: RHS (of type bv67) not assignable to LHS (of type int) -BitvectorResolution.dfy(36,6): Error: RHS (of type bv67) not assignable to LHS (of type int) -BitvectorResolution.dfy(38,6): Error: RHS (of type bv67) not assignable to LHS (of type int) -BitvectorResolution.dfy(39,6): Error: RHS (of type bv67) not assignable to LHS (of type int) +BitvectorResolution.dfy(35,6): Error: Method return value mismatch (expecting int, got bv67) +BitvectorResolution.dfy(36,6): Error: Method return value mismatch (expecting int, got bv67) +BitvectorResolution.dfy(38,6): Error: Method return value mismatch (expecting int, got bv67) +BitvectorResolution.dfy(39,6): Error: Method return value mismatch (expecting int, got bv67) BitvectorResolution.dfy(40,15): Error: type of right argument to << (real) must be an integer-numeric or bitvector type BitvectorResolution.dfy(41,15): Error: type of right argument to << (SmallReal) must be an integer-numeric or bitvector type BitvectorResolution.dfy(42,25): Error: incorrect argument type for function parameter 'w' (expected nat, found real) diff --git a/Test/dafny0/ByMethodResolution.dfy.expect b/Test/dafny0/ByMethodResolution.dfy.expect index d848c1a5b2e..aad4bd0a434 100644 --- a/Test/dafny0/ByMethodResolution.dfy.expect +++ b/Test/dafny0/ByMethodResolution.dfy.expect @@ -1,6 +1,6 @@ ByMethodResolution.dfy(17,6): Error: number of return parameters does not match declaration (found 2, expected 1) -ByMethodResolution.dfy(25,4): Error: RHS (of type bv9) not assignable to LHS (of type real) -ByMethodResolution.dfy(24,6): Error: RHS (of type int) not assignable to LHS (of type real) +ByMethodResolution.dfy(25,4): Error: Method return value mismatch (expecting real, got bv9) +ByMethodResolution.dfy(24,6): Error: Method return value mismatch (expecting real, got int) ByMethodResolution.dfy(63,13): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function with 'function method') ByMethodResolution.dfy(64,13): Error: a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') ByMethodResolution.dfy(65,13): Error: a call to a twostate function is allowed only in specification contexts diff --git a/Test/dafny0/ConstantErrors.dfy.expect b/Test/dafny0/ConstantErrors.dfy.expect index 822a2a41c35..26596c65606 100644 --- a/Test/dafny0/ConstantErrors.dfy.expect +++ b/Test/dafny0/ConstantErrors.dfy.expect @@ -3,7 +3,7 @@ ConstantErrors.dfy(12,8): Error: const definition contains a cycle: five -> six ConstantErrors.dfy(21,6): Error: 'this' is not allowed in a 'static' context ConstantErrors.dfy(32,6): Error: a ghost const field is allowed only in specification contexts ConstantErrors.dfy(33,6): Error: a ghost const field is allowed only in specification contexts -ConstantErrors.dfy(44,7): Error: RHS (of type int) not assignable to LHS (of type SmallInt) +ConstantErrors.dfy(44,7): Error: Method return value mismatch (expecting SmallInt, got int) ConstantErrors.dfy(67,10): Error: const field 'x0' is inherited from trait 'Trait' and is not allowed to be re-declared ConstantErrors.dfy(68,10): Error: const field 'x1' is inherited from trait 'Trait' and is not allowed to be re-declared ConstantErrors.dfy(69,10): Error: const field 'x2' is inherited from trait 'Trait' and is not allowed to be re-declared diff --git a/Test/dafny0/DisplayExpressions.dfy.expect b/Test/dafny0/DisplayExpressions.dfy.expect index d2714fa8123..1c24392274c 100644 --- a/Test/dafny0/DisplayExpressions.dfy.expect +++ b/Test/dafny0/DisplayExpressions.dfy.expect @@ -3,6 +3,6 @@ DisplayExpressions.dfy(12,8): Error: the type of this variable is underspecified DisplayExpressions.dfy(17,8): Error: the type of this variable is underspecified DisplayExpressions.dfy(22,8): Error: the type of this variable is underspecified DisplayExpressions.dfy(27,14): Error: the type of this expression is underspecified -DisplayExpressions.dfy(42,6): Error: RHS (of type seq) not assignable to LHS (of type seq) (covariant type parameter would require int <: byte) +DisplayExpressions.dfy(42,6): Error: Method return value mismatch (expecting seq, got seq) (covariant type parameter would require int <: byte) DisplayExpressions.dfy(74,18): Error: arguments must have comparable types (got seq and seq) 7 resolution/type errors detected in DisplayExpressions.dfy diff --git a/Test/dafny0/ForLoops-Resolution.dfy.expect b/Test/dafny0/ForLoops-Resolution.dfy.expect index 76de5773c2e..dc94dac1f76 100644 --- a/Test/dafny0/ForLoops-Resolution.dfy.expect +++ b/Test/dafny0/ForLoops-Resolution.dfy.expect @@ -1,7 +1,7 @@ ForLoops-Resolution.dfy(6,18): Error: unresolved identifier: i ForLoops-Resolution.dfy(11,13): Error: unresolved identifier: i -ForLoops-Resolution.dfy(32,8): Error: RHS (of type Nat) not assignable to LHS (of type nat) -ForLoops-Resolution.dfy(38,8): Error: RHS (of type int) not assignable to LHS (of type Nat) +ForLoops-Resolution.dfy(32,8): Error: Method return value mismatch (expecting nat, got Nat) +ForLoops-Resolution.dfy(38,8): Error: Method return value mismatch (expecting Nat, got int) ForLoops-Resolution.dfy(78,4): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating (or you can add a 'decreases' clause to this 'for' loop if you want to prove that it does indeed terminate) ForLoops-Resolution.dfy(86,4): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating (or you can add a 'decreases' clause to this 'for' loop if you want to prove that it does indeed terminate) ForLoops-Resolution.dfy(95,16): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating diff --git a/Test/dafny0/NewtypesResolution.dfy.expect b/Test/dafny0/NewtypesResolution.dfy.expect index 82598394378..50526a3a060 100644 --- a/Test/dafny0/NewtypesResolution.dfy.expect +++ b/Test/dafny0/NewtypesResolution.dfy.expect @@ -15,8 +15,8 @@ NewtypesResolution.dfy(101,24): Error: Wrong number of type arguments (1 instead NewtypesResolution.dfy(105,10): Error: recursive constraint dependency involving a newtype: Cycle -> BadLemma -> Cycle NewtypesResolution.dfy(114,10): Error: recursive constraint dependency involving a newtype: SelfCycle -> SelfCycle NewtypesResolution.dfy(120,21): Error: name of type (N9) is used as a variable -NewtypesResolution.dfy(139,6): Error: RHS (of type int) not assignable to LHS (of type Int) -NewtypesResolution.dfy(140,6): Error: RHS (of type AnotherInt) not assignable to LHS (of type Int) +NewtypesResolution.dfy(139,6): Error: Method return value mismatch (expecting Int, got int) +NewtypesResolution.dfy(140,6): Error: Method return value mismatch (expecting Int, got AnotherInt) NewtypesResolution.dfy(156,9): Error: name of type (B) is used as a variable NewtypesResolution.dfy(157,11): Error: name of type (Syn) is used as a variable NewtypesResolution.dfy(162,8): Error: member 'U' does not exist in type synonym 'Y' diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 6151c7497a6..2f53b2b739e 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -73,8 +73,8 @@ ResolutionErrors.dfy(485,8): Error: when allocating an object of type 'Y', one o ResolutionErrors.dfy(490,8): Error: when allocating an object of type 'Luci', one of its constructor methods must be called ResolutionErrors.dfy(491,8): Error: when allocating an object of type 'Luci', one of its constructor methods must be called ResolutionErrors.dfy(493,15): Error: class Lamb does not have an anonymous constructor -ResolutionErrors.dfy(546,7): Error: RHS (of type List) not assignable to LHS (of type List) (covariant type parameter would require A <: B) -ResolutionErrors.dfy(551,7): Error: RHS (of type List) not assignable to LHS (of type List) (covariant type parameter would require A <: B) +ResolutionErrors.dfy(546,7): Error: Method return value mismatch (expecting List, got List) (covariant type parameter would require A <: B) +ResolutionErrors.dfy(551,7): Error: Method return value mismatch (expecting List, got List) (covariant type parameter would require A <: B) ResolutionErrors.dfy(565,17): Error: type of case bodies do not agree (found Tree<_T1, _T0>, previous types Tree<_T0, _T1>) (covariant type parameter 0 would require _T1 <: _T0) ResolutionErrors.dfy(577,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree ResolutionErrors.dfy(592,20): Error: unresolved identifier: w @@ -98,12 +98,12 @@ ResolutionErrors.dfy(762,22): Error: a possibly infinite loop is allowed only if ResolutionErrors.dfy(795,17): Error: wrong number of method result arguments (got 0, expected 1) ResolutionErrors.dfy(816,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. ResolutionErrors.dfy(827,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. -ResolutionErrors.dfy(850,6): Error: RHS (of type B) not assignable to LHS (of type object) -ResolutionErrors.dfy(852,6): Error: RHS (of type B) not assignable to LHS (of type object) -ResolutionErrors.dfy(857,6): Error: RHS (of type G) not assignable to LHS (of type object) -ResolutionErrors.dfy(858,6): Error: RHS (of type Dt) not assignable to LHS (of type object) -ResolutionErrors.dfy(859,6): Error: RHS (of type CoDt) not assignable to LHS (of type object) -ResolutionErrors.dfy(851,6): Error: RHS (of type int) not assignable to LHS (of type object) +ResolutionErrors.dfy(850,6): Error: Method return value mismatch (expecting object, got B) +ResolutionErrors.dfy(852,6): Error: Method return value mismatch (expecting object, got B) +ResolutionErrors.dfy(857,6): Error: Method return value mismatch (expecting object, got G) +ResolutionErrors.dfy(858,6): Error: Method return value mismatch (expecting object, got Dt) +ResolutionErrors.dfy(859,6): Error: Method return value mismatch (expecting object, got CoDt) +ResolutionErrors.dfy(851,6): Error: Method return value mismatch (expecting object, got int) ResolutionErrors.dfy(871,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int) ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) ResolutionErrors.dfy(887,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) @@ -150,10 +150,10 @@ ResolutionErrors.dfy(1089,21): Error: unresolved identifier: x ResolutionErrors.dfy(1092,21): Error: unresolved identifier: x ResolutionErrors.dfy(1099,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P ResolutionErrors.dfy(1111,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name or declare a module import 'opened'?) -ResolutionErrors.dfy(1121,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require bool = int) -ResolutionErrors.dfy(1126,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require B = A) -ResolutionErrors.dfy(1131,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require int = A) -ResolutionErrors.dfy(1132,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require A = int) +ResolutionErrors.dfy(1121,6): Error: Method return value mismatch (expecting P, got P) (non-variant type parameter would require bool = int) +ResolutionErrors.dfy(1126,6): Error: Method return value mismatch (expecting P, got P) (non-variant type parameter would require B = A) +ResolutionErrors.dfy(1131,6): Error: Method return value mismatch (expecting P, got P) (non-variant type parameter would require int = A) +ResolutionErrors.dfy(1132,6): Error: Method return value mismatch (expecting P, got P) (non-variant type parameter would require A = int) ResolutionErrors.dfy(1137,13): Error: arguments must have comparable types (got P and P) ResolutionErrors.dfy(1138,13): Error: arguments must have comparable types (got P and P) ResolutionErrors.dfy(1139,13): Error: arguments must have comparable types (got P and P) diff --git a/Test/dafny0/SubsetTypesERR.dfy.expect b/Test/dafny0/SubsetTypesERR.dfy.expect index 018a2024989..7ac154da498 100644 --- a/Test/dafny0/SubsetTypesERR.dfy.expect +++ b/Test/dafny0/SubsetTypesERR.dfy.expect @@ -1,11 +1,11 @@ SubsetTypesERR.dfy(11,8): Error: type array is not assignable to LHS (of type array) (nonvariance for type parameter expects Person? = Person) SubsetTypesERR.dfy(13,8): Error: type array is not assignable to LHS (of type array) (nonvariance for type parameter expects Person? = Person) SubsetTypesERR.dfy(15,8): Error: type array is not assignable to LHS (of type array) (nonvariance for type parameter expects Person? = Person) -SubsetTypesERR.dfy(17,8): Error: RHS (of type array) not assignable to LHS (of type array) (nonvariance for type parameter expects Person? = Person) +SubsetTypesERR.dfy(17,8): Error: Method return value mismatch (expecting array, got array) (nonvariance for type parameter expects Person? = Person) SubsetTypesERR.dfy(23,8): Error: type array is not assignable to LHS (of type array) (nonvariance for type parameter expects Person = Person?) SubsetTypesERR.dfy(25,8): Error: type array is not assignable to LHS (of type array) (nonvariance for type parameter expects Person = Person?) SubsetTypesERR.dfy(27,8): Error: type array is not assignable to LHS (of type array) (nonvariance for type parameter expects Person = Person?) -SubsetTypesERR.dfy(29,8): Error: RHS (of type array) not assignable to LHS (of type array) (nonvariance for type parameter expects Person = Person?) +SubsetTypesERR.dfy(29,8): Error: Method return value mismatch (expecting array, got array) (nonvariance for type parameter expects Person = Person?) SubsetTypesERR.dfy(37,8): Error: RHS (of type array) not assignable to LHS (of type array) (nonvariance for type parameter expects Person? = Person) SubsetTypesERR.dfy(39,8): Error: RHS (of type array) not assignable to LHS (of type array) (nonvariance for type parameter expects Person = Person?) SubsetTypesERR.dfy(42,8): Error: RHS (of type array) not assignable to LHS (of type array) (nonvariance for type parameter expects Person = Person?) diff --git a/Test/dafny0/TypeConstraints.dfy.expect b/Test/dafny0/TypeConstraints.dfy.expect index 80ff7af5206..168b98f6f94 100644 --- a/Test/dafny0/TypeConstraints.dfy.expect +++ b/Test/dafny0/TypeConstraints.dfy.expect @@ -1,17 +1,17 @@ -TypeConstraints.dfy(42,6): Error: RHS (of type int) not assignable to LHS (of type bool) -TypeConstraints.dfy(49,6): Error: RHS (of type int) not assignable to LHS (of type bool) +TypeConstraints.dfy(42,6): Error: Method return value mismatch (expecting bool, got int) +TypeConstraints.dfy(49,6): Error: Method return value mismatch (expecting bool, got int) TypeConstraints.dfy(56,9): Error: RHS (of type int) not assignable to LHS (of type bool) TypeConstraints.dfy(65,6): Error: RHS (of type bool) not assignable to LHS (of type int) -TypeConstraints.dfy(80,6): Error: RHS (of type MyInt) not assignable to LHS (of type int) -TypeConstraints.dfy(81,6): Error: RHS (of type int) not assignable to LHS (of type MyInt) -TypeConstraints.dfy(77,6): Error: RHS (of type int) not assignable to LHS (of type MyInt) +TypeConstraints.dfy(80,6): Error: Method return value mismatch (expecting int, got MyInt) +TypeConstraints.dfy(81,6): Error: Method return value mismatch (expecting MyInt, got int) +TypeConstraints.dfy(77,6): Error: Method return value mismatch (expecting MyInt, got int) TypeConstraints.dfy(94,8): Error: the type of this local variable is underspecified TypeConstraints.dfy(94,11): Error: the type of this local variable is underspecified TypeConstraints.dfy(102,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) TypeConstraints.dfy(136,16): 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) TypeConstraints.dfy(147,16): 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 C?) TypeConstraints.dfy(149,16): 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 C) -TypeConstraints.dfy(176,6): Error: RHS (of type C) not assignable to LHS (of type R) +TypeConstraints.dfy(176,6): Error: Method return value mismatch (expecting R, got C) TypeConstraints.dfy(424,8): Error: type array is not assignable to LHS (of type array) (nonvariance for type parameter expects int = nat) TypeConstraints.dfy(426,8): Error: type array is not assignable to LHS (of type array) (nonvariance for type parameter expects nat = int) TypeConstraints.dfy(429,8): Error: RHS (of type array) not assignable to LHS (of type array) (nonvariance for type parameter expects nat = int) diff --git a/Test/exports/ExportResolve.dfy.expect b/Test/exports/ExportResolve.dfy.expect index 1e2b88a8b13..1943980e692 100644 --- a/Test/exports/ExportResolve.dfy.expect +++ b/Test/exports/ExportResolve.dfy.expect @@ -97,12 +97,12 @@ ExportResolve.dfy(298,19): Error: member '_ctor' has not been imported in this s ExportResolve.dfy(342,15): Error: unresolved identifier: reveal_OpaqueFunction ExportResolve.dfy(342,29): Error: expression has no reveal lemma ExportResolve.dfy(414,15): Error: member 'Q' has not been imported in this scope and cannot be accessed here -ExportResolve.dfy(410,8): Error: RHS (of type C.X) not assignable to LHS (of type C.Z) -ExportResolve.dfy(411,8): Error: RHS (of type A.T) not assignable to LHS (of type C.Z) -ExportResolve.dfy(412,8): Error: RHS (of type int) not assignable to LHS (of type A.T) +ExportResolve.dfy(410,8): Error: Method return value mismatch (expecting C.Z, got C.X) +ExportResolve.dfy(411,8): Error: Method return value mismatch (expecting C.Z, got A.T) +ExportResolve.dfy(412,8): Error: Method return value mismatch (expecting A.T, got int) ExportResolve.dfy(436,15): Error: member 'Q' has not been imported in this scope and cannot be accessed here -ExportResolve.dfy(432,8): Error: RHS (of type C.X) not assignable to LHS (of type C.Z) -ExportResolve.dfy(433,8): Error: RHS (of type A.T) not assignable to LHS (of type C.Z) +ExportResolve.dfy(432,8): Error: Method return value mismatch (expecting C.Z, got C.X) +ExportResolve.dfy(433,8): Error: Method return value mismatch (expecting C.Z, got A.T) ExportResolve.dfy(457,15): Error: member 'Q' has not been imported in this scope and cannot be accessed here ExportResolve.dfy(473,15): Error: Cannot export mutable field 'u' without revealing its enclosing class 'C' ExportResolve.dfy(475,15): Error: Cannot export constructor 'FromInt' without revealing its enclosing class 'C' diff --git a/Test/git-issues/git-issue-3125.dfy b/Test/git-issues/git-issue-3125.dfy new file mode 100644 index 00000000000..3074c4800aa --- /dev/null +++ b/Test/git-issues/git-issue-3125.dfy @@ -0,0 +1,10 @@ +// RUN: %dafny_0 /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method Foo() returns (i: int) { + return "hello"; +} + +function foo(): int { + "hello" +} diff --git a/Test/git-issues/git-issue-3125.dfy.expect b/Test/git-issues/git-issue-3125.dfy.expect new file mode 100644 index 00000000000..394bf86dc45 --- /dev/null +++ b/Test/git-issues/git-issue-3125.dfy.expect @@ -0,0 +1,3 @@ +git-issue-3125.dfy(5,4): Error: Method return value mismatch (expecting int, got string) +git-issue-3125.dfy(8,9): Error: Function body type mismatch (expected int, got string) +2 resolution/type errors detected in git-issue-3125.dfy diff --git a/Test/traits/TraitPolymorphism.dfy.expect b/Test/traits/TraitPolymorphism.dfy.expect index 3db8f8a52ce..8eb368a96ce 100644 --- a/Test/traits/TraitPolymorphism.dfy.expect +++ b/Test/traits/TraitPolymorphism.dfy.expect @@ -1,3 +1,3 @@ TraitPolymorphism.dfy(56,10): Error: arguments must have comparable types (got C1 and T2) -TraitPolymorphism.dfy(58,6): Error: RHS (of type C1) not assignable to LHS (of type T2) +TraitPolymorphism.dfy(58,6): Error: Method return value mismatch (expecting T2, got C1) 2 resolution/type errors detected in TraitPolymorphism.dfy diff --git a/docs/dev/news/3125.fix b/docs/dev/news/3125.fix new file mode 100644 index 00000000000..82966fe19b0 --- /dev/null +++ b/docs/dev/news/3125.fix @@ -0,0 +1 @@ +Do not refer to an implicit assignment in error messages on return statements From 59991658c64ea9348b2fed19e2505a773e02ef16 Mon Sep 17 00:00:00 2001 From: Nathan Taylor Date: Wed, 30 Nov 2022 14:12:30 -0600 Subject: [PATCH 2/4] Distingush between implicit identifiers and non --- .../DafnyCore/AST/Expressions/Expressions.cs | 18 +++++++++++++ Source/DafnyCore/Resolver/Resolver.cs | 16 +++--------- Test/dafny0/BitvectorResolution.dfy | 4 +-- Test/dafny0/BitvectorResolution.dfy.expect | 8 +++--- Test/dafny0/ByMethodResolution.dfy.expect | 2 +- Test/dafny0/ConstantErrors.dfy.expect | 2 +- Test/dafny0/DisplayExpressions.dfy.expect | 2 +- Test/dafny0/ForLoops-Resolution.dfy.expect | 4 +-- Test/dafny0/NewtypesResolution.dfy.expect | 4 +-- Test/dafny0/ResolutionErrors.dfy.expect | 26 ++++++++++--------- Test/dafny0/SubsetTypesERR.dfy.expect | 4 +-- Test/dafny0/TypeConstraints.dfy.expect | 12 ++++----- Test/exports/ExportResolve.dfy.expect | 10 +++---- Test/git-issues/git-issue-3125.dfy | 3 ++- Test/git-issues/git-issue-3125.dfy.expect | 7 ++--- Test/traits/TraitPolymorphism.dfy.expect | 2 +- 16 files changed, 68 insertions(+), 56 deletions(-) diff --git a/Source/DafnyCore/AST/Expressions/Expressions.cs b/Source/DafnyCore/AST/Expressions/Expressions.cs index c5fdcfd36f6..a44c1ad6b22 100644 --- a/Source/DafnyCore/AST/Expressions/Expressions.cs +++ b/Source/DafnyCore/AST/Expressions/Expressions.cs @@ -1078,6 +1078,24 @@ public IEnumerable GetResolvedDeclarations() { public IToken NameToken => tok; } +/// +/// An implicit identifier is used in the context of a ReturnStmt tacetly +/// assigning a value to a Method's out parameter. +/// +public class ImplicitIdentifierExpr : IdentifierExpr { + public ImplicitIdentifierExpr(IToken tok, string name) + : base(tok, name) { } + + /// + /// Constructs a resolved implicit identifier. + /// + public ImplicitIdentifierExpr(IToken tok, IVariable v) + : base(tok, v) { } + + public override bool IsImplicit => true; +} + + /// /// If an "AutoGhostIdentifierExpr" is used as the out-parameter of a ghost method or /// a method with a ghost parameter, resolution will change the .Var's .IsGhost to true diff --git a/Source/DafnyCore/Resolver/Resolver.cs b/Source/DafnyCore/Resolver/Resolver.cs index 3cdad94d608..3d66cf7d506 100644 --- a/Source/DafnyCore/Resolver/Resolver.cs +++ b/Source/DafnyCore/Resolver/Resolver.cs @@ -9557,7 +9557,7 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext foreach (Formal f in cmc.Outs) { Expression produceLhs; if (stmt is ReturnStmt) { - var ident = new IdentifierExpr(f.tok, f.Name); + var ident = new ImplicitIdentifierExpr(f.tok, f.Name); // resolve it here to avoid capture into more closely declared local variables ident.Var = f; ident.Type = ident.Var.Type; @@ -9743,18 +9743,8 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext ResolveExpression(rr.Expr, resolutionContext); Contract.Assert(rr.Expr.Type != null); // follows from postcondition of ResolveExpression - bool isHiddenUpdateToOutVar = false; - if (s.Lhs is IdentifierExpr) { - IdentifierExpr ie = (IdentifierExpr)s.Lhs; - if (ie.Var is Formal) { - Formal f = ((Formal)ie.Var); - if (!f.InParam) { - isHiddenUpdateToOutVar = true; - } - } - } - if (isHiddenUpdateToOutVar) { - AddAssignableConstraint(stmt.Tok, lhsType, rr.Expr.Type, "Method return value mismatch (expecting {0}, got {1})"); + if (s.Lhs is ImplicitIdentifierExpr { Var: Formal { InParam: false } }) { + AddAssignableConstraint(stmt.Tok, lhsType, rr.Expr.Type, "Method return value mismatch (expected {0}, got {1})"); } else { AddAssignableConstraint(stmt.Tok, lhsType, rr.Expr.Type, "RHS (of type {1}) not assignable to LHS (of type {0})"); } diff --git a/Test/dafny0/BitvectorResolution.dfy b/Test/dafny0/BitvectorResolution.dfy index fb2a6df1b2a..4b7c54519ef 100644 --- a/Test/dafny0/BitvectorResolution.dfy +++ b/Test/dafny0/BitvectorResolution.dfy @@ -35,8 +35,8 @@ module OrdinaryTypeChecking { x := b67 << 3; // error: result not assignable to an int x := b67 << 3 as int; // error: ditto (the "as" applies only to the "3") x := (b67 << 3) as int; - x := b67.RotateLeft(3); - x := b67.RotateRight(3); + x := b67.RotateLeft(3); // error: bitwise rotations produce bitvectors + x := b67.RotateRight(3); // error: ditto b67 := b67 << r; // error: cannot shift by a real b67 := b67 << small; // error: cannot shift by a real b67 := b67.RotateLeft(r); diff --git a/Test/dafny0/BitvectorResolution.dfy.expect b/Test/dafny0/BitvectorResolution.dfy.expect index 1bfc561e691..2b3b55d42be 100644 --- a/Test/dafny0/BitvectorResolution.dfy.expect +++ b/Test/dafny0/BitvectorResolution.dfy.expect @@ -2,10 +2,10 @@ BitvectorResolution.dfy(9,13): Error: literal (5000) is too large for the bitvec BitvectorResolution.dfy(15,9): Error: literal (1) is too large for the bitvector type bv0 BitvectorResolution.dfy(18,9): Error: literal (4294967296) is too large for the bitvector type bv32 BitvectorResolution.dfy(24,12): Error: literal (1) is too large for the bitvector type bv0 -BitvectorResolution.dfy(35,6): Error: Method return value mismatch (expecting int, got bv67) -BitvectorResolution.dfy(36,6): Error: Method return value mismatch (expecting int, got bv67) -BitvectorResolution.dfy(38,6): Error: Method return value mismatch (expecting int, got bv67) -BitvectorResolution.dfy(39,6): Error: Method return value mismatch (expecting int, got bv67) +BitvectorResolution.dfy(35,6): Error: RHS (of type bv67) not assignable to LHS (of type int) +BitvectorResolution.dfy(36,6): Error: RHS (of type bv67) not assignable to LHS (of type int) +BitvectorResolution.dfy(38,6): Error: RHS (of type bv67) not assignable to LHS (of type int) +BitvectorResolution.dfy(39,6): Error: RHS (of type bv67) not assignable to LHS (of type int) BitvectorResolution.dfy(40,15): Error: type of right argument to << (real) must be an integer-numeric or bitvector type BitvectorResolution.dfy(41,15): Error: type of right argument to << (SmallReal) must be an integer-numeric or bitvector type BitvectorResolution.dfy(42,25): Error: incorrect argument type for function parameter 'w' (expected nat, found real) diff --git a/Test/dafny0/ByMethodResolution.dfy.expect b/Test/dafny0/ByMethodResolution.dfy.expect index aad4bd0a434..b35506ebc42 100644 --- a/Test/dafny0/ByMethodResolution.dfy.expect +++ b/Test/dafny0/ByMethodResolution.dfy.expect @@ -1,6 +1,6 @@ ByMethodResolution.dfy(17,6): Error: number of return parameters does not match declaration (found 2, expected 1) ByMethodResolution.dfy(25,4): Error: Method return value mismatch (expecting real, got bv9) -ByMethodResolution.dfy(24,6): Error: Method return value mismatch (expecting real, got int) +ByMethodResolution.dfy(24,6): Error: RHS (of type int) not assignable to LHS (of type real) ByMethodResolution.dfy(63,13): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function with 'function method') ByMethodResolution.dfy(64,13): Error: a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') ByMethodResolution.dfy(65,13): Error: a call to a twostate function is allowed only in specification contexts diff --git a/Test/dafny0/ConstantErrors.dfy.expect b/Test/dafny0/ConstantErrors.dfy.expect index 26596c65606..822a2a41c35 100644 --- a/Test/dafny0/ConstantErrors.dfy.expect +++ b/Test/dafny0/ConstantErrors.dfy.expect @@ -3,7 +3,7 @@ ConstantErrors.dfy(12,8): Error: const definition contains a cycle: five -> six ConstantErrors.dfy(21,6): Error: 'this' is not allowed in a 'static' context ConstantErrors.dfy(32,6): Error: a ghost const field is allowed only in specification contexts ConstantErrors.dfy(33,6): Error: a ghost const field is allowed only in specification contexts -ConstantErrors.dfy(44,7): Error: Method return value mismatch (expecting SmallInt, got int) +ConstantErrors.dfy(44,7): Error: RHS (of type int) not assignable to LHS (of type SmallInt) ConstantErrors.dfy(67,10): Error: const field 'x0' is inherited from trait 'Trait' and is not allowed to be re-declared ConstantErrors.dfy(68,10): Error: const field 'x1' is inherited from trait 'Trait' and is not allowed to be re-declared ConstantErrors.dfy(69,10): Error: const field 'x2' is inherited from trait 'Trait' and is not allowed to be re-declared diff --git a/Test/dafny0/DisplayExpressions.dfy.expect b/Test/dafny0/DisplayExpressions.dfy.expect index 1c24392274c..d2714fa8123 100644 --- a/Test/dafny0/DisplayExpressions.dfy.expect +++ b/Test/dafny0/DisplayExpressions.dfy.expect @@ -3,6 +3,6 @@ DisplayExpressions.dfy(12,8): Error: the type of this variable is underspecified DisplayExpressions.dfy(17,8): Error: the type of this variable is underspecified DisplayExpressions.dfy(22,8): Error: the type of this variable is underspecified DisplayExpressions.dfy(27,14): Error: the type of this expression is underspecified -DisplayExpressions.dfy(42,6): Error: Method return value mismatch (expecting seq, got seq) (covariant type parameter would require int <: byte) +DisplayExpressions.dfy(42,6): Error: RHS (of type seq) not assignable to LHS (of type seq) (covariant type parameter would require int <: byte) DisplayExpressions.dfy(74,18): Error: arguments must have comparable types (got seq and seq) 7 resolution/type errors detected in DisplayExpressions.dfy diff --git a/Test/dafny0/ForLoops-Resolution.dfy.expect b/Test/dafny0/ForLoops-Resolution.dfy.expect index dc94dac1f76..76de5773c2e 100644 --- a/Test/dafny0/ForLoops-Resolution.dfy.expect +++ b/Test/dafny0/ForLoops-Resolution.dfy.expect @@ -1,7 +1,7 @@ ForLoops-Resolution.dfy(6,18): Error: unresolved identifier: i ForLoops-Resolution.dfy(11,13): Error: unresolved identifier: i -ForLoops-Resolution.dfy(32,8): Error: Method return value mismatch (expecting nat, got Nat) -ForLoops-Resolution.dfy(38,8): Error: Method return value mismatch (expecting Nat, got int) +ForLoops-Resolution.dfy(32,8): Error: RHS (of type Nat) not assignable to LHS (of type nat) +ForLoops-Resolution.dfy(38,8): Error: RHS (of type int) not assignable to LHS (of type Nat) ForLoops-Resolution.dfy(78,4): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating (or you can add a 'decreases' clause to this 'for' loop if you want to prove that it does indeed terminate) ForLoops-Resolution.dfy(86,4): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating (or you can add a 'decreases' clause to this 'for' loop if you want to prove that it does indeed terminate) ForLoops-Resolution.dfy(95,16): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating diff --git a/Test/dafny0/NewtypesResolution.dfy.expect b/Test/dafny0/NewtypesResolution.dfy.expect index 50526a3a060..82598394378 100644 --- a/Test/dafny0/NewtypesResolution.dfy.expect +++ b/Test/dafny0/NewtypesResolution.dfy.expect @@ -15,8 +15,8 @@ NewtypesResolution.dfy(101,24): Error: Wrong number of type arguments (1 instead NewtypesResolution.dfy(105,10): Error: recursive constraint dependency involving a newtype: Cycle -> BadLemma -> Cycle NewtypesResolution.dfy(114,10): Error: recursive constraint dependency involving a newtype: SelfCycle -> SelfCycle NewtypesResolution.dfy(120,21): Error: name of type (N9) is used as a variable -NewtypesResolution.dfy(139,6): Error: Method return value mismatch (expecting Int, got int) -NewtypesResolution.dfy(140,6): Error: Method return value mismatch (expecting Int, got AnotherInt) +NewtypesResolution.dfy(139,6): Error: RHS (of type int) not assignable to LHS (of type Int) +NewtypesResolution.dfy(140,6): Error: RHS (of type AnotherInt) not assignable to LHS (of type Int) NewtypesResolution.dfy(156,9): Error: name of type (B) is used as a variable NewtypesResolution.dfy(157,11): Error: name of type (Syn) is used as a variable NewtypesResolution.dfy(162,8): Error: member 'U' does not exist in type synonym 'Y' diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 2f53b2b739e..e0942ac9e59 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -73,8 +73,10 @@ ResolutionErrors.dfy(485,8): Error: when allocating an object of type 'Y', one o ResolutionErrors.dfy(490,8): Error: when allocating an object of type 'Luci', one of its constructor methods must be called ResolutionErrors.dfy(491,8): Error: when allocating an object of type 'Luci', one of its constructor methods must be called ResolutionErrors.dfy(493,15): Error: class Lamb does not have an anonymous constructor -ResolutionErrors.dfy(546,7): Error: Method return value mismatch (expecting List, got List) (covariant type parameter would require A <: B) -ResolutionErrors.dfy(551,7): Error: Method return value mismatch (expecting List, got List) (covariant type parameter would require A <: B) +ResolutionErrors.dfy(546,7): Error: RHS (of type List) not assignable to LHS (of type List) (covariant type parameter would require A <: B) +ResolutionErrors.dfy(551,7): Error: RHS (of type List) not assignable to LHS (of type List) (covariant type parameter would require A <: B) +ResolutionErrors.dfy(551,7): Error: RHS (of type List) not assignable to LHS (of type List) (covar +iant type parameter would require A <: B) ResolutionErrors.dfy(565,17): Error: type of case bodies do not agree (found Tree<_T1, _T0>, previous types Tree<_T0, _T1>) (covariant type parameter 0 would require _T1 <: _T0) ResolutionErrors.dfy(577,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree ResolutionErrors.dfy(592,20): Error: unresolved identifier: w @@ -98,12 +100,12 @@ ResolutionErrors.dfy(762,22): Error: a possibly infinite loop is allowed only if ResolutionErrors.dfy(795,17): Error: wrong number of method result arguments (got 0, expected 1) ResolutionErrors.dfy(816,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. ResolutionErrors.dfy(827,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. -ResolutionErrors.dfy(850,6): Error: Method return value mismatch (expecting object, got B) -ResolutionErrors.dfy(852,6): Error: Method return value mismatch (expecting object, got B) -ResolutionErrors.dfy(857,6): Error: Method return value mismatch (expecting object, got G) -ResolutionErrors.dfy(858,6): Error: Method return value mismatch (expecting object, got Dt) -ResolutionErrors.dfy(859,6): Error: Method return value mismatch (expecting object, got CoDt) -ResolutionErrors.dfy(851,6): Error: Method return value mismatch (expecting object, got int) +ResolutionErrors.dfy(850,6): Error: RHS (of type B) not assignable to LHS (of type object) +ResolutionErrors.dfy(852,6): Error: RHS (of type B) not assignable to LHS (of type object) +ResolutionErrors.dfy(857,6): Error: RHS (of type G) not assignable to LHS (of type object) +ResolutionErrors.dfy(858,6): Error: RHS (of type Dt) not assignable to LHS (of type object) +ResolutionErrors.dfy(859,6): Error: RHS (of type CoDt) not assignable to LHS (of type object) +ResolutionErrors.dfy(851,6): Error: RHS (of type int) not assignable to LHS (of type object) ResolutionErrors.dfy(871,13): Error: a modifies-clause expression must denote an object or a set/iset/multiset/seq of objects (instead got int) ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) ResolutionErrors.dfy(887,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) @@ -150,10 +152,10 @@ ResolutionErrors.dfy(1089,21): Error: unresolved identifier: x ResolutionErrors.dfy(1092,21): Error: unresolved identifier: x ResolutionErrors.dfy(1099,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P ResolutionErrors.dfy(1111,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name or declare a module import 'opened'?) -ResolutionErrors.dfy(1121,6): Error: Method return value mismatch (expecting P, got P) (non-variant type parameter would require bool = int) -ResolutionErrors.dfy(1126,6): Error: Method return value mismatch (expecting P, got P) (non-variant type parameter would require B = A) -ResolutionErrors.dfy(1131,6): Error: Method return value mismatch (expecting P, got P) (non-variant type parameter would require int = A) -ResolutionErrors.dfy(1132,6): Error: Method return value mismatch (expecting P, got P) (non-variant type parameter would require A = int) +ResolutionErrors.dfy(1121,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require bool = int) +ResolutionErrors.dfy(1126,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require B = A) +ResolutionErrors.dfy(1131,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require int = A) +ResolutionErrors.dfy(1132,6): Error: RHS (of type P) not assignable to LHS (of type P) (non-variant type parameter would require A = int) ResolutionErrors.dfy(1137,13): Error: arguments must have comparable types (got P and P) ResolutionErrors.dfy(1138,13): Error: arguments must have comparable types (got P and P) ResolutionErrors.dfy(1139,13): Error: arguments must have comparable types (got P and P) diff --git a/Test/dafny0/SubsetTypesERR.dfy.expect b/Test/dafny0/SubsetTypesERR.dfy.expect index 7ac154da498..018a2024989 100644 --- a/Test/dafny0/SubsetTypesERR.dfy.expect +++ b/Test/dafny0/SubsetTypesERR.dfy.expect @@ -1,11 +1,11 @@ SubsetTypesERR.dfy(11,8): Error: type array is not assignable to LHS (of type array) (nonvariance for type parameter expects Person? = Person) SubsetTypesERR.dfy(13,8): Error: type array is not assignable to LHS (of type array) (nonvariance for type parameter expects Person? = Person) SubsetTypesERR.dfy(15,8): Error: type array is not assignable to LHS (of type array) (nonvariance for type parameter expects Person? = Person) -SubsetTypesERR.dfy(17,8): Error: Method return value mismatch (expecting array, got array) (nonvariance for type parameter expects Person? = Person) +SubsetTypesERR.dfy(17,8): Error: RHS (of type array) not assignable to LHS (of type array) (nonvariance for type parameter expects Person? = Person) SubsetTypesERR.dfy(23,8): Error: type array is not assignable to LHS (of type array) (nonvariance for type parameter expects Person = Person?) SubsetTypesERR.dfy(25,8): Error: type array is not assignable to LHS (of type array) (nonvariance for type parameter expects Person = Person?) SubsetTypesERR.dfy(27,8): Error: type array is not assignable to LHS (of type array) (nonvariance for type parameter expects Person = Person?) -SubsetTypesERR.dfy(29,8): Error: Method return value mismatch (expecting array, got array) (nonvariance for type parameter expects Person = Person?) +SubsetTypesERR.dfy(29,8): Error: RHS (of type array) not assignable to LHS (of type array) (nonvariance for type parameter expects Person = Person?) SubsetTypesERR.dfy(37,8): Error: RHS (of type array) not assignable to LHS (of type array) (nonvariance for type parameter expects Person? = Person) SubsetTypesERR.dfy(39,8): Error: RHS (of type array) not assignable to LHS (of type array) (nonvariance for type parameter expects Person = Person?) SubsetTypesERR.dfy(42,8): Error: RHS (of type array) not assignable to LHS (of type array) (nonvariance for type parameter expects Person = Person?) diff --git a/Test/dafny0/TypeConstraints.dfy.expect b/Test/dafny0/TypeConstraints.dfy.expect index 168b98f6f94..80ff7af5206 100644 --- a/Test/dafny0/TypeConstraints.dfy.expect +++ b/Test/dafny0/TypeConstraints.dfy.expect @@ -1,17 +1,17 @@ -TypeConstraints.dfy(42,6): Error: Method return value mismatch (expecting bool, got int) -TypeConstraints.dfy(49,6): Error: Method return value mismatch (expecting bool, got int) +TypeConstraints.dfy(42,6): Error: RHS (of type int) not assignable to LHS (of type bool) +TypeConstraints.dfy(49,6): Error: RHS (of type int) not assignable to LHS (of type bool) TypeConstraints.dfy(56,9): Error: RHS (of type int) not assignable to LHS (of type bool) TypeConstraints.dfy(65,6): Error: RHS (of type bool) not assignable to LHS (of type int) -TypeConstraints.dfy(80,6): Error: Method return value mismatch (expecting int, got MyInt) -TypeConstraints.dfy(81,6): Error: Method return value mismatch (expecting MyInt, got int) -TypeConstraints.dfy(77,6): Error: Method return value mismatch (expecting MyInt, got int) +TypeConstraints.dfy(80,6): Error: RHS (of type MyInt) not assignable to LHS (of type int) +TypeConstraints.dfy(81,6): Error: RHS (of type int) not assignable to LHS (of type MyInt) +TypeConstraints.dfy(77,6): Error: RHS (of type int) not assignable to LHS (of type MyInt) TypeConstraints.dfy(94,8): Error: the type of this local variable is underspecified TypeConstraints.dfy(94,11): Error: the type of this local variable is underspecified TypeConstraints.dfy(102,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) TypeConstraints.dfy(136,16): 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) TypeConstraints.dfy(147,16): 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 C?) TypeConstraints.dfy(149,16): 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 C) -TypeConstraints.dfy(176,6): Error: Method return value mismatch (expecting R, got C) +TypeConstraints.dfy(176,6): Error: RHS (of type C) not assignable to LHS (of type R) TypeConstraints.dfy(424,8): Error: type array is not assignable to LHS (of type array) (nonvariance for type parameter expects int = nat) TypeConstraints.dfy(426,8): Error: type array is not assignable to LHS (of type array) (nonvariance for type parameter expects nat = int) TypeConstraints.dfy(429,8): Error: RHS (of type array) not assignable to LHS (of type array) (nonvariance for type parameter expects nat = int) diff --git a/Test/exports/ExportResolve.dfy.expect b/Test/exports/ExportResolve.dfy.expect index 1943980e692..1e2b88a8b13 100644 --- a/Test/exports/ExportResolve.dfy.expect +++ b/Test/exports/ExportResolve.dfy.expect @@ -97,12 +97,12 @@ ExportResolve.dfy(298,19): Error: member '_ctor' has not been imported in this s ExportResolve.dfy(342,15): Error: unresolved identifier: reveal_OpaqueFunction ExportResolve.dfy(342,29): Error: expression has no reveal lemma ExportResolve.dfy(414,15): Error: member 'Q' has not been imported in this scope and cannot be accessed here -ExportResolve.dfy(410,8): Error: Method return value mismatch (expecting C.Z, got C.X) -ExportResolve.dfy(411,8): Error: Method return value mismatch (expecting C.Z, got A.T) -ExportResolve.dfy(412,8): Error: Method return value mismatch (expecting A.T, got int) +ExportResolve.dfy(410,8): Error: RHS (of type C.X) not assignable to LHS (of type C.Z) +ExportResolve.dfy(411,8): Error: RHS (of type A.T) not assignable to LHS (of type C.Z) +ExportResolve.dfy(412,8): Error: RHS (of type int) not assignable to LHS (of type A.T) ExportResolve.dfy(436,15): Error: member 'Q' has not been imported in this scope and cannot be accessed here -ExportResolve.dfy(432,8): Error: Method return value mismatch (expecting C.Z, got C.X) -ExportResolve.dfy(433,8): Error: Method return value mismatch (expecting C.Z, got A.T) +ExportResolve.dfy(432,8): Error: RHS (of type C.X) not assignable to LHS (of type C.Z) +ExportResolve.dfy(433,8): Error: RHS (of type A.T) not assignable to LHS (of type C.Z) ExportResolve.dfy(457,15): Error: member 'Q' has not been imported in this scope and cannot be accessed here ExportResolve.dfy(473,15): Error: Cannot export mutable field 'u' without revealing its enclosing class 'C' ExportResolve.dfy(475,15): Error: Cannot export constructor 'FromInt' without revealing its enclosing class 'C' diff --git a/Test/git-issues/git-issue-3125.dfy b/Test/git-issues/git-issue-3125.dfy index 3074c4800aa..9559c149b83 100644 --- a/Test/git-issues/git-issue-3125.dfy +++ b/Test/git-issues/git-issue-3125.dfy @@ -2,7 +2,8 @@ // RUN: %diff "%s.expect" "%t" method Foo() returns (i: int) { - return "hello"; + i := "explicit assignment"; + return "implicit assignment"; } function foo(): int { diff --git a/Test/git-issues/git-issue-3125.dfy.expect b/Test/git-issues/git-issue-3125.dfy.expect index 394bf86dc45..38c66257083 100644 --- a/Test/git-issues/git-issue-3125.dfy.expect +++ b/Test/git-issues/git-issue-3125.dfy.expect @@ -1,3 +1,4 @@ -git-issue-3125.dfy(5,4): Error: Method return value mismatch (expecting int, got string) -git-issue-3125.dfy(8,9): Error: Function body type mismatch (expected int, got string) -2 resolution/type errors detected in git-issue-3125.dfy +git-issue-3125.dfy(5,6): Error: RHS (of type string) not assignable to LHS (of type int) +git-issue-3125.dfy(6,4): Error: Method return value mismatch (expected int, got string) +git-issue-3125.dfy(9,9): Error: Function body type mismatch (expected int, got string) +3 resolution/type errors detected in git-issue-3125.dfy diff --git a/Test/traits/TraitPolymorphism.dfy.expect b/Test/traits/TraitPolymorphism.dfy.expect index 8eb368a96ce..3db8f8a52ce 100644 --- a/Test/traits/TraitPolymorphism.dfy.expect +++ b/Test/traits/TraitPolymorphism.dfy.expect @@ -1,3 +1,3 @@ TraitPolymorphism.dfy(56,10): Error: arguments must have comparable types (got C1 and T2) -TraitPolymorphism.dfy(58,6): Error: Method return value mismatch (expecting T2, got C1) +TraitPolymorphism.dfy(58,6): Error: RHS (of type C1) not assignable to LHS (of type T2) 2 resolution/type errors detected in TraitPolymorphism.dfy From c9a32a2f4dbeb3900a0d7dda90f4eed9b209eee8 Mon Sep 17 00:00:00 2001 From: Nathan Taylor Date: Wed, 30 Nov 2022 14:18:55 -0600 Subject: [PATCH 3/4] typo in test --- Test/dafny0/ByMethodResolution.dfy.expect | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/dafny0/ByMethodResolution.dfy.expect b/Test/dafny0/ByMethodResolution.dfy.expect index b35506ebc42..d16ded5e66d 100644 --- a/Test/dafny0/ByMethodResolution.dfy.expect +++ b/Test/dafny0/ByMethodResolution.dfy.expect @@ -1,5 +1,5 @@ ByMethodResolution.dfy(17,6): Error: number of return parameters does not match declaration (found 2, expected 1) -ByMethodResolution.dfy(25,4): Error: Method return value mismatch (expecting real, got bv9) +ByMethodResolution.dfy(25,4): Error: Method return value mismatch (expected real, got bv9) ByMethodResolution.dfy(24,6): Error: RHS (of type int) not assignable to LHS (of type real) ByMethodResolution.dfy(63,13): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function with 'function method') ByMethodResolution.dfy(64,13): Error: a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method') From 5b9536a0c9752fc85f7dd1612a38445d93d639e4 Mon Sep 17 00:00:00 2001 From: Nathan Taylor Date: Wed, 30 Nov 2022 16:49:59 -0600 Subject: [PATCH 4/4] typo in test --- Test/dafny0/ResolutionErrors.dfy.expect | 2 -- 1 file changed, 2 deletions(-) diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index e0942ac9e59..6151c7497a6 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -75,8 +75,6 @@ ResolutionErrors.dfy(491,8): Error: when allocating an object of type 'Luci', on ResolutionErrors.dfy(493,15): Error: class Lamb does not have an anonymous constructor ResolutionErrors.dfy(546,7): Error: RHS (of type List) not assignable to LHS (of type List) (covariant type parameter would require A <: B) ResolutionErrors.dfy(551,7): Error: RHS (of type List) not assignable to LHS (of type List) (covariant type parameter would require A <: B) -ResolutionErrors.dfy(551,7): Error: RHS (of type List) not assignable to LHS (of type List) (covar -iant type parameter would require A <: B) ResolutionErrors.dfy(565,17): Error: type of case bodies do not agree (found Tree<_T1, _T0>, previous types Tree<_T0, _T1>) (covariant type parameter 0 would require _T1 <: _T0) ResolutionErrors.dfy(577,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree ResolutionErrors.dfy(592,20): Error: unresolved identifier: w