Skip to content

Commit 460ef35

Browse files
author
Owen Jones
committed
Refactoring: Make entryt::get_key()
1 parent f1f32dc commit 460ef35

File tree

2 files changed

+10
-9
lines changed

2 files changed

+10
-9
lines changed

cbmc/src/pointer-analysis/value_set.cpp

Lines changed: 2 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -56,15 +56,8 @@ value_sett::entryt &value_sett::get_entry(
5656
const typet &type,
5757
const namespacet &ns)
5858
{
59-
irep_idt index;
60-
61-
if(field_sensitive(e.identifier, type, ns))
62-
index=id2string(e.identifier)+e.suffix;
63-
else
64-
index=e.identifier;
65-
66-
std::pair<valuest::iterator, bool> r=
67-
values.insert(std::pair<idt, entryt>(index, e));
59+
std::pair<valuest::iterator, bool> r =
60+
values.insert(std::pair<idt, entryt>(e.get_key(type, ns), e));
6861

6962
return r.first->second;
7063
}

cbmc/src/pointer-analysis/value_set.h

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -298,6 +298,14 @@ class value_sett
298298
{
299299
return !(*this==other);
300300
}
301+
302+
const irep_idt get_key(const typet &type, const namespacet &ns) const
303+
{
304+
if(field_sensitive(identifier, type, ns))
305+
return id2string(identifier) + suffix;
306+
307+
return identifier;
308+
}
301309
};
302310

303311
/// Set of expressions; only used for the `get` API, not for internal

0 commit comments

Comments
 (0)