diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index b9dab60e6f6..a3ba83bc5f4 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -261,12 +261,12 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) if(level == L0) { return renamedt{ - std::move(rename_ssa(std::move(ssa), ns).value)}; + std::move(rename_ssa(std::move(ssa), ns).value())}; } else if(level == L1) { return renamedt{ - std::move(rename_ssa(std::move(ssa), ns).value)}; + std::move(rename_ssa(std::move(ssa), ns).value())}; } else if(level==L2) { diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp index 96c065483dd..fdc1164da62 100644 --- a/src/goto-symex/renaming_level.cpp +++ b/src/goto-symex/renaming_level.cpp @@ -50,27 +50,27 @@ operator()(renamedt l0_expr) const !l0_expr.get().get_level_1().empty() || !l0_expr.get().get_level_2().empty()) { - return renamedt{std::move(l0_expr.value)}; + return renamedt{std::move(l0_expr.value())}; } const irep_idt l0_name = l0_expr.get().get_l1_object_identifier(); const auto it = current_names.find(l0_name); if(it == current_names.end()) - return renamedt{std::move(l0_expr.value)}; + return renamedt{std::move(l0_expr.value())}; // rename! - l0_expr.value.set_level_1(it->second.second); - return renamedt{std::move(l0_expr.value)}; + l0_expr.value().set_level_1(it->second.second); + return renamedt{std::move(l0_expr.value())}; } renamedt symex_level2t:: operator()(renamedt l1_expr) const { if(!l1_expr.get().get_level_2().empty()) - return renamedt{std::move(l1_expr.value)}; - l1_expr.value.set_level_2(current_count(l1_expr.get().get_identifier())); - return renamedt{std::move(l1_expr.value)}; + return renamedt{std::move(l1_expr.value())}; + l1_expr.value().set_level_2(current_count(l1_expr.get().get_identifier())); + return renamedt{std::move(l1_expr.value())}; } void symex_level1t::restore_from(const current_namest &other) diff --git a/src/goto-symex/renaming_level.h b/src/goto-symex/renaming_level.h index 4ed86353767..2d8b5bfcafb 100644 --- a/src/goto-symex/renaming_level.h +++ b/src/goto-symex/renaming_level.h @@ -69,7 +69,7 @@ struct symex_renaming_levelt /// Wrapper for expressions or types which have been renamed up to a given /// \p level template -class renamedt +class renamedt : private underlyingt { public: static_assert( @@ -79,16 +79,19 @@ class renamedt const underlyingt &get() const { - return value; + return static_cast(*this); } void simplify(const namespacet &ns) { - (void)::simplify(value, ns); + (void)::simplify(value(), ns); } private: - underlyingt value; + underlyingt &value() + { + return static_cast(*this); + }; friend struct symex_level0t; friend struct symex_level1t; @@ -96,7 +99,7 @@ class renamedt friend class goto_symex_statet; /// Only the friend classes can create renamedt objects - explicit renamedt(underlyingt value) : value(std::move(value)) + explicit renamedt(underlyingt value) : underlyingt(std::move(value)) { } };