Skip to content

Commit ada420d

Browse files
Move restore_from definition to cpp file
1 parent 96332d6 commit ada420d

File tree

2 files changed

+19
-17
lines changed

2 files changed

+19
-17
lines changed

src/goto-symex/renaming_level.cpp

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,3 +55,21 @@ void symex_level1t::operator()(ssa_exprt &ssa_expr)
5555
// rename!
5656
ssa_expr.set_level_1(it->second.second);
5757
}
58+
59+
void symex_level1t::restore_from(const renaming_levelt::current_namest &other)
60+
{
61+
auto it = current_names.begin();
62+
for(const auto &pair : other)
63+
{
64+
while(it != current_names.end() && it->first < pair.first)
65+
++it;
66+
if(it == current_names.end() || pair.first < it->first)
67+
current_names.insert(it, pair);
68+
else if(it != current_names.end())
69+
{
70+
PRECONDITION(it->first == pair.first);
71+
it->second = pair.second;
72+
++it;
73+
}
74+
}
75+
}

src/goto-symex/renaming_level.h

Lines changed: 1 addition & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -62,23 +62,7 @@ struct symex_level1t : public renaming_levelt
6262
{
6363
void operator()(ssa_exprt &ssa_expr);
6464

65-
void restore_from(const current_namest &other)
66-
{
67-
auto it = current_names.begin();
68-
for(const auto &pair : other)
69-
{
70-
while(it != current_names.end() && it->first < pair.first)
71-
++it;
72-
if(it == current_names.end() || pair.first < it->first)
73-
current_names.insert(it, pair);
74-
else if(it != current_names.end())
75-
{
76-
PRECONDITION(it->first == pair.first);
77-
it->second = pair.second;
78-
++it;
79-
}
80-
}
81-
}
65+
void restore_from(const current_namest &other);
8266

8367
symex_level1t() = default;
8468
~symex_level1t() override = default;

0 commit comments

Comments
 (0)