Fixed

dafny-lang · Sep 30, 2024 · 4cf2984 · 4cf2984
1 parent 88b0656
commit 4cf2984
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 7 deletions.
diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
@@ -48,7 +48,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
     const update_field_if_uninit_macro :=
       if pointerType.Raw? then "update_field_if_uninit!" else "update_field_if_uninit_object!"
     const update_field_mut_if_uninit_macro :=
-      if pointerType.Raw? then "update_field_mut_if_uninit!" else "update_fiel_mutd_if_uninit_object!"
+      if pointerType.Raw? then "update_field_mut_if_uninit!" else "update_field_mut_if_uninit_object!"
     const Upcast :=
       if pointerType.Raw? then "Upcast" else "UpcastObject"
     const UpcastFnMacro :=

diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs
@@ -6791,7 +6791,7 @@ public Dafny.ISequence<Dafny.Rune> update__field__mut__if__uninit__macro { get {
       if (((this).pointerType).is_Raw) {
         return Dafny.Sequence<Dafny.Rune>.UnicodeFromString("update_field_mut_if_uninit!");
       } else {
-        return Dafny.Sequence<Dafny.Rune>.UnicodeFromString("update_fiel_mutd_if_uninit_object!");
+        return Dafny.Sequence<Dafny.Rune>.UnicodeFromString("update_field_mut_if_uninit_object!");
       }
     } }
     public Dafny.ISequence<Dafny.Rune> Upcast { get {

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/avoid_soundness_mut.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/avoid_soundness_mut.dfy
@@ -1,7 +1,7 @@
 // RUN: %baredafny build -t:rs "%s"
 // RUN: "%S/avoid_soundness_mut-rust/cargo" run --release > "%t"
 // RUN: %diff "%s.expect" "%t"
-// RUN: %baredafny built -t:rs --raw-pointers "%s"
+// RUN: %baredafny build -t:rs --raw-pointers "%s"
 // RUN: "%S/avoid_soundness_mut-rust/cargo" run --release > "%t"
 // RUN: %diff "%s.expect" "%t"
 

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/externalclasses.rs b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/externalclasses.rs
@@ -83,7 +83,7 @@ pub mod DafnyLibraries {
 
 pub mod ExternModuleWithOneClassToImport {
   pub struct NonShareableBox {
-    s: ::dafny_runtime::DafnyString
+    s: ::dafny_runtime::Field<::dafny_runtime::DafnyString>
   }
   impl NonShareableBox {
     pub fn _allocate_object() -> ::dafny_runtime::Object<Self> {
@@ -98,10 +98,10 @@ pub mod ExternModuleWithOneClassToImport {
   impl crate::ExternModuleWithOneClassToImport::TraitDefinedInModule
     for NonShareableBox {
     fn Get(&self) -> ::dafny_runtime::DafnyString {
-      self.s.clone()
+      ::dafny_runtime::read_field(self.s)
     }
-    fn Put(&mut self, c: &::dafny_runtime::DafnyString) {
-      self.s = c.clone();
+    fn Put(&self, c: &::dafny_runtime::DafnyString) {
+      ::dafny_runtime::modify_field(self.s, c.clone());
     }
   }
 }