Revert some changes on test and ex spec

verus-lang · Oct 2, 2024 · 89a55a6 · 89a55a6
1 parent 7893343
commit 89a55a6
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 37 deletions.
diff --git a/source/rust_verify_test/tests/hash.rs b/source/rust_verify_test/tests/hash.rs
@@ -57,20 +57,6 @@ test_verify_one_file! {
             assert(!m@.contains_key(6));
             assert(m@.contains_key(3));
 
-            m.extend({
-                let mut other = HashMap::<u32, i8>::new();
-                assert(other@ == Map::<u32, i8>::empty());
-
-                other.insert(3, 5);
-                other.insert(6, 7);
-                assert(other@[3] == 5);
-                other
-            });
-            assert(m@.contains_key(6));
-            assert(m@[6] == 7);
-            assert(m@.contains_key(3));
-            assert(m@[3] == 5);
-
             m.clear();
             assert(!m@.contains_key(3));
             let b = m.contains_key(&3);
@@ -699,20 +685,6 @@ test_verify_one_file! {
             assert(!m@.contains_key(six@));
             assert(m@.contains_key(three@));
 
-            m.extend({
-                let mut other = StringHashMap::<i8>::new();
-                assert(other@ == Map::<Seq<char>, i8>::empty());
-
-                other.insert(three.clone(), 5);
-                other.insert(six.clone(), 7);
-                assert(other@[three@] == 5);
-                other
-            });
-            assert(m@.contains_key(six@));
-            assert(m@[six@] == 7);
-            assert(m@.contains_key(three@));
-            assert(m@[three@] == 5);
-
             m.clear();
             assert(!m@.contains_key(three@));
             let b = m.contains_key(three.as_str());

diff --git a/source/vstd/std_specs/hash.rs b/source/vstd/std_specs/hash.rs
@@ -494,15 +494,6 @@ pub fn ex_hash_map_clear<Key, Value, S>(m: &mut HashMap<Key, Value, S>)
     m.clear()
 }
 
-#[verifier::external_fn_specification]
-pub fn ex_hash_map_extend<Key, Value>(m: &mut HashMap<Key, Value>, other: HashMap<Key, Value>)
-    where Key: Eq + Hash
-    ensures
-        m@ == old(m)@.union_prefer_right(other@),
-{
-    m.extend(other)
-}
-
 // We now specify the behavior of `HashSet`.
 #[verifier::external_type_specification]
 #[verifier::external_body]