Skip to content

Commit aa3f0f1

Browse files
Make renamedt inherit from underlyingt
This is so that we can easily convert from an exprt to a renamedt using static_cast. The potential use case, is to be able to look at all the operands of a renamedt, as renamedt themselves without having to construct new objects. For instance assuming `f` takes `renamedt` as argument, we could declare a renamedt method: ``` void renamedt::apply_to_operands() { for(exprt &op : operands()) f(static_cast<renamedt&>(op)); } ```
1 parent 42b2b34 commit aa3f0f1

File tree

3 files changed

+17
-14
lines changed

3 files changed

+17
-14
lines changed

src/goto-symex/goto_symex_state.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -261,12 +261,12 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
261261
if(level == L0)
262262
{
263263
return renamedt<exprt, level>{
264-
std::move(rename_ssa<L0>(std::move(ssa), ns).value)};
264+
std::move(rename_ssa<L0>(std::move(ssa), ns).value())};
265265
}
266266
else if(level == L1)
267267
{
268268
return renamedt<exprt, level>{
269-
std::move(rename_ssa<L1>(std::move(ssa), ns).value)};
269+
std::move(rename_ssa<L1>(std::move(ssa), ns).value())};
270270
}
271271
else if(level==L2)
272272
{

src/goto-symex/renaming_level.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -50,27 +50,27 @@ operator()(renamedt<ssa_exprt, L0> l0_expr) const
5050
!l0_expr.get().get_level_1().empty() ||
5151
!l0_expr.get().get_level_2().empty())
5252
{
53-
return renamedt<ssa_exprt, L1>{std::move(l0_expr.value)};
53+
return renamedt<ssa_exprt, L1>{std::move(l0_expr.value())};
5454
}
5555

5656
const irep_idt l0_name = l0_expr.get().get_l1_object_identifier();
5757

5858
const auto it = current_names.find(l0_name);
5959
if(it == current_names.end())
60-
return renamedt<ssa_exprt, L1>{std::move(l0_expr.value)};
60+
return renamedt<ssa_exprt, L1>{std::move(l0_expr.value())};
6161

6262
// rename!
63-
l0_expr.value.set_level_1(it->second.second);
64-
return renamedt<ssa_exprt, L1>{std::move(l0_expr.value)};
63+
l0_expr.value().set_level_1(it->second.second);
64+
return renamedt<ssa_exprt, L1>{std::move(l0_expr.value())};
6565
}
6666

6767
renamedt<ssa_exprt, L2> symex_level2t::
6868
operator()(renamedt<ssa_exprt, L1> l1_expr) const
6969
{
7070
if(!l1_expr.get().get_level_2().empty())
71-
return renamedt<ssa_exprt, L2>{std::move(l1_expr.value)};
72-
l1_expr.value.set_level_2(current_count(l1_expr.get().get_identifier()));
73-
return renamedt<ssa_exprt, L2>{std::move(l1_expr.value)};
71+
return renamedt<ssa_exprt, L2>{std::move(l1_expr.value())};
72+
l1_expr.value().set_level_2(current_count(l1_expr.get().get_identifier()));
73+
return renamedt<ssa_exprt, L2>{std::move(l1_expr.value())};
7474
}
7575

7676
void symex_level1t::restore_from(const current_namest &other)

src/goto-symex/renaming_level.h

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ struct symex_renaming_levelt
6969
/// Wrapper for expressions or types which have been renamed up to a given
7070
/// \p level
7171
template <typename underlyingt, levelt level>
72-
class renamedt
72+
class renamedt : private underlyingt
7373
{
7474
public:
7575
static_assert(
@@ -79,24 +79,27 @@ class renamedt
7979

8080
const underlyingt &get() const
8181
{
82-
return value;
82+
return static_cast<const underlyingt &>(*this);
8383
}
8484

8585
void simplify(const namespacet &ns)
8686
{
87-
(void)::simplify(value, ns);
87+
(void)::simplify(value(), ns);
8888
}
8989

9090
private:
91-
underlyingt value;
91+
underlyingt &value()
92+
{
93+
return static_cast<underlyingt &>(*this);
94+
};
9295

9396
friend struct symex_level0t;
9497
friend struct symex_level1t;
9598
friend struct symex_level2t;
9699
friend class goto_symex_statet;
97100

98101
/// Only the friend classes can create renamedt objects
99-
explicit renamedt(underlyingt value) : value(std::move(value))
102+
explicit renamedt(underlyingt value) : underlyingt(std::move(value))
100103
{
101104
}
102105
};

0 commit comments

Comments
 (0)