From f21e9ed29a4433e6a636cb443ba305536e2a17c4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 Mar 2022 12:29:37 +0000 Subject: [PATCH] goto-symex: do not rely on undocumented find_symbols(expr) behaviour L2 re-renaming should not be applied to symbols contained in the type (array sizes may be symbolic). Some variants of find_symbols exclude such symbols, when others don't. (Cleanup thereof takes place in another commit.) Either way, goto-symex should be explicit in what it wants to process, which is really just the expression and all its operands. --- src/goto-symex/goto_symex_state.cpp | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index b80011ee2f0..da88f723b9b 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -20,7 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -837,13 +836,15 @@ ssa_exprt goto_symex_statet::declare(ssa_exprt ssa, const namespacet &ns) // L2 renaming const exprt fields = field_sensitivity.get_fields(ns, *this, ssa); - for(const auto &l1_symbol : find_symbols(fields)) - { - const ssa_exprt &field_ssa = to_ssa_expr(l1_symbol); - const std::size_t field_generation = level2.increase_generation( - l1_symbol.get_identifier(), field_ssa, fresh_l2_name_provider); - CHECK_RETURN(field_generation == 1); - } + fields.visit_pre([this](const exprt &e) { + if(auto l1_symbol = expr_try_dynamic_cast(e)) + { + const ssa_exprt &field_ssa = to_ssa_expr(*l1_symbol); + const std::size_t field_generation = level2.increase_generation( + l1_symbol->get_identifier(), field_ssa, fresh_l2_name_provider); + CHECK_RETURN(field_generation == 1); + } + }); record_events.push(false); exprt expr_l2 = rename(std::move(ssa), ns).get();