diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp index b3fd1f36273..bf3c2b4a02c 100644 --- a/src/goto-symex/auto_objects.cpp +++ b/src/goto-symex/auto_objects.cpp @@ -87,7 +87,7 @@ void goto_symext::trigger_auto_object( const ssa_exprt &ssa_expr=to_ssa_expr(expr); const irep_idt &obj_identifier=ssa_expr.get_object_name(); - if(obj_identifier!="goto_symex::\\guard") + if(obj_identifier != statet::guard_identifier()) { const symbolt &symbol= ns.lookup(obj_identifier); diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 08c9ab12398..70a56aa7df3 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -84,7 +84,6 @@ class goto_symext target(_target), atomic_section_counter(0), log(mh), - guard_identifier("goto_symex::\\guard"), path_storage(path_storage), path_segment_vccs(0), _total_vccs(std::numeric_limits::max()), @@ -238,10 +237,6 @@ class goto_symext guardt &, bool keep_array); - // guards - - const irep_idt guard_identifier; - virtual void symex_goto(statet &); virtual void symex_start_thread(statet &); virtual void symex_atomic_begin(statet &); diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 7b8d5aa7c97..9554e8f8208 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -180,7 +180,7 @@ void goto_symex_statet::assignment( #if 0 PRECONDITION(l1_identifier != get_original_name(l1_identifier) - || l1_identifier=="goto_symex::\\guard" + || l1_identifier == guard_identifier() || ns.lookup(l1_identifier).is_shared() || has_prefix(id2string(l1_identifier), "symex::invalid_object") || has_prefix(id2string(l1_identifier), "symex_dynamic::dynamic_object")); @@ -372,9 +372,11 @@ bool goto_symex_statet::l2_thread_read_encoding( // is it a shared object? const irep_idt &obj_identifier=expr.get_object_name(); if( - obj_identifier == "goto_symex::\\guard" || + obj_identifier == guard_identifier() || (!ns.lookup(obj_identifier).is_shared() && !(dirty)(obj_identifier))) + { return false; + } ssa_exprt ssa_l1=expr; ssa_l1.remove_level_2(); @@ -508,9 +510,11 @@ bool goto_symex_statet::l2_thread_write_encoding( // is it a shared object? const irep_idt &obj_identifier=expr.get_object_name(); if( - obj_identifier == "goto_symex::\\guard" || + obj_identifier == guard_identifier() || (!ns.lookup(obj_identifier).is_shared() && !(dirty)(obj_identifier))) + { return false; // not shared + } // see whether we are within an atomic section if(atomic_section_id!=0) diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 3eb88a4b88b..85d0e5589ab 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -220,6 +220,13 @@ class goto_symex_statet final typedef std::map goto_state_mapt; + // guards + static irep_idt guard_identifier() + { + static irep_idt id = "goto_symex::\\guard"; + return id; + } + // stack frames -- these are used for function calls and // for exceptions struct framet diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp index 69e1e128456..baab8d0edb7 100644 --- a/src/goto-symex/renaming_level.cpp +++ b/src/goto-symex/renaming_level.cpp @@ -15,6 +15,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include +#include "goto_symex_state.h" + void symex_level0t:: operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr) { @@ -25,7 +27,7 @@ operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr) const irep_idt &obj_identifier = ssa_expr.get_object_name(); // guards are not L0-renamed - if(obj_identifier == "goto_symex::\\guard") + if(obj_identifier == goto_symex_statet::guard_identifier()) return; const symbolt *s; diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 1f18a25f313..d921f9859e7 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -243,8 +243,8 @@ void goto_symext::symex_goto(statet &state) } else { - symbol_exprt guard_symbol_expr= - symbol_exprt(guard_identifier, bool_typet()); + symbol_exprt guard_symbol_expr = + symbol_exprt(statet::guard_identifier(), bool_typet()); exprt new_rhs = boolean_negate(new_guard); ssa_exprt new_lhs(guard_symbol_expr); @@ -394,7 +394,6 @@ static void for_each2( /// \param [in, out] dest_state: second state /// \param ns: namespace /// \param diff_guard: difference between the guards of the two states -/// \param guard_identifier: prefix used for goto symex guards /// \param [out] log: logger for debug messages /// \param do_simplify: should the right-hand-side of the assignment that is /// added to the target be simplified @@ -408,7 +407,6 @@ static void merge_names( goto_symext::statet &dest_state, const namespacet &ns, const guardt &diff_guard, - const irep_idt &guard_identifier, messaget &log, const bool do_simplify, symex_target_equationt &target, @@ -419,7 +417,7 @@ static void merge_names( const irep_idt l1_identifier = ssa.get_identifier(); const irep_idt &obj_identifier = ssa.get_object_name(); - if(obj_identifier == guard_identifier) + if(obj_identifier == goto_symext::statet::guard_identifier()) return; // just a guard, don't bother if(goto_count == dest_count) @@ -544,7 +542,6 @@ void goto_symext::phi_function( dest_state, ns, diff_guard, - guard_identifier, log, symex_config.simplify_opt, target,