Skip to content

Commit 1dbd906

Browse files
committed
Use sharing_map instead of unordered_map for cache
1 parent 788012a commit 1dbd906

File tree

2 files changed

+4
-4
lines changed

2 files changed

+4
-4
lines changed

src/goto-symex/goto_state.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,21 +16,21 @@ optionalt<symbol_exprt>
1616
dereference_cachet::lookup(const exprt &dereference) const
1717
{
1818
auto it = cache.find(dereference);
19-
if(it == cache.end())
19+
if(it == nullopt)
2020
{
2121
return nullopt;
2222
}
2323
else
2424
{
25-
return {it->second};
25+
return {it->get()};
2626
}
2727
}
2828

2929
void dereference_cachet::insert(
3030
exprt new_cached_expr,
3131
symbol_exprt new_cache_symbol)
3232
{
33-
cache.emplace(std::move(new_cached_expr), std::move(new_cache_symbol));
33+
cache.insert(std::move(new_cached_expr), std::move(new_cache_symbol));
3434
}
3535

3636
/// Print the constant propagation map in a human-friendly format.

src/goto-symex/goto_state.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ class goto_symex_statet;
3131
struct dereference_cachet
3232
{
3333
private:
34-
std::unordered_map<exprt, symbol_exprt, irep_hash> cache;
34+
sharing_mapt<exprt, symbol_exprt, false, irep_hash> cache;
3535

3636
public:
3737
optionalt<symbol_exprt> lookup(const exprt &pointer) const;

0 commit comments

Comments
 (0)