diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy index c5b5462dff..35db636895 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy @@ -2183,6 +2183,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { } else { // The self type of any other type is borrowed onExpr, recOwnership, recIdents := GenExpr(on, selfIdent, env, OwnershipBorrowed); + onExpr := FromGeneralBorrowToSelfBorrow(onExpr, recOwnership, env); readIdents := readIdents + recIdents; } r := fullPath.ApplyType(onTypeExprs).FSel(escapeName(name.name)).ApplyType(typeExprs).Apply([onExpr] + argExprs); diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs index 7dd608c077..2211a97cc8 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs @@ -2541,6 +2541,7 @@ public void GenCall(DAST._IExpression @on, Defs._ISelfInfo selfIdent, DAST._ICal _9_onExpr = _out15; _10_recOwnership = _out16; _11_recIdents = _out17; + _9_onExpr = (this).FromGeneralBorrowToSelfBorrow(_9_onExpr, _10_recOwnership, env); readIdents = Dafny.Set>.Union(readIdents, _11_recIdents); } r = ((((_7_fullPath).ApplyType(_8_onTypeExprs)).FSel(Defs.__default.escapeName((name).dtor_name))).ApplyType(_2_typeExprs)).Apply(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(_9_onExpr), _0_argExprs)); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/datatypes-scoping.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/datatypes-scoping.dfy index 13ef7682d6..a4abdb8d3b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/datatypes-scoping.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/datatypes-scoping.dfy @@ -12,6 +12,10 @@ datatype Loop2 = Loop2(loop: Loop) { method hash() { print "\nThis is Dafny hash 2"; } + + method doHash() { + hash(); + } } method Main() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/datatypes-scoping.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/datatypes-scoping.dfy.expect index d2b9c22168..9f527b4486 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/datatypes-scoping.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/datatypes-scoping.dfy.expect @@ -1,4 +1,4 @@ -Dafny program verifier finished with 1 verified, 0 errors +Dafny program verifier finished with 2 verified, 0 errors This is Dafny Hash This is Dafny hash 2 \ No newline at end of file