diff --git a/src/pervasive_ext/string_map.rs b/src/pervasive_ext/string_map.rs index 0f6c31b7b..4a154bf9e 100644 --- a/src/pervasive_ext/string_map.rs +++ b/src/pervasive_ext/string_map.rs @@ -59,6 +59,14 @@ impl StringMap { } } + #[verifier(external_body)] + pub fn extend(&mut self, m2: StringMap) + ensures + self@ == old(self)@.union_prefer_right(m2@), + { + self.inner.extend(m2.into_rust_map()) + } + #[verifier(external)] pub fn from_rust_map(inner: std::collections::BTreeMap) -> StringMap { diff --git a/src/unit_tests/kubernetes_api_objects/mod.rs b/src/unit_tests/kubernetes_api_objects/mod.rs new file mode 100644 index 000000000..fe5c6b4e8 --- /dev/null +++ b/src/unit_tests/kubernetes_api_objects/mod.rs @@ -0,0 +1,3 @@ +// Copyright 2022 VMware, Inc. +// SPDX-License-Identifier: MIT +pub mod object_meta; diff --git a/src/unit_tests/object_meta.rs b/src/unit_tests/kubernetes_api_objects/object_meta.rs similarity index 98% rename from src/unit_tests/object_meta.rs rename to src/unit_tests/kubernetes_api_objects/object_meta.rs index 9dfc68c37..8b92b8545 100644 --- a/src/unit_tests/object_meta.rs +++ b/src/unit_tests/kubernetes_api_objects/object_meta.rs @@ -11,7 +11,6 @@ verus! { #[test] #[verifier(external)] pub fn test_set_name() { - println!("Testing set_name()..."); let mut object_meta = ObjectMeta::default(); object_meta.set_name(new_strlit("name").to_string()); assert_eq!("name".to_string(), object_meta.into_kube().name.unwrap()); diff --git a/src/unit_tests/mod.rs b/src/unit_tests/mod.rs index 118fd51b2..d88d9df1e 100644 --- a/src/unit_tests/mod.rs +++ b/src/unit_tests/mod.rs @@ -1,4 +1,4 @@ // Copyright 2022 VMware, Inc. // SPDX-License-Identifier: MIT -pub mod object_meta; - +pub mod kubernetes_api_objects; +pub mod vstd_ext; diff --git a/src/unit_tests/vstd_ext/mod.rs b/src/unit_tests/vstd_ext/mod.rs new file mode 100644 index 000000000..ea73db118 --- /dev/null +++ b/src/unit_tests/vstd_ext/mod.rs @@ -0,0 +1,3 @@ +// Copyright 2022 VMware, Inc. +// SPDX-License-Identifier: MIT +pub mod string_map; diff --git a/src/unit_tests/vstd_ext/string_map.rs b/src/unit_tests/vstd_ext/string_map.rs new file mode 100644 index 000000000..d15791ced --- /dev/null +++ b/src/unit_tests/vstd_ext/string_map.rs @@ -0,0 +1,28 @@ +// Copyright 2022 VMware, Inc. +// SPDX-License-Identifier: MIT +use crate::pervasive_ext::string_map::*; +use vstd::prelude::*; +use vstd::string::*; + +verus! { + +#[test] +#[verifier(external)] +pub fn test_extend() { + let mut m = StringMap::empty(); + m.insert(new_strlit("key1").to_string(), new_strlit("val1").to_string()); + m.insert(new_strlit("key2").to_string(), new_strlit("val2").to_string()); + + let mut m2 = StringMap::empty(); + m.insert(new_strlit("key1").to_string(), new_strlit("new_val1").to_string()); + m.insert(new_strlit("key3").to_string(), new_strlit("val3").to_string()); + + m.extend(m2); + + let rust_map = m.into_rust_map(); + assert_eq!(rust_map.get(&"key1".to_string()), Some(&"new_val1".to_string())); + assert_eq!(rust_map.get(&"key2".to_string()), Some(&"val2".to_string())); + assert_eq!(rust_map.get(&"key3".to_string()), Some(&"val3".to_string())); +} + +}