Fixed an issue

dafny-lang · Feb 11, 2025 · c044738 · c044738
1 parent d928f2f
commit c044738
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 1 deletion.
diff --git 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
@@ -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<Dafny.ISequence<Dafny.Rune>>.Union(readIdents, _11_recIdents);
           }
           r = ((((_7_fullPath).ApplyType(_8_onTypeExprs)).FSel(Defs.__default.escapeName((name).dtor_name))).ApplyType(_2_typeExprs)).Apply(Dafny.Sequence<RAST._IExpr>.Concat(Dafny.Sequence<RAST._IExpr>.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
@@ -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
@@ -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