replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Add convenience method sharing_mapt::erase_if_exists 

Just saves repeating the if-has-key-then-erase pattern
This commit is contained in:
Chris Smowton 2019-04-15 16:32:02 +01:00
parent d5df938726
commit f0de6395e8
2 changed files with 19 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/util/sharing_map.h
View File

@ -222,6 +222,19 @@ public:
/// \param k: The key of the element to erase
void erase(const key_type &k);
/// Erase element if it exists
///
/// Complexity:
/// - Worst case: O(H * S + M)
/// - Best case: O(H)
///
/// \param k: The key of the element to erase
void erase_if_exists(const key_type &k)
{
if(has_key(k))
erase(k);
}
/// Insert element, element must not exist in map
///
/// Complexity:

6
unit/util/sharing_map.cpp
View File

@ -201,6 +201,12 @@ TEST_CASE("Sharing map interface", "[core][util]")
sm.erase("j");
REQUIRE(!sm.has_key("j"));
sm.erase_if_exists("j");
REQUIRE(!sm.has_key("j"));
sm.insert("j", "1");
sm.erase_if_exists("j");
REQUIRE(!sm.has_key("j"));
sm.insert("i", "0");
sm.insert("j", "1");