diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/src/dafny_libraries.rs b/AwsCryptographicMaterialProviders/runtimes/rust/src/dafny_libraries.rs index de16d5af7..a5e7f437f 100644 --- a/AwsCryptographicMaterialProviders/runtimes/rust/src/dafny_libraries.rs +++ b/AwsCryptographicMaterialProviders/runtimes/rust/src/dafny_libraries.rs @@ -71,6 +71,12 @@ pub mod DafnyLibraries { } } + impl + ::dafny_runtime::UpcastObject for MutableMap + { + ::dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any); + } + pub mod FileIO { use std::fs::File; use std::io::Read; @@ -89,7 +95,12 @@ pub mod DafnyLibraries { let mut file = match File::open(path) { Err(why) => { - let err_msg = format!("couldn't open {} for reading from {}: {}", path.display(), curr_dir(), why); + let err_msg = format!( + "couldn't open {} for reading from {}: {}", + path.display(), + curr_dir(), + why + ); let err_msg = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&err_msg); return (true, dafny_runtime::Sequence::default(), err_msg); } @@ -111,8 +122,7 @@ pub mod DafnyLibraries { } } - fn curr_dir() -> String - { + fn curr_dir() -> String { let path = std::env::current_dir(); match path { Ok(path) => format!("{}", path.display()), @@ -137,7 +147,12 @@ pub mod DafnyLibraries { .open(path); let mut file = match maybe_file { Err(why) => { - let err_msg = format!("couldn't open {} for writing from {}: {}", path.display(), curr_dir(), why); + let err_msg = format!( + "couldn't open {} for writing from {}: {}", + path.display(), + curr_dir(), + why + ); let err_msg = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&err_msg); return (true, err_msg); } diff --git a/StandardLibrary/runtimes/java/src/main/java/DafnyLibraries/MutableMap.java b/StandardLibrary/runtimes/java/src/main/java/DafnyLibraries/MutableMap.java index b9f2f1316..76f0ba5d9 100644 --- a/StandardLibrary/runtimes/java/src/main/java/DafnyLibraries/MutableMap.java +++ b/StandardLibrary/runtimes/java/src/main/java/DafnyLibraries/MutableMap.java @@ -8,8 +8,7 @@ import java.util.Map; import java.util.concurrent.*; -public class MutableMap - extends DafnyLibraries._ExternBase_MutableMap { +public class MutableMap implements DafnyLibraries.MutableMapTrait { private ConcurrentHashMap m; @@ -17,7 +16,6 @@ public MutableMap( dafny.TypeDescriptor _td_K, dafny.TypeDescriptor _td_V ) { - super(_td_K, _td_V); m = new ConcurrentHashMap(); } diff --git a/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/DafnyLibraries.py b/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/DafnyLibraries.py index 4c2c4f2e5..3edd73b2f 100644 --- a/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/DafnyLibraries.py +++ b/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/DafnyLibraries.py @@ -23,7 +23,7 @@ def Unlock(self): self.lock.release() -class MutableMap(smithy_dafny_standard_library.internaldafny.generated.DafnyLibraries.MutableMap): +class MutableMap(smithy_dafny_standard_library.internaldafny.generated.DafnyLibraries.MutableMapTrait): def ctor__(self): pass diff --git a/libraries b/libraries index fabf44d71..7af1ae1b9 160000 --- a/libraries +++ b/libraries @@ -1 +1 @@ -Subproject commit fabf44d71c6d5065b0021cb4e5e96b5128c87d39 +Subproject commit 7af1ae1b99aa893616db42c0ddeb5af6827b1524