diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 0b99d2434f0..6bba6a2ead0 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -25,6 +25,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +static void get_l1_name(exprt &expr); + goto_symex_statet::goto_symex_statet() : depth(0), symex_target(nullptr), @@ -220,7 +222,7 @@ void goto_symex_statet::assignment( get_l1_name(l1_rhs); ssa_exprt l1_lhs(lhs); - get_l1_name(l1_lhs); + l1_lhs.remove_level_2(); if(run_validation_checks) { @@ -750,7 +752,7 @@ void goto_symex_statet::get_original_name(typet &type) const } } -void goto_symex_statet::get_l1_name(exprt &expr) const +static void get_l1_name(exprt &expr) { // do not reset the type ! diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index b2dcd4741dc..83923692de5 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -97,9 +97,6 @@ class goto_symex_statet final void set_l1_indices(ssa_exprt &expr, const namespacet &ns); void set_l2_indices(ssa_exprt &expr, const namespacet &ns); - // only required for value_set.assign - void get_l1_name(exprt &expr) const; - // this maps L1 names to (L2) types typedef std::unordered_map l1_typest; l1_typest l1_types; diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp index ce3b2527f51..3d25ae8c328 100644 --- a/src/util/ssa_expr.cpp +++ b/src/util/ssa_expr.cpp @@ -13,6 +13,10 @@ Author: Daniel Kroening, kroening@kroening.com #include +/// If \p expr is a symbol "s" add to \p os "s!l0@l1#l2" and to \p l1_object_os +/// "s!l0@l1". +/// If \p expr is a member or index expression, recursively apply the procedure +/// and add ".component_name" or "[index]" to \p os. static void build_ssa_identifier_rec( const exprt &expr, const irep_idt &l0, @@ -82,7 +86,7 @@ bool ssa_exprt::can_build_identifier(const exprt &expr) return false; } -std::pair ssa_exprt::build_identifier( +static std::pair build_identifier( const exprt &expr, const irep_idt &l0, const irep_idt &l1, @@ -95,3 +99,14 @@ std::pair ssa_exprt::build_identifier( return std::make_pair(irep_idt(oss.str()), irep_idt(l1_object_oss.str())); } + +void ssa_exprt::update_identifier() +{ + const irep_idt &l0 = get_level_0(); + const irep_idt &l1 = get_level_1(); + const irep_idt &l2 = get_level_2(); + + auto idpair = build_identifier(get_original_expr(), l0, l1, l2); + set_identifier(idpair.first); + set(ID_L1_object_identifier, idpair.second); +} diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h index 56d4f627d8a..136065fcfe5 100644 --- a/src/util/ssa_expr.h +++ b/src/util/ssa_expr.h @@ -101,7 +101,7 @@ class ssa_exprt:public symbol_exprt void remove_level_2() { remove(ID_L2); - update_identifier(); + set_identifier(get_l1_object_identifier()); } const irep_idt get_level_0() const @@ -119,22 +119,7 @@ class ssa_exprt:public symbol_exprt return get(ID_L2); } - void update_identifier() - { - const irep_idt &l0=get_level_0(); - const irep_idt &l1=get_level_1(); - const irep_idt &l2=get_level_2(); - - auto idpair=build_identifier(get_original_expr(), l0, l1, l2); - set_identifier(idpair.first); - set(ID_L1_object_identifier, idpair.second); - } - - static std::pair build_identifier( - const exprt &src, - const irep_idt &l0, - const irep_idt &l1, - const irep_idt &l2); + void update_identifier(); /* Used to determine whether or not an identifier can be built * before trying and getting an exception */