diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 7aa6e2b8a3a..6cb117acc68 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -407,15 +407,12 @@ bool goto_symex_statet::l2_thread_read_encoding( guardt write_guard; write_guard.add(false_exprt()); - written_in_atomic_sectiont::const_iterator a_s_writes= - written_in_atomic_section.find(ssa_l1); + const auto a_s_writes = written_in_atomic_section.find(ssa_l1); if(a_s_writes!=written_in_atomic_section.end()) { - for(a_s_w_entryt::const_iterator it=a_s_writes->second.begin(); - it!=a_s_writes->second.end(); - ++it) + for(const auto &guard_in_list : a_s_writes->second) { - guardt g=*it; + guardt g = guard_in_list; g-=guard; if(g.is_true()) // there has already been a write to l1_identifier within @@ -423,7 +420,7 @@ bool goto_symex_statet::l2_thread_read_encoding( // that implies the current one return false; - write_guard|=*it; + write_guard |= guard_in_list; } } diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 7925bb0304d..e12365b6529 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -173,47 +173,31 @@ class goto_symex_statet final // stack frames -- these are used for function calls and // for exceptions - class framet + struct framet { - public: // function calls irep_idt function_identifier; goto_state_mapt goto_state_map; symex_targett::sourcet calling_location; goto_programt::const_targett end_of_function; - exprt return_value; - bool hidden_function; + exprt return_value = nil_exprt(); + bool hidden_function = false; symex_renaming_levelt::current_namest old_level1; - typedef std::set local_objectst; - local_objectst local_objects; - - framet(): - return_value(nil_exprt()), - hidden_function(false) - { - } + std::set local_objects; // exceptions - typedef std::map catch_mapt; - catch_mapt catch_map; + std::map catch_map; // loop and recursion unwinding struct loop_infot { - loop_infot(): - count(0), - is_recursion(false) - { - } - - unsigned count; - bool is_recursion; + unsigned count = 0; + bool is_recursion = false; }; - typedef std::unordered_map loop_iterationst; - loop_iterationst loop_iterations; + std::unordered_map loop_iterations; }; typedef std::vector call_stackt; @@ -249,40 +233,27 @@ class goto_symex_statet final // threads unsigned atomic_section_id; typedef std::pair > a_s_r_entryt; - typedef std::unordered_map - read_in_atomic_sectiont; typedef std::list a_s_w_entryt; - typedef std::unordered_map - written_in_atomic_sectiont; - read_in_atomic_sectiont read_in_atomic_section; - written_in_atomic_sectiont written_in_atomic_section; + std::unordered_map read_in_atomic_section; + std::unordered_map + written_in_atomic_section; unsigned total_vccs, remaining_vccs; - class threadt + struct threadt { - public: goto_programt::const_targett pc; guardt guard; call_stackt call_stack; std::map function_frame; - unsigned atomic_section_id; - - threadt(): - atomic_section_id(0) - { - } + unsigned atomic_section_id = 0; }; - typedef std::vector threadst; - threadst threads; + std::vector threads; bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns); bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns); - void populate_dirty_for_function( - const irep_idt &id, const goto_functiont &); - bool record_events; incremental_dirtyt dirty; @@ -294,7 +265,6 @@ class goto_symex_statet final /// \brief This state is saved, with the PC pointing to the next instruction /// of a GOTO bool has_saved_next_instruction; - bool saved_target_is_backwards; private: /// \brief Dangerous, do not use diff --git a/src/goto-symex/symex_atomic_section.cpp b/src/goto-symex/symex_atomic_section.cpp index b3d1f0b8dae..f7721c68673 100644 --- a/src/goto-symex/symex_atomic_section.cpp +++ b/src/goto-symex/symex_atomic_section.cpp @@ -45,20 +45,16 @@ void goto_symext::symex_atomic_end(statet &state) const unsigned atomic_section_id=state.atomic_section_id; state.atomic_section_id=0; - for(goto_symex_statet::read_in_atomic_sectiont::const_iterator - r_it=state.read_in_atomic_section.begin(); - r_it!=state.read_in_atomic_section.end(); - ++r_it) + for(const auto &pair : state.read_in_atomic_section) { - ssa_exprt r=r_it->first; - r.set_level_2(r_it->second.first); + ssa_exprt r = pair.first; + r.set_level_2(pair.second.first); // guard is the disjunction over reads - PRECONDITION(!r_it->second.second.empty()); - guardt read_guard(r_it->second.second.front()); - for(std::list::const_iterator - it=++(r_it->second.second.begin()); - it!=r_it->second.second.end(); + PRECONDITION(!pair.second.second.empty()); + guardt read_guard(pair.second.second.front()); + for(std::list::const_iterator it = ++(pair.second.second.begin()); + it != pair.second.second.end(); ++it) read_guard|=*it; exprt read_guard_expr=read_guard.as_expr(); @@ -71,20 +67,16 @@ void goto_symext::symex_atomic_end(statet &state) state.source); } - for(goto_symex_statet::written_in_atomic_sectiont::const_iterator - w_it=state.written_in_atomic_section.begin(); - w_it!=state.written_in_atomic_section.end(); - ++w_it) + for(const auto &pair : state.written_in_atomic_section) { - ssa_exprt w=w_it->first; + ssa_exprt w = pair.first; w.set_level_2(state.level2.current_count(w.get_identifier())); // guard is the disjunction over writes - PRECONDITION(!w_it->second.empty()); - guardt write_guard(w_it->second.front()); - for(std::list::const_iterator - it=++(w_it->second.begin()); - it!=w_it->second.end(); + PRECONDITION(!pair.second.empty()); + guardt write_guard(pair.second.front()); + for(std::list::const_iterator it = ++(pair.second.begin()); + it != pair.second.end(); ++it) write_guard|=*it; exprt write_guard_expr=write_guard.as_expr(); diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 88768c4fe6a..44b7691c496 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -298,12 +298,11 @@ void goto_symext::symex_function_call_code( frame.hidden_function=goto_function.is_hidden(); const goto_symex_statet::framet &p_frame=state.previous_frame(); - for(goto_symex_statet::framet::loop_iterationst::const_iterator - it=p_frame.loop_iterations.begin(); - it!=p_frame.loop_iterations.end(); - ++it) - if(it->second.is_recursion) - frame.loop_iterations.insert(*it); + for(const auto &pair : p_frame.loop_iterations) + { + if(pair.second.is_recursion) + frame.loop_iterations.insert(pair); + } // increase unwinding counter frame.loop_iterations[identifier].is_recursion=true; diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 9209faab474..bbeea7e9cff 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -184,7 +184,6 @@ void goto_symext::symex_goto(statet &state) path_storaget::patht next_instruction(target, state); next_instruction.state.saved_target = state_pc; next_instruction.state.has_saved_next_instruction = true; - next_instruction.state.saved_target_is_backwards = backward; path_storaget::patht jump_target(target, state); jump_target.state.saved_target = new_state_pc; @@ -192,7 +191,6 @@ void goto_symext::symex_goto(statet &state) // `forward` tells us where the branch we're _currently_ executing is // pointing to; this needs to be inverted for the branch that we're saving, // so let its truth value for `backwards` be the same as ours for `forward`. - jump_target.state.saved_target_is_backwards = !backward; log.debug() << "Saving next instruction '" << next_instruction.state.saved_target->source_location << "'"