diff --git a/regression/ansi-c/struct7/main.c b/regression/ansi-c/struct7/main.c new file mode 100644 index 00000000000..54397c6bc2d --- /dev/null +++ b/regression/ansi-c/struct7/main.c @@ -0,0 +1,11 @@ +struct S +{ + int x; + int x; +}; + +int main() +{ + struct S s; + return s.x; +} diff --git a/regression/ansi-c/struct7/test.desc b/regression/ansi-c/struct7/test.desc new file mode 100644 index 00000000000..b9bd5b62b50 --- /dev/null +++ b/regression/ansi-c/struct7/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=\(64\|1\)$ +^SIGNAL=0$ +^file main.c line 4: duplicate member x$ +^CONVERSION ERROR$ +-- diff --git a/src/aa-path-symex/path_symex_history.cpp b/src/aa-path-symex/path_symex_history.cpp index 33ed11f4f5d..e35cd62d337 100644 --- a/src/aa-path-symex/path_symex_history.cpp +++ b/src/aa-path-symex/path_symex_history.cpp @@ -29,10 +29,8 @@ void path_symex_stept::output(std::ostream &out) const out << "PCs:"; /* - for(pc_vectort::const_iterator p_it=s_it->pc_vector.begin(); - p_it!=pc_vector.end(); - p_it++) - out << " " << *p_it; + for(const auto &pc : s_it->pc_vector) + out << " " << pc; */ out << "\n"; diff --git a/src/aa-path-symex/path_symex_state.cpp b/src/aa-path-symex/path_symex_state.cpp index c0d316ced05..a078c4c2e65 100644 --- a/src/aa-path-symex/path_symex_state.cpp +++ b/src/aa-path-symex/path_symex_state.cpp @@ -85,11 +85,8 @@ void path_symex_statet::output(const threadt &thread, std::ostream &out) const { out << " PC: " << thread.pc << std::endl; out << " Call stack:"; - for(call_stackt::const_iterator - it=thread.call_stack.begin(); - it!=thread.call_stack.end(); - it++) - out << " " << it->return_location << std::endl; + for(const auto &call : thread.call_stack) + out << " " << call.return_location << std::endl; out << std::endl; } diff --git a/src/aa-symex/path_search.cpp b/src/aa-symex/path_search.cpp index 8ad24bc828e..9b8d2295a45 100644 --- a/src/aa-symex/path_search.cpp +++ b/src/aa-symex/path_search.cpp @@ -346,14 +346,11 @@ void path_searcht::do_show_vcc( std::vector steps; state.history.build_history(steps); - for(std::vector::const_iterator - s_it=steps.begin(); - s_it!=steps.end(); - s_it++) + for(const auto &step_ref : steps) { - if((*s_it)->guard.is_not_nil()) + if(step_ref->guard.is_not_nil()) { - std::string string_value=from_expr(ns, "", (*s_it)->guard); + std::string string_value=from_expr(ns, "", step_ref->guard); out << "{-" << count << "} " << string_value << "\n"; count++; } @@ -403,22 +400,16 @@ bool path_searcht::drop_state(const statet &state) const // unwinding limit -- loops if(unwind_limit!=-1 && state.get_instruction()->is_backwards_goto()) { - for(path_symex_statet::unwinding_mapt::const_iterator - it=state.unwinding_map.begin(); - it!=state.unwinding_map.end(); - it++) - if(it->second>unwind_limit) + for(const auto &loop_info : state.unwinding_map) + if(loop_info.second>unwind_limit) return true; } // unwinding limit -- recursion if(unwind_limit!=-1 && state.get_instruction()->is_function_call()) { - for(path_symex_statet::recursion_mapt::const_iterator - it=state.recursion_map.begin(); - it!=state.recursion_map.end(); - it++) - if(it->second>unwind_limit) + for(const auto &rec_info : state.recursion_map) + if(rec_info.second>unwind_limit) return true; } @@ -500,23 +491,17 @@ Function: path_searcht::initialize_property_map void path_searcht::initialize_property_map( const goto_functionst &goto_functions) { - for(goto_functionst::function_mapt::const_iterator - it=goto_functions.function_map.begin(); - it!=goto_functions.function_map.end(); - it++) + forall_goto_functions(it, goto_functions) if(!it->second.is_inlined()) { const goto_programt &goto_program=it->second.body; - for(goto_programt::instructionst::const_iterator - it=goto_program.instructions.begin(); - it!=goto_program.instructions.end(); - it++) + forall_goto_program_instructions(i_it, goto_program) { - if(!it->is_assert()) + if(!i_it->is_assert()) continue; - const locationt &location=it->location; + const locationt &location=i_it->location; irep_idt property_name=location.get_property_id(); diff --git a/src/aa-symex/symex_parseoptions.cpp b/src/aa-symex/symex_parseoptions.cpp index e9099b1d568..8eaf3de42f1 100644 --- a/src/aa-symex/symex_parseoptions.cpp +++ b/src/aa-symex/symex_parseoptions.cpp @@ -541,15 +541,12 @@ Function: symex_parseoptionst::report_properties void symex_parseoptionst::report_properties( const path_searcht::property_mapt &property_map) { - for(path_searcht::property_mapt::const_iterator - it=property_map.begin(); - it!=property_map.end(); - it++) + for(const auto &prop_pair : property_map) { if(get_ui()==ui_message_handlert::XML_UI) { xmlt xml_result("result"); - xml_result.set_attribute("claim", id2string(it->first)); + xml_result.set_attribute("claim", id2string(prop_pair.first)); std::string status_string; @@ -566,9 +563,9 @@ void symex_parseoptionst::report_properties( } else { - status() << "[" << it->first << "] " - << it->second.description << ": "; - switch(it->second.status) + status() << "[" << prop_pair.first << "] " + << prop_pair.second.description << ": "; + switch(prop_pair.second.status) { case path_searcht::PASS: status() << "OK"; break; case path_searcht::FAIL: status() << "FAILED"; break; @@ -578,8 +575,8 @@ void symex_parseoptionst::report_properties( } if(cmdline.isset("show-trace") && - it->second.status==path_searcht::FAIL) - show_counterexample(it->second.error_trace); + prop_pair.second.status==path_searcht::FAIL) + show_counterexample(prop_pair.second.error_trace); } if(!cmdline.isset("property")) @@ -588,11 +585,8 @@ void symex_parseoptionst::report_properties( unsigned failed=0; - for(path_searcht::property_mapt::const_iterator - it=property_map.begin(); - it!=property_map.end(); - it++) - if(it->second.status==path_searcht::FAIL) + for(const auto &prop_pair : property_map) + if(prop_pair.second.status==path_searcht::FAIL) failed++; status() << "** " << failed diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index 0e95e233e44..552649d6009 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -34,10 +34,7 @@ void ai_baset::output( const goto_functionst &goto_functions, std::ostream &out) const { - for(goto_functionst::function_mapt::const_iterator - f_it=goto_functions.function_map.begin(); - f_it!=goto_functions.function_map.end(); - f_it++) + forall_goto_functions(f_it, goto_functions) { if(f_it->second.body_available()) { @@ -175,10 +172,7 @@ Function: ai_baset::initialize void ai_baset::initialize(const goto_functionst &goto_functions) { - for(goto_functionst::function_mapt::const_iterator - it=goto_functions.function_map.begin(); - it!=goto_functions.function_map.end(); - it++) + forall_goto_functions(it, goto_functions) initialize(it->second); } @@ -271,13 +265,8 @@ bool ai_baset::visit( goto_program.get_successors(l, successors); - for(goto_programt::const_targetst::const_iterator - it=successors.begin(); - it!=successors.end(); - it++) + for(const auto &to_l : successors) { - locationt to_l=*it; - if(to_l==goto_program.instructions.end()) continue; @@ -512,10 +501,7 @@ void ai_baset::sequential_fixedpoint( { // do each function at least once - for(goto_functionst::function_mapt::const_iterator - it=goto_functions.function_map.begin(); - it!=goto_functions.function_map.end(); - it++) + forall_goto_functions(it, goto_functions) fixedpoint(it->second.body, goto_functions, ns); } @@ -572,21 +558,19 @@ void ai_baset::concurrent_fixedpoint( { new_shared=false; - for(thread_wlt::const_iterator it=thread_wl.begin(); - it!=thread_wl.end(); - ++it) + for(const auto &wl_pair : thread_wl) { working_sett working_set; - put_in_working_set(working_set, it->second); + put_in_working_set(working_set, wl_pair.second); - statet &begin_state=get_state(it->second); - merge(begin_state, sh_target, it->second); + statet &begin_state=get_state(wl_pair.second); + merge(begin_state, sh_target, wl_pair.second); while(!working_set.empty()) { goto_programt::const_targett l=get_next(working_set); - visit(l, working_set, *(it->first), goto_functions, ns); + visit(l, working_set, *(wl_pair.first), goto_functions, ns); // the underlying domain must make sure that the final state // carries all possible values; otherwise we would need to diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp index 347bcd0a0b2..c226e2c73ab 100644 --- a/src/analyses/call_graph.cpp +++ b/src/analyses/call_graph.cpp @@ -110,12 +110,10 @@ void call_grapht::output_dot(std::ostream &out) const { out << "digraph call_graph {\n"; - for(grapht::const_iterator it=graph.begin(); - it!=graph.end(); - it++) + for(const auto &edge : graph) { - out << " \"" << it->first << "\" -> " - << "\"" << it->second << "\" " + out << " \"" << edge.first << "\" -> " + << "\"" << edge.second << "\" " << " [arrowhead=\"vee\"];" << "\n"; } @@ -137,12 +135,9 @@ Function: call_grapht::output void call_grapht::output(std::ostream &out) const { - for(grapht::const_iterator - it=graph.begin(); - it!=graph.end(); - it++) + for(const auto &edge : graph) { - out << it->first << " -> " << it->second << "\n"; + out << edge.first << " -> " << edge.second << "\n"; } } @@ -160,15 +155,12 @@ Function: call_grapht::output_xml void call_grapht::output_xml(std::ostream &out) const { - for(grapht::const_iterator - it=graph.begin(); - it!=graph.end(); - it++) + for(const auto &edge : graph) { out << "first), out); + xmlt::escape_attribute(id2string(edge.first), out); out << "\" callee=\""; - xmlt::escape_attribute(id2string(it->second), out); + xmlt::escape_attribute(id2string(edge.second), out); out << "\">\n"; } } diff --git a/src/analyses/cfg_dominators.h b/src/analyses/cfg_dominators.h index 0abee1ec6e9..01ca0871a16 100644 --- a/src/analyses/cfg_dominators.h +++ b/src/analyses/cfg_dominators.h @@ -103,10 +103,8 @@ void cfg_dominators_templatet::initialise(P &program) cfg(program); // initialise top element - for(typename cfgt::entry_mapt::const_iterator - e_it=cfg.entry_map.begin(); - e_it!=cfg.entry_map.end(); ++e_it) - top.insert(cfg[e_it->second].PC); + for(const auto &node : cfg.entry_map) + top.insert(cfg[node.second].PC); } /*******************************************************************\ @@ -151,24 +149,18 @@ void cfg_dominators_templatet::fixedpoint(P &program) bool changed=false; typename cfgt::nodet &node=cfg[cfg.entry_map[current]]; if(node.dominators.empty()) - for(typename cfgt::edgest::const_iterator - p_it=(post_dom?node.out:node.in).begin(); - !changed && p_it!=(post_dom?node.out:node.in).end(); - ++p_it) - if(!cfg[p_it->first].dominators.empty()) + for(const auto & edge : (post_dom?node.out:node.in)) + if(!cfg[edge.first].dominators.empty()) { - node.dominators=cfg[p_it->first].dominators; + node.dominators=cfg[edge.first].dominators; node.dominators.insert(current); changed=true; } // compute intersection of predecessors - for(typename cfgt::edgest::const_iterator - p_it=(post_dom?node.out:node.in).begin(); - p_it!=(post_dom?node.out:node.in).end(); - ++p_it) + for(const auto & edge : (post_dom?node.out:node.in)) { - const target_sett &other=cfg[p_it->first].dominators; + const target_sett &other=cfg[edge.first].dominators; if(other.empty()) continue; @@ -198,12 +190,9 @@ void cfg_dominators_templatet::fixedpoint(P &program) if(changed) // fixed point for node reached? { - for(typename cfgt::edgest::const_iterator - s_it=(post_dom?node.in:node.out).begin(); - s_it!=(post_dom?node.in:node.out).end(); - ++s_it) + for(const auto & edge : (post_dom?node.in:node.out)) { - worklist.push_back(cfg[s_it->first].PC); + worklist.push_back(cfg[edge.first].PC); } } } @@ -224,21 +213,21 @@ Function: cfg_dominators_templatet::output template void cfg_dominators_templatet::output(std::ostream &out) const { - for(typename cfgt::entry_mapt::const_iterator - it=cfg.entry_map.begin(); - it!=cfg.entry_map.end(); ++it) + for(const auto &node : cfg.entry_map) { - unsigned n=it->first->location_number; + unsigned n=node.first->location_number; if(post_dom) out << n << " post-dominated by "; else out << n << " dominated by "; - for(typename target_sett::const_iterator d_it=it->second.dominators.begin(); - d_it!=it->second.dominators.end();) + for(typename target_sett::const_iterator + d_it=node.second.dominators.begin(); + d_it!=node.second.dominators.end(); + ) // no d_it++ { out << (*d_it)->location_number; - if (++d_it!=it->second.dominators.end()) + if (++d_it!=node.second.dominators.end()) out << ", "; } out << "\n"; diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 66fb6ef71b3..c7d5879d858 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -341,12 +341,9 @@ void constant_propagator_domaint::valuest::output( if(is_bottom) out << " bottom\n"; - for(replace_symbolt::expr_mapt::const_iterator - it=replace_const.expr_map.begin(); - it!=replace_const.expr_map.end(); - ++it) - out << ' ' << it->first << "=" << - from_expr(ns, "", it->second) << '\n'; + for(const auto &replace_pair : replace_const.expr_map) + out << ' ' << replace_pair.first << "=" + << from_expr(ns, "", replace_pair.second) << '\n'; } /*******************************************************************\ @@ -401,7 +398,7 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src) for(replace_symbolt::expr_mapt::const_iterator it=replace_const.expr_map.begin(); it!=replace_const.expr_map.end(); - ) + ) // no it++ { if(src.replace_const.expr_map.find(it->first) == src.replace_const.expr_map.end()) @@ -413,20 +410,17 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src) else ++it; } - for(replace_symbolt::expr_mapt::const_iterator - it=src.replace_const.expr_map.begin(); - it!=src.replace_const.expr_map.end(); - ++it) + for(const auto &src_replace_pair : src.replace_const.expr_map) { - replace_symbolt::expr_mapt::iterator - c_it = replace_const.expr_map.find(it->first); + replace_symbolt::expr_mapt::iterator c_it= + replace_const.expr_map.find(src_replace_pair.first); - if(c_it != replace_const.expr_map.end()) + if(c_it!=replace_const.expr_map.end()) { // values are different, set to top - if(c_it->second != it->second) + if(c_it->second!=src_replace_pair.second) { - changed = set_to_top(it->first); + changed=set_to_top(src_replace_pair.first); assert(changed); } } @@ -460,27 +454,24 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src) bool changed = false; - for(replace_symbolt::expr_mapt::const_iterator - it=src.replace_const.expr_map.begin(); - it!=src.replace_const.expr_map.end(); - ++it) + for(const auto &src_replace_pair : src.replace_const.expr_map) { - replace_symbolt::expr_mapt::iterator - c_it = replace_const.expr_map.find(it->first); + replace_symbolt::expr_mapt::iterator c_it= + replace_const.expr_map.find(src_replace_pair.first); - if(c_it != replace_const.expr_map.end()) + if(c_it!=replace_const.expr_map.end()) { - if(c_it->second != it->second) + if(c_it->second!=src_replace_pair.second) { set_to_bottom(); - changed = true; + changed=true; break; } } else { - set_to(it->first, it->second); - changed = true; + set_to(src_replace_pair.first, src_replace_pair.second); + changed=true; } } diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index 878a7037320..5155d13b7e5 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -288,12 +288,9 @@ std::set custom_bitvector_analysist::aliases( std::set result; - for(std::set::const_iterator - p_it=pointer_set.begin(); - p_it!=pointer_set.end(); - p_it++) + for(const auto &pointer : pointer_set) { - result.insert(dereference_exprt(*p_it)); + result.insert(dereference_exprt(pointer)); } result.insert(src); @@ -345,10 +342,9 @@ void custom_bitvector_domaint::transform( vectorst rhs_vectors=get_rhs(code_assign.rhs()); - for(std::set::const_iterator - l_it=lhs_set.begin(); l_it!=lhs_set.end(); l_it++) + for(const auto &lhs : lhs_set) { - assign_lhs(*l_it, rhs_vectors); + assign_lhs(lhs, rhs_vectors); } // is it a pointer? @@ -423,20 +419,16 @@ void custom_bitvector_domaint::transform( { if(mode==CLEAR_MAY) { - for(bitst::iterator b_it=may_bits.begin(); - b_it!=may_bits.end(); - b_it++) - clear_bit(b_it->second, bit_nr); + for(auto &bit : may_bits) + clear_bit(bit.second, bit_nr); // erase blank ones erase_blank_vectors(may_bits); } else if(mode==CLEAR_MUST) { - for(bitst::iterator b_it=must_bits.begin(); - b_it!=must_bits.end(); - b_it++) - clear_bit(b_it->second, bit_nr); + for(auto &bit : must_bits) + clear_bit(bit.second, bit_nr); // erase blank ones erase_blank_vectors(must_bits); @@ -449,10 +441,9 @@ void custom_bitvector_domaint::transform( // may alias other stuff std::set lhs_set=cba.aliases(deref, from); - for(std::set::const_iterator - l_it=lhs_set.begin(); l_it!=lhs_set.end(); l_it++) + for(const auto &lhs : lhs_set) { - set_bit(*l_it, bit_nr, mode); + set_bit(lhs, bit_nr, mode); } } } @@ -521,10 +512,9 @@ void custom_bitvector_domaint::transform( // may alias other stuff std::set lhs_set=cba.aliases(deref, from); - for(std::set::const_iterator - l_it=lhs_set.begin(); l_it!=lhs_set.end(); l_it++) + for(const auto &lhs : lhs_set) { - set_bit(*l_it, bit_nr, mode); + set_bit(lhs, bit_nr, mode); } } } @@ -576,12 +566,10 @@ void custom_bitvector_domaint::output( const custom_bitvector_analysist &cba= static_cast(ai); - for(bitst::const_iterator it=may_bits.begin(); - it!=may_bits.end(); - it++) + for(const auto &bit : may_bits) { - out << it->first << " MAY:"; - bit_vectort b=it->second; + out << bit.first << " MAY:"; + bit_vectort b=bit.second; for(unsigned i=0; b!=0; i++, b>>=1) if(b&1) @@ -594,12 +582,10 @@ void custom_bitvector_domaint::output( out << '\n'; } - for(bitst::const_iterator it=must_bits.begin(); - it!=must_bits.end(); - it++) + for(const auto &bit : must_bits) { - out << it->first << " MUST:"; - bit_vectort b=it->second; + out << bit.first << " MUST:"; + bit_vectort b=bit.second; for(unsigned i=0; b!=0; i++, b>>=1) if(b&1) @@ -642,34 +628,30 @@ bool custom_bitvector_domaint::merge( bool changed=false; // first do MAY - for(bitst::const_iterator b_it=b.may_bits.begin(); - b_it!=b.may_bits.end(); - b_it++) + for(const auto &bit : may_bits) { - bit_vectort &a_bits=may_bits[b_it->first]; + bit_vectort &a_bits=may_bits[bit.first]; bit_vectort old=a_bits; - a_bits|=b_it->second; + a_bits|=bit.second; if(old!=a_bits) changed=true; } // now do MUST - for(bitst::iterator a_it=must_bits.begin(); - a_it!=must_bits.end(); - a_it++) + for(auto &bit : must_bits) { bitst::const_iterator b_it= - b.must_bits.find(a_it->first); + b.must_bits.find(bit.first); if(b_it==b.must_bits.end()) { - a_it->second=0; + bit.second=0; changed=true; } else { - bit_vectort old=a_it->second; - a_it->second&=b_it->second; - if(old!=a_it->second) changed=true; + bit_vectort old=bit.second; + bit.second&=bit.second; + if(old!=bit.second) changed=true; } } @@ -696,7 +678,7 @@ void custom_bitvector_domaint::erase_blank_vectors(bitst &bits) { for(bitst::iterator a_it=bits.begin(); a_it!=bits.end(); - ) + ) // no a_it++ { if(a_it->second==0) a_it=bits.erase(a_it); @@ -759,12 +741,9 @@ exprt custom_bitvector_domaint::eval( { if(src.id()=="get_may") { - for(custom_bitvector_domaint::bitst::const_iterator - b_it=may_bits.begin(); - b_it!=may_bits.end(); - b_it++) + for(const auto &bit : may_bits) { - if(get_bit(b_it->second, bit_nr)) return true_exprt(); + if(get_bit(bit.second, bit_nr)) return true_exprt(); } return false_exprt(); diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index 0114058e0dc..ddabac0c522 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -36,15 +36,13 @@ bool dep_graph_domaint::merge( has_values=tvt::unknown(); depst::iterator it=control_deps.begin(); - for(depst::const_iterator ito=src.control_deps.begin(); - ito!=src.control_deps.end(); - ++ito) + for(const auto &c_dep : src.control_deps) { - while(it!=control_deps.end() && *it<*ito) + while(it!=control_deps.end() && *itsecond]; - for(cfg_post_dominatorst::cfgt::edgest::const_iterator - s_it=m.out.begin(); - s_it!=m.out.end(); - ++s_it) + for(const auto &edge : m.out) { const cfg_post_dominatorst::cfgt::nodet &m_s= - dep_graph.cfg_post_dominators().cfg[s_it->first]; + dep_graph.cfg_post_dominators().cfg[edge.first]; if(m_s.dominators.find(to)!=m_s.dominators.end()) post_dom_one=true; @@ -142,11 +135,8 @@ void dep_graph_domaint::control_dependencies( } // add edges to the graph - for(depst::const_iterator - it=control_deps.begin(); - it!=control_deps.end(); - ++it) - dep_graph.add_dep(dep_edget::CTRL, *it, to); + for(const auto &c_dep : control_deps) + dep_graph.add_dep(dep_edget::CTRL, c_dep, to); } /*******************************************************************\ @@ -215,25 +205,17 @@ void dep_graph_domaint::data_dependencies( const rd_range_domaint::ranges_at_loct &w_ranges= dep_graph.reaching_definitions()[to].get(it->first); - for(rd_range_domaint::ranges_at_loct::const_iterator - w_itl=w_ranges.begin(); - w_itl!=w_ranges.end(); - ++w_itl) + for(const auto &w_range : w_ranges) { bool found=false; - for(rd_range_domaint::rangest::const_iterator - w_it=w_itl->second.begin(); - w_it!=w_itl->second.end() && !found; - ++w_it) - for(range_domaint::const_iterator - r_it=r_ranges.begin(); - r_it!=r_ranges.end() && !found; - ++r_it) - if(may_be_def_use_pair(w_it->first, w_it->second, - r_it->first, r_it->second)) + for(const auto &wr : w_range.second) + for(const auto &r_range : r_ranges) + if(!found && + may_be_def_use_pair(wr.first, wr.second, + r_range.first, r_range.second)) { // found a def-use pair - data_deps.insert(w_itl->first); + data_deps.insert(w_range.first); found=true; } } @@ -242,15 +224,12 @@ void dep_graph_domaint::data_dependencies( } // add edges to the graph - for(depst::const_iterator - it=data_deps.begin(); - it!=data_deps.end(); - ++it) + for(const auto &d_dep : data_deps) { // *it might be handled in a future call call to visit only, // depending on the sequence of successors; make sure it exists - dep_graph.get_state(*it); - dep_graph.add_dep(dep_edget::DATA, *it, to); + dep_graph.get_state(d_dep); + dep_graph.add_dep(dep_edget::DATA, d_dep, to); } } @@ -286,14 +265,12 @@ void dep_graph_domaint::transform( assert(s!=0); depst::iterator it=s->control_deps.begin(); - for(depst::const_iterator ito=control_deps.begin(); - ito!=control_deps.end(); - ++ito) + for(const auto &c_dep : control_deps) { - while(it!=s->control_deps.end() && *it<*ito) + while(it!=s->control_deps.end() && *itcontrol_deps.end() || *ito<*it) - s->control_deps.insert(it, *ito); + if(it==s->control_deps.end() || c_dep<*it) + s->control_deps.insert(it, c_dep); else if(it!=s->control_deps.end()) ++it; } diff --git a/src/analyses/dirty.cpp b/src/analyses/dirty.cpp index bc4327581cd..a159f6ddef2 100644 --- a/src/analyses/dirty.cpp +++ b/src/analyses/dirty.cpp @@ -114,9 +114,6 @@ Function: dirtyt::output void dirtyt::output(std::ostream &out) const { - for(id_sett::const_iterator - it=dirty.begin(); - it!=dirty.end(); - it++) - out << *it << std::endl; + for(const auto &d : dirty) + out << d << std::endl; } diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index 711dd35d170..15c25eefea7 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -10,8 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "escape_analysis.h" -#include - /*******************************************************************\ Function: escape_domaint::is_tracked @@ -119,11 +117,9 @@ void escape_domaint::assign_lhs_aliases( aliases.isolate(identifier); - for(std::set::const_iterator it=alias_set.begin(); - it!=alias_set.end(); - it++) + for(const auto &alias : alias_set) { - aliases.make_union(identifier, *it); + aliases.make_union(identifier, alias); } } } @@ -195,11 +191,9 @@ void escape_domaint::get_rhs_aliases( irep_idt identifier=symbol_expr.get_identifier(); alias_set.insert(identifier); - for(aliasest::const_iterator it=aliases.begin(); - it!=aliases.end(); - it++) - if(aliases.same_set(*it, identifier)) - alias_set.insert(*it); + for(const auto &alias : aliases) + if(aliases.same_set(alias, identifier)) + alias_set.insert(alias); } } else if(rhs.id()==ID_if) @@ -329,10 +323,9 @@ void escape_domaint::transform( std::set lhs_set; get_rhs_aliases(lhs, lhs_set); - for(std::set::const_iterator - l_it=lhs_set.begin(); l_it!=lhs_set.end(); l_it++) + for(const auto &lhs : lhs_set) { - cleanup_map[*l_it].cleanup_functions.insert(cleanup_function); + cleanup_map[lhs].cleanup_functions.insert(cleanup_function); } } } @@ -372,16 +365,11 @@ void escape_domaint::output( return; } - for(cleanup_mapt::const_iterator it=cleanup_map.begin(); - it!=cleanup_map.end(); - it++) + for(const auto &cleanup : cleanup_map) { - out << it->first << ':'; - for(std::set::const_iterator - c_it=it->second.cleanup_functions.begin(); - c_it!=it->second.cleanup_functions.end(); - c_it++) - out << ' ' << *c_it; + out << cleanup.first << ':'; + for(const auto &id : cleanup.second.cleanup_functions) + out << ' ' << id; out << '\n'; } @@ -435,12 +423,10 @@ bool escape_domaint::merge( bool changed=false; - for(cleanup_mapt::const_iterator b_it=b.cleanup_map.begin(); - b_it!=b.cleanup_map.end(); - b_it++) + for(const auto &cleanup : b.cleanup_map) { - const std::set &b_cleanup=b_it->second.cleanup_functions; - std::set &a_cleanup=cleanup_map[b_it->first].cleanup_functions; + const std::set &b_cleanup=cleanup.second.cleanup_functions; + std::set &a_cleanup=cleanup_map[cleanup.first].cleanup_functions; unsigned old_size=a_cleanup.size(); a_cleanup.insert(b_cleanup.begin(), b_cleanup.end()); if(a_cleanup.size()!=old_size) changed=true; @@ -514,12 +500,9 @@ void escape_domaint::check_lhs( unsigned count=0; - for(aliasest::const_iterator - a_it=aliases.begin(); - a_it!=aliases.end(); - a_it++) + for(const auto &alias : aliases) { - if(*a_it!=identifier && aliases.same_set(*a_it, identifier)) + if(alias!=identifier && aliases.same_set(alias, identifier)) count+=1; } @@ -556,11 +539,9 @@ void escape_analysist::insert_cleanup( { source_locationt source_location=location->source_location; - for(std::set::const_iterator c_it=cleanup_functions.begin(); - c_it!=cleanup_functions.end(); - c_it++) + for(const auto &cleanup : cleanup_functions) { - symbol_exprt function=ns.lookup(*c_it).symbol_expr(); + symbol_exprt function=ns.lookup(cleanup).symbol_expr(); const code_typet &function_type=to_code_type(function.type()); goto_function.body.insert_before_swap(location); @@ -645,11 +626,17 @@ void escape_analysist::instrument( insert_cleanup(f_it->second, i_it, code_dead.symbol(), cleanup_functions1, true, ns); insert_cleanup(f_it->second, i_it, code_dead.symbol(), cleanup_functions2, false, ns); - for(unsigned i=0; ifirst << std::endl; @@ -268,13 +265,8 @@ bool flow_insensitive_analysis_baset::visit( else statistics[l]++; - for(goto_programt::const_targetst::const_iterator - it=successors.begin(); - it!=successors.end(); - it++) + for(const auto &to_l : successors) { - locationt to_l=*it; - if(to_l==goto_program.instructions.end()) continue; @@ -492,13 +484,11 @@ bool flow_insensitive_analysis_baset::do_function_call_rec( get_reference_set(function, values); // now call all of these - for(expr_sett::const_iterator it=values.begin(); - it!=values.end(); - it++) + for(const auto &v : values) { - if(it->id()==ID_object_descriptor) + if(v.id()==ID_object_descriptor) { - const object_descriptor_exprt &o=to_object_descriptor_expr(*it); + const object_descriptor_exprt &o=to_object_descriptor_expr(v); // ... but only if they are actually functions. goto_functionst::function_mapt::const_iterator it= @@ -554,10 +544,7 @@ void flow_insensitive_analysis_baset::fixedpoint( { // do each function at least once - for(goto_functionst::function_mapt::const_iterator - it=goto_functions.function_map.begin(); - it!=goto_functions.function_map.end(); - it++) + forall_goto_functions(it, goto_functions) if(functions_done.find(it->first)== functions_done.end()) { diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp index f89530d3ed8..a3c5d4629e6 100644 --- a/src/analyses/global_may_alias.cpp +++ b/src/analyses/global_may_alias.cpp @@ -30,11 +30,9 @@ void global_may_alias_domaint::assign_lhs_aliases( aliases.isolate(identifier); - for(std::set::const_iterator it=alias_set.begin(); - it!=alias_set.end(); - it++) + for(const auto &alias : alias_set) { - aliases.make_union(identifier, *it); + aliases.make_union(identifier, alias); } } } @@ -60,11 +58,9 @@ void global_may_alias_domaint::get_rhs_aliases( irep_idt identifier=to_symbol_expr(rhs).get_identifier(); alias_set.insert(identifier); - for(aliasest::const_iterator it=aliases.begin(); - it!=aliases.end(); - it++) - if(aliases.same_set(*it, identifier)) - alias_set.insert(*it); + for(const auto &alias : alias_set) + if(aliases.same_set(alias, identifier)) + alias_set.insert(alias); } else if(rhs.id()==ID_if) { diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 0bc3a1c7826..131b7890de5 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1380,10 +1380,8 @@ void goto_checkt::check_rec( guardt old_guard=guard; - for(unsigned i=0; iguard=false_exprt(); t->source_location=i.source_location; t->source_location.set_property_class("error label"); - t->source_location.set_comment("error label "+*l_it); + t->source_location.set_comment("error label "+label); t->source_location.set("user-provided", true); } } @@ -1734,10 +1729,7 @@ void goto_checkt::goto_check(goto_functiont &goto_function) } } - for(goto_programt::instructionst::iterator - i_it=new_code.instructions.begin(); - i_it!=new_code.instructions.end(); - i_it++) + Forall_goto_program_instructions(i_it, new_code) { if(i_it->source_location.is_nil()) { @@ -1810,10 +1802,7 @@ void goto_check( { goto_checkt goto_check(ns, options); - for(goto_functionst::function_mapt::iterator - it=goto_functions.function_map.begin(); - it!=goto_functions.function_map.end(); - it++) + Forall_goto_functions(it, goto_functions) { goto_check.goto_check(it->second); } @@ -1838,10 +1827,7 @@ void goto_check( const namespacet ns(goto_model.symbol_table); goto_checkt goto_check(ns, options); - for(goto_functionst::function_mapt::iterator - it=goto_model.goto_functions.function_map.begin(); - it!=goto_model.goto_functions.function_map.end(); - it++) + Forall_goto_functions(it, goto_model.goto_functions) { goto_check.goto_check(it->second); } diff --git a/src/analyses/interval_analysis.cpp b/src/analyses/interval_analysis.cpp index f260c10372d..17c3dd68562 100644 --- a/src/analyses/interval_analysis.cpp +++ b/src/analyses/interval_analysis.cpp @@ -65,12 +65,9 @@ void instrument_intervals( exprt::operandst assertion; - for(std::set::const_iterator - s_it=symbols.begin(); - s_it!=symbols.end(); - s_it++) + for(const auto &symbol_expr : symbols) { - exprt tmp=d.make_expression(*s_it); + exprt tmp=d.make_expression(symbol_expr); if(!tmp.is_true()) assertion.push_back(tmp); } diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 93a487f6c41..0d5ca3d80aa 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -41,27 +41,25 @@ void interval_domaint::output( return; } - for(int_mapt::const_iterator - i_it=int_map.begin(); i_it!=int_map.end(); i_it++) + for(const auto &interval : int_map) { - if(i_it->second.is_top()) continue; - if(i_it->second.lower_set) - out << i_it->second.lower << " <= "; - out << i_it->first; - if(i_it->second.upper_set) - out << " <= " << i_it->second.upper; + if(interval.second.is_top()) continue; + if(interval.second.lower_set) + out << interval.second.lower << " <= "; + out << interval.first; + if(interval.second.upper_set) + out << " <= " << interval.second.upper; out << "\n"; } - for(float_mapt::const_iterator - i_it=float_map.begin(); i_it!=float_map.end(); i_it++) + for(const auto &interval : float_map) { - if(i_it->second.is_top()) continue; - if(i_it->second.lower_set) - out << i_it->second.lower << " <= "; - out << i_it->first; - if(i_it->second.upper_set) - out << " <= " << i_it->second.upper; + if(interval.second.is_top()) continue; + if(interval.second.lower_set) + out << interval.second.lower << " <= "; + out << interval.first; + if(interval.second.upper_set) + out << " <= " << interval.second.upper; out << "\n"; } } diff --git a/src/analyses/invariant_propagation.cpp b/src/analyses/invariant_propagation.cpp index d73ad724eee..c7ed805eddf 100644 --- a/src/analyses/invariant_propagation.cpp +++ b/src/analyses/invariant_propagation.cpp @@ -28,10 +28,8 @@ Function: invariant_propagationt::make_all_true void invariant_propagationt::make_all_true() { - for(state_mapt::iterator it=state_map.begin(); - it!=state_map.end(); - it++) - it->second.invariant_set.make_true(); + for(auto &state : state_map) + state.second.invariant_set.make_true(); } /*******************************************************************\ @@ -48,10 +46,8 @@ Function: invariant_propagationt::make_all_false void invariant_propagationt::make_all_false() { - for(state_mapt::iterator it=state_map.begin(); - it!=state_map.end(); - it++) - it->second.invariant_set.make_false(); + for(auto &state : state_map) + state.second.invariant_set.make_false(); } /*******************************************************************\ @@ -81,10 +77,7 @@ void invariant_propagationt::add_objects( typedef std::unordered_map object_cachet; object_cachet object_cache; - for(goto_programt::instructionst::const_iterator - i_it=goto_program.instructions.begin(); - i_it!=goto_program.instructions.end(); - i_it++) + forall_goto_program_instructions(i_it, goto_program) { #if 0 invariant_sett &is=(*this)[i_it].invariant_set; @@ -92,19 +85,16 @@ void invariant_propagationt::add_objects( is.add_objects(globals); #endif - for(goto_programt::decl_identifierst::const_iterator - l_it=locals.begin(); - l_it!=locals.end(); - l_it++) + for(const auto &local : locals) { // cache hit? - object_cachet::const_iterator e_it=object_cache.find(*l_it); + object_cachet::const_iterator e_it=object_cache.find(local); if(e_it==object_cache.end()) { - const symbolt &symbol=ns.lookup(*l_it); + const symbolt &symbol=ns.lookup(local); - object_listt &objects=object_cache[*l_it]; + object_listt &objects=object_cache[local]; get_objects(symbol, objects); #if 0 is.add_objects(objects); @@ -138,11 +128,8 @@ void invariant_propagationt::get_objects( get_objects_rec(symbol.symbol_expr(), object_list); - for(std::list::const_iterator - it=object_list.begin(); - it!=object_list.end(); - it++) - dest.push_back(object_store.add(*it)); + for(const auto &expr : object_list) + dest.push_back(object_store.add(expr)); } /*******************************************************************\ @@ -173,13 +160,10 @@ void invariant_propagationt::get_objects_rec( exprt member_expr(ID_member); member_expr.copy_to_operands(src); - for(struct_typet::componentst::const_iterator - it=c.begin(); - it!=c.end(); - it++) + for(const auto &component : c) { - member_expr.set(ID_component_name, it->get_string(ID_name)); - member_expr.type()=it->type(); + member_expr.set(ID_component_name, component.get_name()); + member_expr.type()=component.type(); // recursive call get_objects_rec(member_expr, dest); } @@ -214,10 +198,7 @@ void invariant_propagationt::add_objects( object_listt globals; get_globals(globals); - for(goto_functionst::function_mapt::const_iterator - f_it=goto_functions.function_map.begin(); - f_it!=goto_functions.function_map.end(); - f_it++) + forall_goto_functions(f_it, goto_functions) { // get the locals std::set locals; @@ -229,10 +210,7 @@ void invariant_propagationt::add_objects( typedef std::unordered_map object_cachet; object_cachet object_cache; - for(goto_programt::instructionst::const_iterator - i_it=goto_program.instructions.begin(); - i_it!=goto_program.instructions.end(); - i_it++) + forall_goto_program_instructions(i_it, goto_program) { #if 0 invariant_sett &is=(*this)[i_it].invariant_set; @@ -240,19 +218,16 @@ void invariant_propagationt::add_objects( is.add_objects(globals); #endif - for(std::set::const_iterator - l_it=locals.begin(); - l_it!=locals.end(); - l_it++) + for(const auto &local : locals) { // cache hit? - object_cachet::const_iterator e_it=object_cache.find(*l_it); + object_cachet::const_iterator e_it=object_cache.find(local); if(e_it==object_cache.end()) { - const symbolt &symbol=ns.lookup(*l_it); + const symbolt &symbol=ns.lookup(local); - object_listt &objects=object_cache[*l_it]; + object_listt &objects=object_cache[local]; get_objects(symbol, objects); #if 0 is.add_objects(objects); @@ -370,10 +345,7 @@ void invariant_propagationt::initialize(const goto_functionst &goto_functions) { baset::initialize(goto_functions); - for(goto_functionst::function_mapt::const_iterator f_it= - goto_functions.function_map.begin(); - f_it!=goto_functions.function_map.end(); - f_it++) + forall_goto_functions(f_it, goto_functions) initialize(f_it->second.body); } diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp index c5cfac661a5..171e6510233 100644 --- a/src/analyses/invariant_set.cpp +++ b/src/analyses/invariant_set.cpp @@ -349,15 +349,11 @@ void invariant_sett::add_eq(const std::pair &p) // replicate <= and != constraints - for(ineq_sett::const_iterator it=le_set.begin(); - it!=le_set.end(); - it++) - add_eq(le_set, p, *it); - - for(ineq_sett::const_iterator it=ne_set.begin(); - it!=ne_set.end(); - it++) - add_eq(ne_set, p, *it); + for(const auto &le : le_set) + add_eq(le_set, p, le); + + for(const auto &ne : ne_set) + add_eq(ne_set, p, ne); } /*******************************************************************\ @@ -509,30 +505,24 @@ void invariant_sett::output( out << std::endl; } - for(bounds_mapt::const_iterator it=bounds_map.begin(); - it!=bounds_map.end(); - it++) + for(const auto &bounds : bounds_map) { - out << to_string(it->first, identifier) - << " in " << it->second + out << to_string(bounds.first, identifier) + << " in " << bounds.second << std::endl; } - for(ineq_sett::const_iterator it=le_set.begin(); - it!=le_set.end(); - it++) + for(const auto &le : le_set) { - out << to_string(it->first, identifier) - << " <= " << to_string(it->second, identifier) + out << to_string(le.first, identifier) + << " <= " << to_string(le.second, identifier) << std::endl; } - for(ineq_sett::const_iterator it=ne_set.begin(); - it!=ne_set.end(); - it++) + for(const auto &ne : ne_set) { - out << to_string(it->first, identifier) - << " != " << to_string(it->second, identifier) + out << to_string(ne.first, identifier) + << " != " << to_string(ne.second, identifier) << std::endl; } } @@ -697,24 +687,19 @@ void invariant_sett::strengthen_rec(const exprt &expr) { const struct_typet &struct_type=to_struct_type(op_type); - const struct_typet::componentst &c=struct_type.components(); - exprt lhs_member_expr(ID_member); exprt rhs_member_expr(ID_member); lhs_member_expr.copy_to_operands(expr.op0()); rhs_member_expr.copy_to_operands(expr.op1()); - for(struct_typet::componentst::const_iterator - it=c.begin(); - it!=c.end(); - it++) + for(const auto &comp : struct_type.components()) { - const irep_idt &component_name=it->get(ID_name); + const irep_idt &component_name=comp.get(ID_name); lhs_member_expr.set(ID_component_name, component_name); rhs_member_expr.set(ID_component_name, component_name); - lhs_member_expr.type()=it->type(); - rhs_member_expr.type()=it->type(); + lhs_member_expr.type()=comp.type(); + rhs_member_expr.type()=comp.type(); equal_exprt equality; equality.lhs()=lhs_member_expr; diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp index 1c14ad9d424..a808609497e 100644 --- a/src/analyses/is_threaded.cpp +++ b/src/analyses/is_threaded.cpp @@ -106,17 +106,8 @@ void is_threadedt::compute(const goto_functionst &goto_functions) is_threaded_analysis(goto_functions, ns); - for(goto_functionst::function_mapt::const_iterator - f_it=goto_functions.function_map.begin(); - f_it!=goto_functions.function_map.end(); - f_it++) - { - const goto_programt &goto_program=f_it->second.body; - for(goto_programt::instructionst::const_iterator - i_it=goto_program.instructions.begin(); - i_it!=goto_program.instructions.end(); - i_it++) + forall_goto_functions(f_it, goto_functions) + forall_goto_program_instructions(i_it, f_it->second.body) if(is_threaded_analysis[i_it].is_threaded) is_threaded_set.insert(i_it); - } } diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index 9e01e9cb283..d6d15a19abd 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -323,12 +323,9 @@ void local_bitvector_analysist::build(const goto_functiont &goto_function) // Gather the objects we track, and // feed in sufficiently bad defaults for their value // in the entry location. - for(localst::locals_mapt::const_iterator - it=locals.locals_map.begin(); - it!=locals.locals_map.end(); - it++) - if(is_tracked(it->first)) - loc_infos[0].points_to[pointers.number(it->first)]=flagst::mk_unknown(); + for(const auto &local : locals.locals_map) + if(is_tracked(local.first)) + loc_infos[0].points_to[pointers.number(local.first)]=flagst::mk_unknown(); while(!work_queue.empty()) { @@ -374,13 +371,10 @@ void local_bitvector_analysist::build(const goto_functiont &goto_function) default:; } - for(local_cfgt::successorst::const_iterator - it=node.successors.begin(); - it!=node.successors.end(); - it++) + for(const auto &succ : node.successors) { - if(loc_infos[*it].merge(loc_info_dest)) - work_queue.push(*it); + if(loc_infos[succ].merge(loc_info_dest)) + work_queue.push(succ); } } } diff --git a/src/analyses/local_cfg.cpp b/src/analyses/local_cfg.cpp index 0f70def622b..52f5c6831a4 100644 --- a/src/analyses/local_cfg.cpp +++ b/src/analyses/local_cfg.cpp @@ -60,12 +60,9 @@ void local_cfgt::build(const goto_programt &goto_program) if(!instruction.guard.is_true()) node.successors.push_back(loc_nr+1); - for(goto_programt::targetst::const_iterator - t_it=instruction.targets.begin(); - t_it!=instruction.targets.end(); - t_it++) + for(const auto &target : instruction.targets) { - node_nrt l=loc_map.find(*t_it)->second; + node_nrt l=loc_map.find(target)->second; node.successors.push_back(l); } break; @@ -73,12 +70,9 @@ void local_cfgt::build(const goto_programt &goto_program) case START_THREAD: node.successors.push_back(loc_nr+1); - for(goto_programt::targetst::const_iterator - t_it=instruction.targets.begin(); - t_it!=instruction.targets.end(); - t_it++) + for(const auto &target : instruction.targets) { - node_nrt l=loc_map.find(*t_it)->second; + node_nrt l=loc_map.find(target)->second; node.successors.push_back(l); } break; diff --git a/src/analyses/locals.cpp b/src/analyses/locals.cpp index e9a41949e50..7f30c1c008b 100644 --- a/src/analyses/locals.cpp +++ b/src/analyses/locals.cpp @@ -34,15 +34,9 @@ void localst::build(const goto_functiont &goto_function) to_symbol_expr(code_decl.symbol()); } - const code_typet::parameterst ¶meters= - goto_function.type.parameters(); - - for(code_typet::parameterst::const_iterator - it=parameters.begin(); - it!=parameters.end(); - it++) - locals_map[it->get_identifier()]= - symbol_exprt(it->get_identifier(), it->type()); + for(const auto ¶m : goto_function.type.parameters()) + locals_map[param.get_identifier()]= + symbol_exprt(param.get_identifier(), param.type()); } /*******************************************************************\ @@ -59,9 +53,6 @@ Function: localst::output void localst::output(std::ostream &out) const { - for(locals_mapt::const_iterator - it=locals_map.begin(); - it!=locals_map.end(); - it++) - out << it->first << "\n"; + for(const auto &local : locals_map) + out << local.first << "\n"; } diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h index 2cbfd410375..53d96aaf54d 100644 --- a/src/analyses/natural_loops.h +++ b/src/analyses/natural_loops.h @@ -102,10 +102,9 @@ void natural_loops_templatet::compute(P &program) { if(m_it->is_backwards_goto()) { - for(goto_programt::targetst::const_iterator n_it=m_it->targets.begin(); - n_it!=m_it->targets.end(); ++n_it) + for(const auto &target : m_it->targets) { - if((*n_it)->location_number<=m_it->location_number) + if(target->location_number<=m_it->location_number) { const nodet &node= cfg_dominators.cfg[cfg_dominators.cfg.entry_map[m_it]]; @@ -113,11 +112,11 @@ void natural_loops_templatet::compute(P &program) #ifdef DEBUG std::cout << "Computing loop for " << m_it->location_number << " -> " - << (*n_it)->location_number << "\n"; + << target->location_number << "\n"; #endif - if(node.dominators.find(*n_it)!=node.dominators.end()) + if(node.dominators.find(target)!=node.dominators.end()) { - compute_natural_loop(m_it, *n_it); + compute_natural_loop(m_it, target); } } } @@ -161,12 +160,9 @@ void natural_loops_templatet::compute_natural_loop(T m, T n) const nodet &node= cfg_dominators.cfg[cfg_dominators.cfg.entry_map[p]]; - for(typename nodet::edgest::const_iterator - q_it=node.in.begin(); - q_it!=node.in.end(); - ++q_it) + for(const auto &edge : node.in) { - T q=cfg_dominators.cfg[q_it->first].PC; + T q=cfg_dominators.cfg[edge.first].PC; std::pair result= loop.insert(q); if(result.second) @@ -190,16 +186,15 @@ Function: natural_loops_templatet::output template void natural_loops_templatet::output(std::ostream &out) const { - for(typename loop_mapt::const_iterator h_it=loop_map.begin(); - h_it!=loop_map.end(); ++h_it) + for(const auto &loop : loop_map) { - unsigned n=h_it->first->location_number; + unsigned n=loop.first->location_number; out << n << " is head of { "; - for(typename natural_loopt::const_iterator l_it=h_it->second.begin(); - l_it!=h_it->second.end(); ++l_it) + for(typename natural_loopt::const_iterator l_it=loop.second.begin(); + l_it!=loop.second.end(); ++l_it) { - if(l_it!=h_it->second.begin()) out << ", "; + if(l_it!=loop.second.begin()) out << ", "; out << (*l_it)->location_number; } out << " }\n"; diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index 04809464c70..10c303bcb7d 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -42,12 +42,9 @@ void rd_range_domaint::populate_cache(const irep_idt &identifier) const ranges_at_loct &export_entry=export_cache[identifier]; - for(values_innert::const_iterator - it=v_entry->second.begin(); - it!=v_entry->second.end(); - ++it) + for(const auto &id : v_entry->second) { - const reaching_definitiont &v=bv_container->get(*it); + const reaching_definitiont &v=bv_container->get(id); export_entry[v.definition_at].insert( std::make_pair(v.bit_begin, v.bit_end)); @@ -124,11 +121,8 @@ void rd_range_domaint::transform( (!rd->get_is_threaded()(from) || (!symbol_ptr->is_shared() && !rd->get_is_dirty()(identifier)))) - for(range_domaint::const_iterator - r_it=ranges.begin(); - r_it!=ranges.end(); - ++r_it) - kill(identifier, r_it->first, r_it->second); + for(const auto &range : ranges) + kill(identifier, range.first, range.second); } } } @@ -253,18 +247,15 @@ void rd_range_domaint::transform_function_call( const code_typet &code_type= to_code_type(ns.lookup(fn_symbol_expr.get_identifier()).type); - const code_typet::parameterst ¶meters=code_type.parameters(); - for(code_typet::parameterst::const_iterator it=parameters.begin(); - it!=parameters.end(); - ++it) + for(const auto ¶m : code_type.parameters()) { - const irep_idt &identifier=it->get_identifier(); + const irep_idt &identifier=param.get_identifier(); if(identifier.empty()) continue; range_spect size= - to_range_spect(pointer_offset_bits(it->type(), ns)); + to_range_spect(pointer_offset_bits(param.type(), ns)); gen(from, identifier, 0, size); } } @@ -304,31 +295,22 @@ void rd_range_domaint::transform_end_function( new_values.swap(values); values=rd[call].values; - for(valuest::const_iterator - it=new_values.begin(); - it!=new_values.end(); - ++it) + for(const auto &new_value : new_values) { - const irep_idt &identifier=it->first; + const irep_idt &identifier=new_value.first; if(!rd.get_is_threaded()(call) || (!ns.lookup(identifier).is_shared() && !rd.get_is_dirty()(identifier))) - for(values_innert::const_iterator - i_it=it->second.begin(); - i_it!=it->second.end(); - ++i_it) + for(const auto &id : new_value.second) { - const reaching_definitiont &v=bv_container->get(*i_it); + const reaching_definitiont &v=bv_container->get(id); kill(v.identifier, v.bit_begin, v.bit_end); } - for(values_innert::const_iterator - i_it=it->second.begin(); - i_it!=it->second.end(); - ++i_it) + for(const auto &id : new_value.second) { - const reaching_definitiont &v=bv_container->get(*i_it); + const reaching_definitiont &v=bv_container->get(id); gen(v.definition_at, v.identifier, v.bit_begin, v.bit_end); } } @@ -336,12 +318,9 @@ void rd_range_domaint::transform_end_function( const code_typet &code_type= to_code_type(ns.lookup(from->function).type); - const code_typet::parameterst ¶meters=code_type.parameters(); - for(code_typet::parameterst::const_iterator p_it=parameters.begin(); - p_it!=parameters.end(); - ++p_it) + for(const auto ¶m : code_type.parameters()) { - const irep_idt &identifier=p_it->get_identifier(); + const irep_idt &identifier=param.get_identifier(); if(identifier.empty()) continue; @@ -405,17 +384,11 @@ void rd_range_domaint::transform_assign( (!rd.get_is_threaded()(from) || (!symbol_ptr->is_shared() && !rd.get_is_dirty()(identifier)))) - for(range_domaint::const_iterator - r_it=ranges.begin(); - r_it!=ranges.end(); - ++r_it) - kill(identifier, r_it->first, r_it->second); - - for(range_domaint::const_iterator - r_it=ranges.begin(); - r_it!=ranges.end(); - ++r_it) - gen(from, identifier, r_it->first, r_it->second); + for(const auto &range : ranges) + kill(identifier, range.first, range.second); + + for(const auto &range : ranges) + gen(from, identifier, range.first, range.second); } } @@ -515,20 +488,17 @@ void rd_range_domaint::kill( export_cache.erase(identifier); values_innert::iterator it=entry->second.begin(); - for(values_innert::const_iterator - itn=new_values.begin(); - itn!=new_values.end(); - ++itn) + for(const auto &id : new_values) { - while(it!=entry->second.end() && *it<*itn) + while(it!=entry->second.end() && *itsecond.end() || *itn<*it) + if(it==entry->second.end() || id<*it) { - entry->second.insert(it, *itn); + entry->second.insert(it, id); } else if(it!=entry->second.end()) { - assert(*it==*itn); + assert(*it==id); ++it; } } @@ -686,12 +656,9 @@ void rd_range_domaint::output(std::ostream &out) const return; } - for(valuest::const_iterator - it=values.begin(); - it!=values.end(); - ++it) + for(const auto &value : values) { - const irep_idt &identifier=it->first; + const irep_idt &identifier=value.first; const ranges_at_loct &ranges=get(identifier); @@ -738,25 +705,21 @@ bool rd_range_domaint::merge_inner( #if 0 ranges_at_loct::iterator itr=it->second.begin(); - for(ranges_at_loct::const_iterator itro=ito->second.begin(); - itro!=ito->second.end(); - ++itro) + for(const auto &o : ito->second) { - while(itr!=it->second.end() && itr->firstfirst) + while(itr!=it->second.end() && itr->firstsecond.end() || itro->firstfirst) + if(itr==it->second.end() || o.firstfirst) { - it->second.insert(*itro); + it->second.insert(o); more=true; } else if(itr!=it->second.end()) { - assert(itr->first==itro->first); + assert(itr->first==o.first); - for(rangest::const_iterator itrro=itro->second.begin(); - itrro!=itro->second.end(); - ++itrro) - more=gen(itr->second, itrro->first, itrro->second) || + for(const auto &o_range : o.second) + more=gen(itr->second, o_range.first, o_range.second) || more; ++itr; @@ -764,21 +727,18 @@ bool rd_range_domaint::merge_inner( } #else values_innert::iterator itr=dest.begin(); - for(values_innert::const_iterator - itro=other.begin(); - itro!=other.end(); - ++itro) + for(const auto &id : other) { - while(itr!=dest.end() && *itr<*itro) + while(itr!=dest.end() && *itrfirstfirst) + while(it!=values.end() && it->firstfirstfirst) + if(it==values.end() || value.firstfirst) { - values.insert(*ito); + values.insert(value); changed=true; } else if(it!=values.end()) { - assert(it->first==ito->first); + assert(it->first==value.first); - if(merge_inner(it->second, ito->second)) + if(merge_inner(it->second, value.second)) { changed=true; export_cache.erase(it->first); @@ -865,28 +823,26 @@ bool rd_range_domaint::merge_shared( has_values=tvt::unknown(); valuest::iterator it=values.begin(); - for(valuest::const_iterator ito=other.values.begin(); - ito!=other.values.end(); - ++ito) + for(const auto &value : other.values) { - const irep_idt &identifier=ito->first; + const irep_idt &identifier=value.first; if(!ns.lookup(identifier).is_shared() /*&& !rd.get_is_dirty()(identifier)*/) continue; - while(it!=values.end() && it->firstfirst) + while(it!=values.end() && it->firstfirstfirst) + if(it==values.end() || value.firstfirst) { - values.insert(*ito); + values.insert(value); changed=true; } else if(it!=values.end()) { - assert(it->first==ito->first); + assert(it->first==value.first); - if(merge_inner(it->second, ito->second)) + if(merge_inner(it->second, value.second)) { changed=true; export_cache.erase(it->first); diff --git a/src/analyses/static_analysis.cpp b/src/analyses/static_analysis.cpp index 3737e109ab7..2888ac26ec5 100644 --- a/src/analyses/static_analysis.cpp +++ b/src/analyses/static_analysis.cpp @@ -135,10 +135,7 @@ void static_analysis_baset::output( const goto_functionst &goto_functions, std::ostream &out) const { - for(goto_functionst::function_mapt::const_iterator - f_it=goto_functions.function_map.begin(); - f_it!=goto_functions.function_map.end(); - f_it++) + forall_goto_functions(f_it, goto_functions) { if(f_it->second.body_available()) { @@ -198,10 +195,7 @@ Function: static_analysis_baset::generate_states void static_analysis_baset::generate_states( const goto_functionst &goto_functions) { - for(goto_functionst::function_mapt::const_iterator - f_it=goto_functions.function_map.begin(); - f_it!=goto_functions.function_map.end(); - f_it++) + forall_goto_functions(f_it, goto_functions) generate_states(f_it->second.body); } @@ -239,10 +233,7 @@ Function: static_analysis_baset::update void static_analysis_baset::update( const goto_functionst &goto_functions) { - for(goto_functionst::function_mapt::const_iterator - f_it=goto_functions.function_map.begin(); - f_it!=goto_functions.function_map.end(); - f_it++) + forall_goto_functions(f_it, goto_functions) update(f_it->second.body); } @@ -370,13 +361,8 @@ bool static_analysis_baset::visit( goto_program.get_successors(l, successors); - for(goto_programt::const_targetst::const_iterator - it=successors.begin(); - it!=successors.end(); - it++) + for(const auto &to_l : successors) { - locationt to_l=*it; - if(to_l==goto_program.instructions.end()) continue; @@ -581,13 +567,11 @@ void static_analysis_baset::do_function_call_rec( std::unique_ptr state_from(make_temporary_state(new_state)); // now call all of these - for(std::list::const_iterator it=values.begin(); - it!=values.end(); - it++) + for(const auto &value : values) { - if(it->id()==ID_object_descriptor) + if(value.id()==ID_object_descriptor) { - const object_descriptor_exprt &o=to_object_descriptor_expr(*it); + const object_descriptor_exprt &o=to_object_descriptor_expr(value); std::unique_ptr n2(make_temporary_state(new_state)); do_function_call_rec(l_call, l_return, o.object(), arguments, *n2, goto_functions); merge(new_state, *n2, l_return); @@ -690,21 +674,19 @@ void static_analysis_baset::concurrent_fixedpoint( { new_shared=false; - for(thread_wlt::const_iterator it=thread_wl.begin(); - it!=thread_wl.end(); - ++it) + for(const auto &thread : thread_wl) { working_sett working_set; - put_in_working_set(working_set, it->second); + put_in_working_set(working_set, thread.second); - statet &begin_state=get_state(it->second); - merge(begin_state, shared_state, it->second); + statet &begin_state=get_state(thread.second); + merge(begin_state, shared_state, thread.second); while(!working_set.empty()) { goto_programt::const_targett l=get_next(working_set); - visit(l, working_set, *(it->first), goto_functions); + visit(l, working_set, *thread.first, goto_functions); // the underlying domain must make sure that the final state // carries all possible values; otherwise we would need to diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp index 36640250fa8..c671722843f 100644 --- a/src/analyses/uninitialized_domain.cpp +++ b/src/analyses/uninitialized_domain.cpp @@ -102,7 +102,7 @@ void uninitialized_domaint::output( out << has_values.to_string() << '\n'; else { - for(const auto & id : uninitialized) + for(const auto &id : uninitialized) out << id << '\n'; } } diff --git a/src/ansi-c/anonymous_member.cpp b/src/ansi-c/anonymous_member.cpp index 9aa1d2317b9..22f6d18b6e9 100644 --- a/src/ansi-c/anonymous_member.cpp +++ b/src/ansi-c/anonymous_member.cpp @@ -69,21 +69,18 @@ exprt get_component_rec( const struct_union_typet::componentst &components= struct_union_type.components(); - for(struct_union_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - it++) + for(const auto &comp : components) { - const typet &type=ns.follow(it->type()); + const typet &type=ns.follow(comp.type()); - if(it->get_name()==component_name) + if(comp.get_name()==component_name) { - return make_member_expr(struct_union, *it, ns); + return make_member_expr(struct_union, comp, ns); } - else if(it->get_anonymous() && + else if(comp.get_anonymous() && (type.id()==ID_struct || type.id()==ID_union)) { - exprt tmp=make_member_expr(struct_union, *it, ns); + exprt tmp=make_member_expr(struct_union, comp, ns); exprt result=get_component_rec(tmp, component_name, ns); if(result.is_not_nil()) return result; } @@ -115,18 +112,15 @@ bool has_component_rec( const struct_union_typet::componentst &components= struct_union_type.components(); - for(struct_union_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - it++) + for(const auto &comp : components) { - if(it->get_name()==component_name) + if(comp.get_name()==component_name) { return true; } - else if(it->get_anonymous()) + else if(comp.get_anonymous()) { - if(has_component_rec(it->type(), component_name, ns)) + if(has_component_rec(comp.type(), component_name, ns)) return true; } } diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp index f9dea43c02b..e8b57805c34 100644 --- a/src/ansi-c/ansi_c_declaration.cpp +++ b/src/ansi-c/ansi_c_declaration.cpp @@ -96,10 +96,8 @@ void ansi_c_declarationt::output(std::ostream &out) const out << "Type: " << type().pretty() << "\n"; - for(declaratorst::const_iterator d_it=declarators().begin(); - d_it!=declarators().end(); - d_it++) - out << "Declarator: " << d_it->pretty() << "\n"; + for(const auto &declarator : declarators()) + out << "Declarator: " << declarator.pretty() << "\n"; } /*******************************************************************\ diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 8b4cd4963c4..bfad11ded10 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -48,7 +48,7 @@ exprt::operandst build_function_environment( std::size_t i=0; - for(const auto & p : parameters) + for(const auto &p : parameters) { irep_idt base_name=p.get_base_name().empty()? ("argument#"+std::to_string(i)):p.get_base_name(); @@ -132,7 +132,7 @@ void record_function_outputs( #if 0 std::size_t i=0; - for(const auto & p : parameters) + for(const auto &p : parameters) { if(p.get_identifier().empty()) continue; diff --git a/src/ansi-c/ansi_c_parse_tree.cpp b/src/ansi-c/ansi_c_parse_tree.cpp index ae554a6dd0f..4f58d094563 100644 --- a/src/ansi-c/ansi_c_parse_tree.cpp +++ b/src/ansi-c/ansi_c_parse_tree.cpp @@ -58,12 +58,9 @@ Function: ansi_c_parse_treet::output void ansi_c_parse_treet::output(std::ostream &out) const { - for(itemst::const_iterator - it=items.begin(); - it!=items.end(); - it++) + for(const auto &item : items) { - it->output(out); + item.output(out); out << "\n"; } } diff --git a/src/ansi-c/ansi_c_scope.cpp b/src/ansi-c/ansi_c_scope.cpp index 8c2bcc4e589..761fd23b19b 100644 --- a/src/ansi-c/ansi_c_scope.cpp +++ b/src/ansi-c/ansi_c_scope.cpp @@ -26,13 +26,10 @@ void ansi_c_scopet::print(std::ostream &out) const { out << "Prefix: " << prefix << "\n"; - for(ansi_c_scopet::name_mapt::const_iterator - n_it=name_map.begin(); - n_it!=name_map.end(); - n_it++) + for(const auto &name : name_map) { - out << " ID: " << n_it->first - << " CLASS: " << n_it->second.id_class + out << " ID: " << name.first + << " CLASS: " << name.second.id_class << "\n"; } } diff --git a/src/ansi-c/c_misc.cpp b/src/ansi-c/c_misc.cpp index 80d63e75717..94baea10fa2 100644 --- a/src/ansi-c/c_misc.cpp +++ b/src/ansi-c/c_misc.cpp @@ -138,7 +138,7 @@ std::string MetaString(const std::string &in) { std::string result; - for(const auto & ch : in) + for(const auto &ch : in) MetaChar(result, ch, true); return result; diff --git a/src/ansi-c/c_preprocess.cpp b/src/ansi-c/c_preprocess.cpp index 4ac553d91e4..50b412ea5b5 100644 --- a/src/ansi-c/c_preprocess.cpp +++ b/src/ansi-c/c_preprocess.cpp @@ -155,9 +155,8 @@ static std::string shell_quote(const std::string &src) result+='"'; - for(unsigned i=0; i::const_iterator - it=config.ansi_c.defines.begin(); - it!=config.ansi_c.defines.end(); - it++) - command_file << "/D" << shell_quote(*it) << "\n"; + for(const auto &define : config.ansi_c.defines) + command_file << "/D" << shell_quote(define) << "\n"; - for(std::list::const_iterator - it=config.ansi_c.include_paths.begin(); - it!=config.ansi_c.include_paths.end(); - it++) - command_file << "/I" << shell_quote(*it) << "\n"; + for(const auto &include_path : config.ansi_c.include_paths) + command_file << "/I" << shell_quote(include_path) << "\n"; - for(std::list::const_iterator - it=config.ansi_c.include_files.begin(); - it!=config.ansi_c.include_files.end(); - it++) - command_file << "/FI" << shell_quote(*it) << "\n"; + for(const auto &include_file : config.ansi_c.include_files) + command_file << "/FI" << shell_quote(include_file) << "\n"; // Finally, the file to be preprocessed // (this is already in UTF-8). @@ -670,29 +659,17 @@ bool c_preprocess_codewarrior( command="mwcceppc -E -P -D__CPROVER__ -ppopt line -ppopt full"; - for(std::list::const_iterator - it=config.ansi_c.defines.begin(); - it!=config.ansi_c.defines.end(); - it++) - command+=" -D"+shell_quote(*it); - - for(std::list::const_iterator - it=config.ansi_c.include_paths.begin(); - it!=config.ansi_c.include_paths.end(); - it++) - command+=" -I"+shell_quote(*it); - - for(std::list::const_iterator - it=config.ansi_c.include_files.begin(); - it!=config.ansi_c.include_files.end(); - it++) - command+=" -include "+shell_quote(*it); - - for(std::list::const_iterator - it=config.ansi_c.preprocessor_options.begin(); - it!=config.ansi_c.preprocessor_options.end(); - it++) - command+=" "+*it; + for(const auto &define : config.ansi_c.defines) + command+=" -D"+shell_quote(define); + + for(const auto &include_path : config.ansi_c.include_paths) + command+=" -I"+shell_quote(include_path); + + for(const auto &include_file : config.ansi_c.include_files) + command+=" -include "+shell_quote(include_file); + + for(const auto &opt : config.ansi_c.preprocessor_options) + command+=" "+opt; int result; @@ -955,29 +932,17 @@ bool c_preprocess_gcc_clang( command += " -D __STDC_IEC_559_COMPLEX__=1"; command += " -D __STDC_ISO_10646__=1"; - for(std::list::const_iterator - it=config.ansi_c.defines.begin(); - it!=config.ansi_c.defines.end(); - it++) - command+=" -D"+shell_quote(*it); - - for(std::list::const_iterator - it=config.ansi_c.include_paths.begin(); - it!=config.ansi_c.include_paths.end(); - it++) - command+=" -I"+shell_quote(*it); - - for(std::list::const_iterator - it=config.ansi_c.include_files.begin(); - it!=config.ansi_c.include_files.end(); - it++) - command+=" -include "+shell_quote(*it); - - for(std::list::const_iterator - it=config.ansi_c.preprocessor_options.begin(); - it!=config.ansi_c.preprocessor_options.end(); - it++) - command+=" "+*it; + for(const auto &define : config.ansi_c.defines) + command+=" -D"+shell_quote(define); + + for(const auto &include_path : config.ansi_c.include_paths) + command+=" -I"+shell_quote(include_path); + + for(const auto &include_file : config.ansi_c.include_files) + command+=" -include "+shell_quote(include_file); + + for(const auto &opt : config.ansi_c.preprocessor_options) + command+=" "+opt; int result; @@ -1121,17 +1086,11 @@ bool c_preprocess_arm( command+=" -D__STDC__"; //command+=" -D__STDC_VERSION__=199901L"; - for(std::list::const_iterator - it=config.ansi_c.defines.begin(); - it!=config.ansi_c.defines.end(); - it++) - command+=" "+shell_quote("-D"+*it); - - for(std::list::const_iterator - it=config.ansi_c.include_paths.begin(); - it!=config.ansi_c.include_paths.end(); - it++) - command+=" "+shell_quote("-I"+*it); + for(const auto &define : config.ansi_c.defines) + command+=" "+shell_quote("-D"+define); + + for(const auto &include_path : config.ansi_c.include_paths) + command+=" "+shell_quote("-I"+include_path); int result; diff --git a/src/ansi-c/c_sizeof.cpp b/src/ansi-c/c_sizeof.cpp index 4de0d9dd22b..8a9bc21c713 100644 --- a/src/ansi-c/c_sizeof.cpp +++ b/src/ansi-c/c_sizeof.cpp @@ -122,14 +122,11 @@ exprt c_sizeoft::sizeof_rec(const typet &type) mp_integer bit_field_width=0; - for(struct_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - it++) + for(const auto &comp : components) { - const typet &sub_type=ns.follow(it->type()); + const typet &sub_type=ns.follow(comp.type()); - if(it->get_bool(ID_is_type)) + if(comp.get_bool(ID_is_type)) { } else if(sub_type.id()==ID_code) @@ -163,15 +160,12 @@ exprt c_sizeoft::sizeof_rec(const typet &type) const union_typet::componentst &components= to_union_type(type).components(); - for(union_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - it++) + for(const auto &comp : components) { - if(it->get_bool(ID_is_type) || it->type().id()==ID_code) + if(comp.get_bool(ID_is_type) || comp.type().id()==ID_code) continue; - const typet &sub_type=it->type(); + const typet &sub_type=comp.type(); exprt tmp; @@ -285,12 +279,9 @@ exprt c_sizeoft::c_offsetof( mp_integer bit_field_width=0; - for(struct_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - it++) + for(const auto &comp : components) { - if(it->get_name()==component_name) + if(comp.get_name()==component_name) { // done if(bit_field_width!=0) @@ -298,10 +289,10 @@ exprt c_sizeoft::c_offsetof( return dest; } - if(it->get_bool(ID_is_type)) + if(comp.get_bool(ID_is_type)) continue; - const typet &sub_type=ns.follow(it->type()); + const typet &sub_type=ns.follow(comp.type()); if(sub_type.id()==ID_code) { diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp index 43bbbc7c7bb..3cf2a9684ef 100644 --- a/src/ansi-c/c_typecast.cpp +++ b/src/ansi-c/c_typecast.cpp @@ -609,21 +609,16 @@ void c_typecastt::implicit_typecast_followed( src_type_no_const.subtype().remove(ID_C_constant); // Check union members. - const union_typet &dest_union_type=to_union_type(dest_type); - - for(union_typet::componentst::const_iterator - it=dest_union_type.components().begin(); - it!=dest_union_type.components().end(); - it++) + for(const auto &comp : to_union_type(dest_type).components()) { - if(!check_c_implicit_typecast(src_type_no_const, it->type())) + if(!check_c_implicit_typecast(src_type_no_const, comp.type())) { // build union constructor exprt union_expr(ID_union, orig_dest_type); union_expr.move_to_operands(expr); if(!full_eq(src_type, src_type_no_const)) do_typecast(union_expr.op0(), src_type_no_const); - union_expr.set(ID_component_name, it->get_name()); + union_expr.set(ID_component_name, comp.get_name()); expr=union_expr; return; // ok } diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 1748d5eba40..abe2b49a1d1 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -73,7 +73,7 @@ Function: c_typecheck_baset::add_rounding_mode void c_typecheck_baset::add_rounding_mode(exprt &expr) { - for(auto & op : expr.operands()) + for(auto &op : expr.operands()) add_rounding_mode(op); if(expr.id()==ID_div || diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index dcfb2ea5ccf..879fbc34efc 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -393,15 +393,13 @@ void c_typecheck_baset::typecheck_code_type(code_typet &type) parameter_map.clear(); - for(code_typet::parameterst::iterator - p_it=type.parameters().begin(); - p_it!=type.parameters().end(); - p_it++) + for(auto ¶m : type.parameters()) { // turn the declarations into parameters - if(p_it->id()==ID_declaration) + if(param.id()==ID_declaration) { - ansi_c_declarationt &declaration=to_ansi_c_declaration(*p_it); + ansi_c_declarationt &declaration= + to_ansi_c_declaration(param); code_typet::parametert parameter; @@ -432,7 +430,7 @@ void c_typecheck_baset::typecheck_code_type(code_typet &type) } // put the parameter in place of the declaration - p_it->swap(parameter); + param.swap(parameter); } } @@ -846,16 +844,13 @@ void c_typecheck_baset::typecheck_compound_body( old_components.swap(components); // We get these as declarations! - for(struct_union_typet::componentst::iterator - it=old_components.begin(); - it!=old_components.end(); - it++) + for(auto &decl : old_components) { // the arguments are member declarations or static assertions - assert(it->id()==ID_declaration); + assert(decl.id()==ID_declaration); ansi_c_declarationt &declaration= - to_ansi_c_declaration(static_cast(*it)); + to_ansi_c_declaration(static_cast(decl)); if(declaration.get_is_static_assert()) { @@ -872,17 +867,15 @@ void c_typecheck_baset::typecheck_compound_body( typecheck_type(declaration.type()); make_already_typechecked(declaration.type()); - for(ansi_c_declarationt::declaratorst::iterator - d_it=declaration.declarators().begin(); - d_it!=declaration.declarators().end(); - d_it++) + for(const auto &declarator : declaration.declarators()) { struct_union_typet::componentt new_component; - new_component.add_source_location()=d_it->source_location(); - new_component.set(ID_name, d_it->get_base_name()); - new_component.set(ID_pretty_name, d_it->get_base_name()); - new_component.type()=declaration.full_type(*d_it); + new_component.add_source_location()= + declarator.source_location(); + new_component.set(ID_name, declarator.get_base_name()); + new_component.set(ID_pretty_name, declarator.get_base_name()); + new_component.type()=declaration.full_type(declarator); typecheck_type(new_component.type()); @@ -903,15 +896,12 @@ void c_typecheck_baset::typecheck_compound_body( unsigned anon_member_counter=0; // scan for anonymous members, and name them - for(struct_union_typet::componentst::iterator - it=components.begin(); - it!=components.end(); - it++) + for(auto &member : components) { - if(it->get_name()!=irep_idt()) continue; + if(member.get_name()!=irep_idt()) continue; - it->set_name("$anon"+std::to_string(anon_member_counter++)); - it->set_anonymous(true); + member.set_name("$anon"+std::to_string(anon_member_counter++)); + member.set_anonymous(true); } // scan for duplicate members @@ -926,7 +916,9 @@ void c_typecheck_baset::typecheck_compound_body( { if(!members.insert(it->get_name()).second) { - // we do nothing (as gcc won't complain) + error().source_location=it->source_location(); + error() << "duplicate member " << it->get_name() << eom; + throw 0; } } } @@ -1173,9 +1165,9 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type) // if the type is marked as 'packed'. // gcc/clang may also pick a larger width. Visual Studio doesn't. - for(auto & it : as_expr.operands()) + for(auto &op : as_expr.operands()) { - ansi_c_declarationt &declaration=to_ansi_c_declaration(it); + ansi_c_declarationt &declaration=to_ansi_c_declaration(op); exprt &v=declaration.declarator().value(); if(v.is_not_nil()) // value given? @@ -1239,15 +1231,12 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type) // None, it's anonymous. We generate a tag. std::string anon_identifier="#anon_enum"; - for(std::list::const_iterator - it=enum_members.begin(); - it!=enum_members.end(); - it++) + for(const auto &member : enum_members) { anon_identifier+='$'; - anon_identifier+=id2string(it->get_base_name()); + anon_identifier+=id2string(member.get_base_name()); anon_identifier+='='; - anon_identifier+=id2string(it->get_value()); + anon_identifier+=id2string(member.get_value()); } if(is_packed) @@ -1273,11 +1262,8 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type) // throw in the enum members as 'body' irept::subt &body=enum_tag_symbol.type.add(ID_body).get_sub(); - for(std::list::const_iterator - it=enum_members.begin(); - it!=enum_members.end(); - it++) - body.push_back(*it); + for(const auto &member : enum_members) + body.push_back(member); // We use a subtype to store the underlying type. typet underlying_type= diff --git a/src/ansi-c/parser_static.inc b/src/ansi-c/parser_static.inc index 08a81c93e0d..791c91fc6b7 100644 --- a/src/ansi-c/parser_static.inc +++ b/src/ansi-c/parser_static.inc @@ -350,11 +350,11 @@ static void create_function_scope(const YYSTYPE d) code_typet::parameterst ¶meters=code_type.parameters(); // Add the parameter declarations to the scope. - for(auto & it : parameters) + for(auto ¶m : parameters) { - if(it.id()==ID_declaration) + if(param.id()==ID_declaration) { - ansi_c_declarationt ¶m_decl=to_ansi_c_declaration(it); + ansi_c_declarationt ¶m_decl=to_ansi_c_declaration(param); // we record the function name in the location param_decl.add_source_location().set_function(function_name); @@ -403,9 +403,9 @@ static void adjust_KnR_parameters( ansi_c_declarationt::declaratorst &declarators= declaration.declarators(); - for(const auto & it : declarators) + for(const auto &decl : declarators) { - irep_idt base_name=it.get_base_name(); + irep_idt base_name=decl.get_base_name(); // we just do a linear search over the parameters // this could be improved with a hash map @@ -420,7 +420,7 @@ static void adjust_KnR_parameters( // This copies the declaration type, which can be a // problem if there are compound bodies in there. p_decl.type()=declaration.type(); - p_decl.declarator().type()=it.type(); + p_decl.declarator().type()=decl.type(); break; } } diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index 9ef6cb53dfa..628ac884c75 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -125,7 +125,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()() cover_goals.set_message_handler(get_message_handler()); cover_goals.register_observer(*this); - for(const auto & g : goal_map) + for(const auto &g : goal_map) { // Our goal is to falsify a property, i.e., we will // add the negation of the property as goal. @@ -142,13 +142,13 @@ safety_checkert::resultt bmc_all_propertiest::operator()() if(result==decision_proceduret::D_ERROR) { error=true; - for(auto & g : goal_map) + for(auto &g : goal_map) if(g.second.status==goalt::statust::UNKNOWN) g.second.status=goalt::statust::ERROR; } else { - for(auto & g : goal_map) + for(auto &g : goal_map) if(g.second.status==goalt::statust::UNKNOWN) g.second.status=goalt::statust::SUCCESS; } @@ -197,17 +197,18 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals) { status() << "\n** Results:" << eom; - for(const auto & it : goal_map) - status() << "[" << it.first << "] " - << it.second.description << ": " << it.second.status_string() + for(const auto &goal_pair : goal_map) + status() << "[" << goal_pair.first << "] " + << goal_pair.second.description << ": " + << goal_pair.second.status_string() << eom; if(bmc.options.get_bool_option("trace")) - for(const auto & it : goal_map) - if(it.second.status==goalt::statust::FAILURE) + for(const auto &g : goal_map) + if(g.second.status==goalt::statust::FAILURE) { - std::cout << "\n" << "Trace for " << it.first << ":" << "\n"; - show_goto_trace(std::cout, bmc.ns, it.second.goto_trace); + std::cout << "\n" << "Trace for " << g.first << ":" << "\n"; + show_goto_trace(std::cout, bmc.ns, g.second.goto_trace); } status() << "\n** " << cover_goals.number_covered() @@ -220,14 +221,14 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals) case ui_message_handlert::XML_UI: { - for(const auto & it : goal_map) + for(const auto &g : goal_map) { xmlt xml_result("result"); - xml_result.set_attribute("property", id2string(it.first)); - xml_result.set_attribute("status", it.second.status_string()); + xml_result.set_attribute("property", id2string(g.first)); + xml_result.set_attribute("status", g.second.status_string()); - if(it.second.status==goalt::statust::FAILURE) - convert(bmc.ns, it.second.goto_trace, xml_result.new_element()); + if(g.second.status==goalt::statust::FAILURE) + convert(bmc.ns, g.second.goto_trace, xml_result.new_element()); std::cout << xml_result << "\n"; } @@ -239,17 +240,17 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals) json_objectt json_result; json_arrayt &result_array=json_result["result"].make_array(); - for(const auto & it : goal_map) + for(const auto &g : goal_map) { json_objectt &result=result_array.push_back().make_object(); - result["property"]=json_stringt(id2string(it.first)); - result["description"]=json_stringt(id2string(it.second.description)); - result["status"]=json_stringt(it.second.status_string()); + result["property"]=json_stringt(id2string(g.first)); + result["description"]=json_stringt(id2string(g.second.description)); + result["status"]=json_stringt(g.second.status_string()); - if(it.second.status==goalt::statust::FAILURE) + if(g.second.status==goalt::statust::FAILURE) { jsont &json_trace=result["trace"]; - convert(bmc.ns, it.second.goto_trace, json_trace); + convert(bmc.ns, g.second.goto_trace, json_trace); } } diff --git a/src/cbmc/all_properties_class.h b/src/cbmc/all_properties_class.h index ff3240d9e29..837c3a39966 100644 --- a/src/cbmc/all_properties_class.h +++ b/src/cbmc/all_properties_class.h @@ -82,11 +82,9 @@ class bmc_all_propertiest: exprt as_expr() const { std::vector tmp; - for(instancest::const_iterator - it=instances.begin(); - it!=instances.end(); - it++) - tmp.push_back(literal_exprt((*it)->cond_literal)); + tmp.reserve(instances.size()); + for(const auto &inst : instances) + tmp.push_back(literal_exprt(inst->cond_literal)); return conjunction(tmp); } }; diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 9a566cfdeb8..f3b3c43b375 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -669,7 +669,7 @@ void bmct::setup_unwind() std::vector unwindset_loops; split_string(set, ',', unwindset_loops, true, true); - for(auto & val : unwindset_loops) + for(auto &val : unwindset_loops) { unsigned thread_nr; bool thread_nr_set=false; diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index df33aac8673..817f55c1b86 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -98,8 +98,8 @@ class bmc_covert: { std::vector tmp; - for(const auto &it : instances) - tmp.push_back(literal_exprt(it.condition)); + for(const auto &goal_inst : instances) + tmp.push_back(literal_exprt(goal_inst.condition)); return disjunction(tmp); } @@ -125,7 +125,7 @@ class bmc_covert: { bool first=true; std::string test; - for(const auto & step : goto_trace.steps) + for(const auto &step : goto_trace.steps) { if(step.is_input()) { @@ -166,23 +166,23 @@ void bmc_covert::satisfying_assignment() tests.push_back(testt()); testt &test = tests.back(); - for(auto &g_it : goal_map) + for(auto &goal_pair : goal_map) { - goalt &g=g_it.second; + goalt &g=goal_pair.second; // covered already? if(g.satisfied) continue; // check whether satisfied - for(const auto &c_it : g.instances) + for(const auto &goal_inst : g.instances) { - literalt cond=c_it.condition; + literalt cond=goal_inst.condition; if(solver.l_get(cond).is_true()) { status() << "Covered " << g.description << messaget::eom; g.satisfied=true; - test.covered_goals.push_back(g_it.first); + test.covered_goals.push_back(goal_pair.first); break; } } @@ -250,8 +250,8 @@ bool bmc_covert::operator()() } } - for(auto & it : bmc.equation.SSA_steps) - it.cond_literal=literalt(0, 0); + for(auto &step : bmc.equation.SSA_steps) + step.cond_literal=literalt(0, 0); // Do conversion to next solver layer @@ -283,9 +283,9 @@ bool bmc_covert::operator()() cover_goals.register_observer(*this); - for(const auto &it : goal_map) + for(const auto &g : goal_map) { - literalt l=solver.convert(it.second.as_expr()); + literalt l=solver.convert(g.second.as_expr()); cover_goals.add(l); } @@ -306,8 +306,8 @@ bool bmc_covert::operator()() // report unsigned goals_covered=0; - for(const auto & it : goal_map) - if(it.second.satisfied) goals_covered++; + for(const auto &g : goal_map) + if(g.second.satisfied) goals_covered++; switch(bmc.ui) { @@ -315,11 +315,11 @@ bool bmc_covert::operator()() { status() << "\n** coverage results:" << eom; - for(const auto & it : goal_map) + for(const auto &g : goal_map) { - const goalt &goal=it.second; + const goalt &goal=g.second; - status() << "[" << it.first << "]"; + status() << "[" << g.first << "]"; if(goal.source_location.is_not_nil()) status() << ' ' << goal.source_location; @@ -337,12 +337,12 @@ bool bmc_covert::operator()() case ui_message_handlert::XML_UI: { - for(const auto & it : goal_map) + for(const auto &goal_pair : goal_map) { - const goalt &goal=it.second; + const goalt &goal=goal_pair.second; xmlt xml_result("goal"); - xml_result.set_attribute("id", id2string(it.first)); + xml_result.set_attribute("id", id2string(goal_pair.first)); xml_result.set_attribute("description", goal.description); xml_result.set_attribute("status", goal.satisfied?"SATISFIED":"FAILED"); @@ -352,7 +352,7 @@ bool bmc_covert::operator()() std::cout << xml_result << "\n"; } - for(const auto & test : tests) + for(const auto &test : tests) { xmlt xml_result("test"); if(bmc.options.get_bool_option("trace")) @@ -363,7 +363,7 @@ bool bmc_covert::operator()() { xmlt &xml_test=xml_result.new_element("inputs"); - for(const auto & step : test.goto_trace.steps) + for(const auto &step : test.goto_trace.steps) { if(step.is_input()) { @@ -376,7 +376,7 @@ bool bmc_covert::operator()() } } - for(const auto & goal_id : test.covered_goals) + for(const auto &goal_id : test.covered_goals) { xmlt &xml_goal=xml_result.new_element("goal"); xml_goal.set_attribute("id", id2string(goal_id)); @@ -391,13 +391,13 @@ bool bmc_covert::operator()() { json_objectt json_result; json_arrayt &goals_array=json_result["goals"].make_array(); - for(const auto & it : goal_map) + for(const auto &goal_pair : goal_map) { - const goalt &goal=it.second; + const goalt &goal=goal_pair.second; json_objectt &result=goals_array.push_back().make_object(); result["status"]=json_stringt(goal.satisfied?"satisfied":"failed"); - result["goal"]=json_stringt(id2string(it.first)); + result["goal"]=json_stringt(id2string(goal_pair.first)); result["description"]=json_stringt(goal.description); if(goal.source_location.is_not_nil()) @@ -407,7 +407,7 @@ bool bmc_covert::operator()() json_result["goalsCovered"]=json_numbert(std::to_string(goals_covered)); json_arrayt &tests_array=json_result["tests"].make_array(); - for(const auto & test : tests) + for(const auto &test : tests) { json_objectt &result=tests_array.push_back().make_object(); if(bmc.options.get_bool_option("trace")) @@ -419,7 +419,7 @@ bool bmc_covert::operator()() { json_arrayt &json_test=result["inputs"].make_array(); - for(const auto & step : test.goto_trace.steps) + for(const auto &step : test.goto_trace.steps) { if(step.is_input()) { @@ -432,7 +432,7 @@ bool bmc_covert::operator()() } } json_arrayt &goal_refs=result["coveredGoals"].make_array(); - for(const auto & goal_id : test.covered_goals) + for(const auto &goal_id : test.covered_goals) { goal_refs.push_back(json_stringt(id2string(goal_id))); } @@ -457,7 +457,7 @@ bool bmc_covert::operator()() { std::cout << "Test suite:" << '\n'; - for(const auto & test : tests) + for(const auto &test : tests) std::cout << get_test(test.goto_trace) << '\n'; } diff --git a/src/cbmc/cbmc_dimacs.cpp b/src/cbmc/cbmc_dimacs.cpp index e411e733138..8cbcd015287 100644 --- a/src/cbmc/cbmc_dimacs.cpp +++ b/src/cbmc/cbmc_dimacs.cpp @@ -58,40 +58,32 @@ bool cbmc_dimacst::write_dimacs(std::ostream &out) dynamic_cast(prop).write_dimacs_cnf(out); // we dump the mapping variable<->literals - for(bv_cbmct::symbolst::const_iterator - s_it=get_symbols().begin(); - s_it!=get_symbols().end(); - s_it++) + for(const auto &s : get_symbols()) { - if(s_it->second.is_constant()) - out << "c " << s_it->first << " " - << (s_it->second.is_true()?"TRUE":"FALSE") << "\n"; + if(s.second.is_constant()) + out << "c " << s.first << " " + << (s.second.is_true()?"TRUE":"FALSE") << "\n"; else - out << "c " << s_it->first << " " - << s_it->second.dimacs() << "\n"; + out << "c " << s.first << " " + << s.second.dimacs() << "\n"; } // dump mapping for selected bit-vectors - const boolbv_mapt &boolbv_map=get_map(); - - for(boolbv_mapt::mappingt::const_iterator - m_it=boolbv_map.mapping.begin(); - m_it!=boolbv_map.mapping.end(); - m_it++) + for(const auto &m : get_map().mapping) { - const boolbv_mapt::literal_mapt &literal_map=m_it->second.literal_map; + const boolbv_mapt::literal_mapt &literal_map=m.second.literal_map; if(literal_map.empty()) continue; - out << "c " << m_it->first; + out << "c " << m.first; - for(unsigned i=0; i criteria; - for(const auto & criterion_string : criteria_strings) + for(const auto &criterion_string : criteria_strings) { coverage_criteriont c; @@ -967,7 +964,7 @@ bool cbmc_parse_optionst::process_goto_program( status() << "Instrumenting coverage goals" << eom; - for(const auto & criterion : criteria) + for(const auto &criterion : criteria) instrument_cover_goals(symbol_table, goto_functions, criterion); goto_functions.update(); diff --git a/src/cbmc/counterexample_beautification.cpp b/src/cbmc/counterexample_beautification.cpp index fe86e313f58..8475f122040 100644 --- a/src/cbmc/counterexample_beautification.cpp +++ b/src/cbmc/counterexample_beautification.cpp @@ -152,11 +152,8 @@ void counterexample_beautificationt::operator()( prop_minimizet prop_minimize(bv_cbmc); prop_minimize.set_message_handler(bv_cbmc.get_message_handler()); - for(guard_countt::const_iterator - it=guard_count.begin(); - it!=guard_count.end(); - it++) - prop_minimize.objective(it->first, it->second); + for(const auto &g : guard_count) + prop_minimize.objective(g.first, g.second); // minimize prop_minimize(); diff --git a/src/cbmc/xml_interface.cpp b/src/cbmc/xml_interface.cpp index 45c1d231caa..d94fa7bf034 100644 --- a/src/cbmc/xml_interface.cpp +++ b/src/cbmc/xml_interface.cpp @@ -57,13 +57,10 @@ void xml_interfacet::get_xml_options( const xmlt &xml, cmdlinet &cmdline) { - for(xmlt::elementst::const_iterator - e_it=xml.elements.begin(); - e_it!=xml.elements.end(); - e_it++) + for(const auto &e : xml.elements) { // recursive call - get_xml_options(*e_it, cmdline); + get_xml_options(e, cmdline); } if(xml.name=="valueOption") diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index ab94bc84cfb..4ed417014cd 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -511,19 +511,16 @@ Function: clobber_parse_optionst::report_properties void clobber_parse_optionst::report_properties( const path_searcht::property_mapt &property_map) { - for(path_searcht::property_mapt::const_iterator - it=property_map.begin(); - it!=property_map.end(); - it++) + for(const auto &prop_pair : property_map) { if(get_ui()==ui_message_handlert::XML_UI) { xmlt xml_result("result"); - xml_result.set_attribute("claim", id2string(it->first)); + xml_result.set_attribute("claim", id2string(prop_pair.first)); std::string status_string; - switch(it->second.status) + switch(prop_pair.second.status) { case path_searcht::PASS: status_string="OK"; break; case path_searcht::FAIL: status_string="FAILURE"; break; @@ -536,9 +533,9 @@ void clobber_parse_optionst::report_properties( } else { - status() << "[" << it->first << "] " - << it->second.description << ": "; - switch(it->second.status) + status() << "[" << prop_pair.first << "] " + << prop_pair.second.description << ": "; + switch(prop_pair.second.status) { case path_searcht::PASS: status() << "OK"; break; case path_searcht::FAIL: status() << "FAILED"; break; @@ -548,8 +545,8 @@ void clobber_parse_optionst::report_properties( } if(cmdline.isset("show-trace") && - it->second.status==path_searcht::FAIL) - show_counterexample(it->second.error_trace); + prop_pair.second.status==path_searcht::FAIL) + show_counterexample(prop_pair.second.error_trace); } if(!cmdline.isset("property")) @@ -558,11 +555,8 @@ void clobber_parse_optionst::report_properties( unsigned failed=0; - for(path_searcht::property_mapt::const_iterator - it=property_map.begin(); - it!=property_map.end(); - it++) - if(it->second.status==path_searcht::FAIL) + for(const auto &prop_pair : property_map) + if(prop_pair.second.status==path_searcht::FAIL) failed++; status() << "** " << failed diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 951a72e758d..3a2adda985f 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -70,7 +70,7 @@ void cpp_typecheckt::typecheck() // default linkage is "automatic" current_linkage_spec=ID_auto; - for(auto & item : cpp_parse_tree.items) + for(auto &item : cpp_parse_tree.items) convert(item); static_and_dynamic_initialization(); @@ -238,7 +238,7 @@ void cpp_typecheckt::static_and_dynamic_initialization() disable_access_control = true; - for(const auto & d_it : dynamic_initializations) + for(const auto &d_it : dynamic_initializations) { symbolt &symbol=symbol_table.symbols.find(d_it)->second; @@ -411,7 +411,7 @@ void cpp_typecheckt::clean_up() function_members.reserve(components.size()); - for(const auto & compo_it : components) + for(const auto &compo_it : components) { if(compo_it.get_bool(ID_is_static) || compo_it.get_bool(ID_is_type)) diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp index 50822b74788..05f5491dc9a 100644 --- a/src/cpp/cpp_typecheck_code.cpp +++ b/src/cpp/cpp_typecheck_code.cpp @@ -463,7 +463,7 @@ void cpp_typecheckt::typecheck_decl(codet &code) new_code.reserve_operands(declaration.declarators().size()); // Do the declarators (if any) - for(auto & declarator : declaration.declarators()) + for(auto &declarator : declaration.declarators()) { cpp_declarator_convertert cpp_declarator_converter(*this); cpp_declarator_converter.is_typedef=is_typedef; diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index e60bd707691..f05e0ef321b 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -116,9 +116,9 @@ cpp_scopet &cpp_typecheckt::tag_scope( cpp_scopet::id_sett id_set; cpp_scopes.current_scope().lookup(base_name, cpp_scopet::RECURSIVE, id_set); - for(const auto & it : id_set) - if(it->is_class()) - return static_cast(it->get_parent()); + for(const auto &id : id_set) + if(id->is_class()) + return static_cast(id->get_parent()); // Tags without body that we don't have already // and that are not a tag-only declaration go into @@ -511,14 +511,14 @@ void cpp_typecheckt::typecheck_compound_declarator( // The method may be virtual implicitly. std::set virtual_bases; - for(const auto & it : components) + for(const auto &comp : components) { - if(it.get_bool(ID_is_virtual)) + if(comp.get_bool(ID_is_virtual)) { - if(it.get("virtual_name")==virtual_name) + if(comp.get("virtual_name")==virtual_name) { is_virtual=true; - const code_typet& code_type = to_code_type(it.type()); + const code_typet& code_type=to_code_type(comp.type()); assert(code_type.parameters().size()>0); const typet& pointer_type = code_type.parameters()[0].type(); assert(pointer_type.id() == ID_pointer); @@ -646,14 +646,14 @@ void cpp_typecheckt::typecheck_compound_declarator( arg.type().subtype().set(ID_identifier, virtual_base); // create symbols for the parameters - code_typet::parameterst& args = code_type.parameters(); - for(unsigned i=0; iloc, modified); - } +void acceleration_utilst::find_modified( + const patht &path, + expr_sett &modified) +{ + for(const auto &step : path) + find_modified(step.loc, modified); } void acceleration_utilst::find_modified( - natural_loops_mutablet::natural_loopt &loop, - expr_sett &modified) { - for (natural_loops_mutablet::natural_loopt::iterator it = loop.begin(); - it != loop.end(); - ++it) { - find_modified(*it, modified); - } + const natural_loops_mutablet::natural_loopt &loop, + expr_sett &modified) +{ + for(const auto &step : loop) + find_modified(step, modified); } -void acceleration_utilst::find_modified(goto_programt::targett t, - expr_sett &modified) { +void acceleration_utilst::find_modified( + goto_programt::const_targett t, + expr_sett &modified) +{ if (t->is_assign()) { code_assignt assignment = to_code_assign(t->code); modified.insert(assignment.lhs()); diff --git a/src/goto-instrument/accelerate/acceleration_utils.h b/src/goto-instrument/accelerate/acceleration_utils.h index 02aba5cb387..8638961dc64 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.h +++ b/src/goto-instrument/accelerate/acceleration_utils.h @@ -105,13 +105,19 @@ class acceleration_utilst { void ensure_no_overflows(scratch_programt &program); - void find_modified(patht &path, expr_sett &modified); - void find_modified(goto_programt &program, expr_sett &modified); - void find_modified(goto_programt::instructionst &instructions, - expr_sett &modified); - void find_modified(natural_loops_mutablet::natural_loopt &loop, - expr_sett &modified); - void find_modified(goto_programt::targett t, expr_sett &modified); + void find_modified(const patht &path, expr_sett &modified); + void find_modified( + const goto_programt &program, + expr_sett &modified); + void find_modified( + const goto_programt::instructionst &instructions, + expr_sett &modified); + void find_modified( + const natural_loops_mutablet::natural_loopt &loop, + expr_sett &modified); + void find_modified( + goto_programt::const_targett t, + expr_sett &modified); symbolt fresh_symbol(std::string base, typet type); diff --git a/src/goto-instrument/accelerate/all_paths_enumerator.cpp b/src/goto-instrument/accelerate/all_paths_enumerator.cpp index f9830744c69..06e5b4e135a 100644 --- a/src/goto-instrument/accelerate/all_paths_enumerator.cpp +++ b/src/goto-instrument/accelerate/all_paths_enumerator.cpp @@ -8,7 +8,7 @@ bool all_paths_enumeratort::next(patht &path) { if (last_path.empty()) { // This is the first time we've been called -- build an initial // path. - last_path.push_back(loop_header); + last_path.push_back(path_nodet(loop_header)); // This shouldn't be able to fail. complete_path(last_path, 0); @@ -60,12 +60,10 @@ int all_paths_enumeratort::backtrack(patht &path) { unsigned int ret = 0; - for (goto_programt::targetst::iterator it = succs.begin(); - it != succs.end(); - ++it) { - if (*it == node.loc) { + for (const auto & succ : succs) + { + if(succ==node.loc) break; - } ret++; } @@ -111,11 +109,10 @@ void all_paths_enumeratort::extend_path(patht &path, goto_program.get_successors(t, succs); - for (goto_programt::targetst::iterator it = succs.begin(); - it != succs.end(); - ++it) { + for(const auto &s : succs) + { if (succ == 0) { - next = *it; + next=s; break; } diff --git a/src/goto-instrument/accelerate/cone_of_influence.cpp b/src/goto-instrument/accelerate/cone_of_influence.cpp index c55c4021488..9d0b9c4964a 100644 --- a/src/goto-instrument/accelerate/cone_of_influence.cpp +++ b/src/goto-instrument/accelerate/cone_of_influence.cpp @@ -33,19 +33,13 @@ void cone_of_influencet::cone_of_influence(const expr_sett &targets, #ifdef DEBUG std::cout << "Previous cone: " << std::endl; - for (expr_sett::iterator it = curr.begin(); - it != curr.end(); - ++it) { - std::cout << expr2c(*it, ns) << " "; - } + for(const auto &expr : curr) + std::cout << expr2c(expr, ns) << " "; std::cout << std::endl << "Current cone: " << std::endl; - for (expr_sett::iterator it = next.begin(); - it != next.end(); - ++it) { - std::cout << expr2c(*it, ns) << " "; - } + for(const auto &expr : next) + std::cout << expr2c(expr, ns) << " "; std::cout << std::endl; #endif @@ -110,14 +104,12 @@ void cone_of_influencet::cone_of_influence( gather_rvalues(assignment.lhs(), lhs_syms); - for (expr_sett::iterator it = lhs_syms.begin(); - it != lhs_syms.end(); - ++it) { - if (curr.find(*it) != curr.end()) { + for(const auto &expr : lhs_syms) + if(curr.find(expr)!=curr.end()) + { care = true; break; } - } next.erase(assignment.lhs()); diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp index 65c8056b4a1..da0baedc3e8 100644 --- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp +++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp @@ -705,16 +705,15 @@ void disjunctive_polynomial_accelerationt::build_path( // to see which branch was taken. bool found_branch = false; - for (goto_programt::targetst::iterator it = succs.begin(); - it != succs.end(); - ++it) { - exprt &distinguisher = distinguishing_points[*it]; + for(const auto &succ : succs) + { + exprt &distinguisher=distinguishing_points[succ]; bool taken = scratch_program.eval(distinguisher).is_true(); if (taken) { if (!found_branch || - ((*it)->location_number < next->location_number)) { - next = *it; + (succ->location_number < next->location_number)) { + next=succ; } found_branch = true; @@ -836,12 +835,12 @@ void disjunctive_polynomial_accelerationt::build_fixed() { // header we're happy & redirect it to our end-of-body sentinel. // If it jumps somewhere else, it's part of a nested loop and we // kill it. - for (goto_programt::targetst::iterator target = t->targets.begin(); - target != t->targets.end(); - ++target) { - if ((*target)->location_number > t->location_number) { + for(const auto &target : t->targets) + { + if (target->location_number > t->location_number) { // A forward jump... - if (loop.find(*target) != loop.end()) { + if(loop.find(target)!=loop.end()) + { // Case 1: a forward jump within the loop. Do nothing. continue; } else { @@ -851,7 +850,7 @@ void disjunctive_polynomial_accelerationt::build_fixed() { } } else { // A backwards jump... - if (*target == loop_header) { + if (target==loop_header) { // Case 3: a backwards jump to the loop header. Redirect to sentinel. fixedt->targets.clear(); fixedt->targets.push_back(end); @@ -869,12 +868,11 @@ void disjunctive_polynomial_accelerationt::build_fixed() { // body is the same as the master path. We do this by assuming that // each of the shadow-distinguisher variables is equal to its corresponding // master-distinguisher. - for (std::list::iterator it = distinguishers.begin(); - it != distinguishers.end(); - ++it) { - exprt &shadow = shadow_distinguishers[*it]; + for(const auto &expr : distinguishers) + { + const exprt &shadow=shadow_distinguishers[expr]; - fixed.insert_after(end)->make_assumption(equal_exprt(*it, shadow)); + fixed.insert_after(end)->make_assumption(equal_exprt(expr, shadow)); } // Finally, let's remove all the skips we introduced and fix the diff --git a/src/goto-instrument/accelerate/path.cpp b/src/goto-instrument/accelerate/path.cpp index 7d99309625b..cba1105befa 100644 --- a/src/goto-instrument/accelerate/path.cpp +++ b/src/goto-instrument/accelerate/path.cpp @@ -4,11 +4,12 @@ #include "path.h" -void output_path(patht &path, goto_programt &program, namespacet &ns, - std::ostream &str) { - for (patht::iterator it = path.begin(); - it != path.end(); - ++it) { - program.output_instruction(ns, "path", str, it->loc); - } +void output_path( + const patht &path, + const goto_programt &program, + const namespacet &ns, + std::ostream &str) +{ + for(const auto &step : path) + program.output_instruction(ns, "path", str, step.loc); } diff --git a/src/goto-instrument/accelerate/path.h b/src/goto-instrument/accelerate/path.h index 0c24ff2681f..5f573e09da8 100644 --- a/src/goto-instrument/accelerate/path.h +++ b/src/goto-instrument/accelerate/path.h @@ -12,20 +12,20 @@ class path_nodet { public: - path_nodet(goto_programt::targett &_loc) : - loc(_loc), - guard(nil_exprt()) + explicit path_nodet(const goto_programt::targett &_loc): + loc(_loc), + guard(nil_exprt()) { } - path_nodet(goto_programt::targett &_loc, + path_nodet(const goto_programt::targett &_loc, const exprt &_guard) : loc(_loc), guard(_guard) { } - void output(goto_programt &program, std::ostream &str); + void output(const goto_programt &program, std::ostream &str); goto_programt::targett loc; const exprt guard; @@ -34,6 +34,10 @@ class path_nodet typedef std::list patht; typedef std::list pathst; -void output_path(patht &path, goto_programt &program, namespacet &ns, std::ostream &str); +void output_path( + const patht &path, + const goto_programt &program, + const namespacet &ns, + std::ostream &str); #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_PATH_H diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp index a46608f2a57..1a1444ea146 100644 --- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp +++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp @@ -99,14 +99,13 @@ void sat_path_enumeratort::find_distinguishing_points() { if (succs.size() > 1) { // This location has multiple successors -- each successor is a // distinguishing point. - for (goto_programt::targetst::iterator jt = succs.begin(); - jt != succs.end(); - ++jt) { + for(const auto &succ : succs) + { symbolt distinguisher_sym = utils.fresh_symbol("polynomial::distinguisher", bool_typet()); symbol_exprt distinguisher = distinguisher_sym.symbol_expr(); - distinguishing_points[*jt] = distinguisher; + distinguishing_points[succ]=distinguisher; distinguishers.push_back(distinguisher); } } @@ -138,16 +137,15 @@ void sat_path_enumeratort::build_path( // to see which branch was taken. bool found_branch = false; - for (goto_programt::targetst::iterator it = succs.begin(); - it != succs.end(); - ++it) { - exprt &distinguisher = distinguishing_points[*it]; + for(const auto &succ : succs) + { + exprt &distinguisher=distinguishing_points[succ]; bool taken = scratch_program.eval(distinguisher).is_true(); if (taken) { if (!found_branch || - ((*it)->location_number < next->location_number)) { - next = *it; + (succ->location_number < next->location_number)) { + next=succ; } found_branch = true; @@ -269,12 +267,13 @@ void sat_path_enumeratort::build_fixed() { // header we're happy & redirect it to our end-of-body sentinel. // If it jumps somewhere else, it's part of a nested loop and we // kill it. - for (goto_programt::targetst::iterator target = t->targets.begin(); - target != t->targets.end(); - ++target) { - if ((*target)->location_number > t->location_number) { + for(const auto &target : t->targets) + { + if(target->location_number > t->location_number) + { // A forward jump... - if (loop.find(*target) != loop.end()) { + if(loop.find(target)!=loop.end()) + { // Case 1: a forward jump within the loop. Do nothing. continue; } else { @@ -284,7 +283,8 @@ void sat_path_enumeratort::build_fixed() { } } else { // A backwards jump... - if (*target == loop_header) { + if (target==loop_header) + { // Case 3: a backwards jump to the loop header. Redirect to sentinel. fixedt->targets.clear(); fixedt->targets.push_back(end); @@ -302,12 +302,11 @@ void sat_path_enumeratort::build_fixed() { // body is the same as the master path. We do this by assuming that // each of the shadow-distinguisher variables is equal to its corresponding // master-distinguisher. - for (std::list::iterator it = distinguishers.begin(); - it != distinguishers.end(); - ++it) { - exprt &shadow = shadow_distinguishers[*it]; + for(const auto &expr : distinguishers) + { + const exprt &shadow=shadow_distinguishers[expr]; - fixed.insert_after(end)->make_assumption(equal_exprt(*it, shadow)); + fixed.insert_after(end)->make_assumption(equal_exprt(expr, shadow)); } // Finally, let's remove all the skips we introduced and fix the @@ -320,11 +319,8 @@ void sat_path_enumeratort::record_path(scratch_programt &program) { distinguish_valuest path_val; - for (std::list::iterator it = distinguishers.begin(); - it != distinguishers.end(); - ++it) { - path_val[*it] = program.eval(*it).is_true(); - } + for(const auto &expr : distinguishers) + path_val[expr]=program.eval(expr).is_true(); accelerated_paths.push_back(path_val); } diff --git a/src/goto-instrument/accelerate/trace_automaton.cpp b/src/goto-instrument/accelerate/trace_automaton.cpp index 98718be2124..30e36a683a5 100644 --- a/src/goto-instrument/accelerate/trace_automaton.cpp +++ b/src/goto-instrument/accelerate/trace_automaton.cpp @@ -28,9 +28,8 @@ void trace_automatont::build() { * successors of any location with multiple successors. */ void trace_automatont::build_alphabet(goto_programt &program) { - for (goto_programt::targett it = program.instructions.begin(); - it != program.instructions.end(); - ++it) { + Forall_goto_program_instructions(it, program) + { goto_programt::targetst succs; program.get_successors(it, succs); @@ -44,12 +43,8 @@ void trace_automatont::build_alphabet(goto_programt &program) { void trace_automatont::init_nta() { nta.init_state = nta.add_state(); - for (alphabett::iterator it = alphabet.begin(); - it != alphabet.end(); - ++it) { - goto_programt::targett &t = const_cast(*it); - nta.add_trans(nta.init_state, t, nta.init_state); - } + for(const auto &sym : alphabet) + nta.add_trans(nta.init_state, sym, nta.init_state); } /* @@ -65,10 +60,9 @@ void trace_automatont::add_path(patht &path) { std::cout << "Adding path: "; #endif - for (patht::iterator it = path.begin(); - it != path.end(); - ++it) { - goto_programt::targett l = it->loc; + for(const auto &step : path) + { + goto_programt::targett l=step.loc; #ifdef DEBUG std::cout << ", " << l->location_number << ":" << l->location; #endif @@ -291,12 +285,13 @@ void automatont::move(statet s, goto_programt::targett a, state_sett &t) { } } -void automatont::move(state_sett &s, goto_programt::targett a, state_sett &t) { - for (state_sett::iterator it = s.begin(); - it != s.end(); - ++it) { - move(*it, a, t); - } +void automatont::move( + state_sett &s, + goto_programt::targett a, + state_sett &t) +{ + for(const auto &state : s) + move(state, a, t); } void trace_automatont::get_transitions(sym_mapt &transitions) @@ -307,11 +302,10 @@ void trace_automatont::get_transitions(sym_mapt &transitions) { automatont::transitionst &dta_transitions = dtrans[i]; - for (automatont::transitionst::iterator it = dta_transitions.begin(); - it != dta_transitions.end(); - ++it) { - goto_programt::targett l = it->first; - unsigned int j = it->second; + for(const auto &trans : dta_transitions) + { + goto_programt::targett l=trans.first; + unsigned int j=trans.second; // We have a transition: i -l-> j. state_pairt state_pair(i, j); @@ -341,11 +335,8 @@ void automatont::reverse(goto_programt::targett epsilon) // epsilon transitions to each accept state. new_init = add_state(); - for (state_sett::iterator it = accept_states.begin(); - it != accept_states.end(); - ++it) { - add_trans(new_init, epsilon, *it); - } + for(const auto &s : accept_states) + add_trans(new_init, epsilon, s); } std::cout << "Reversing automaton, old init=" << init_state << ", new init=" @@ -361,11 +352,10 @@ void automatont::reverse(goto_programt::targett epsilon) { transitionst &trans = old_table[i]; - for (transitionst::iterator it = trans.begin(); - it != trans.end(); - ++it) { - goto_programt::targett l = it->first; - unsigned int j = it->second; + for(const auto &t : trans) + { + goto_programt::targett l=t.first; + unsigned int j=t.second; // There was a transition i -l-> j, so add a transition // j -l-> i. @@ -384,15 +374,13 @@ void automatont::trim() { do { state_sett tmp; - for (state_sett::iterator it = new_states.begin(); - it != new_states.end(); - ++it) { - transitionst &trans = transitions[*it]; + for(const auto &s : new_states) + { + transitionst &trans=transitions[s]; - for (transitionst::iterator jt = trans.begin(); - jt != trans.end(); - ++jt) { - unsigned int j = jt->second; + for(const auto &t : trans) + { + unsigned int j=t.second; if (reachable.find(j) == reachable.end()) { reachable.insert(j); @@ -429,20 +417,16 @@ void automatont::output(std::ostream &str) { str << "Accept states: "; - for (state_sett::iterator it = accept_states.begin(); - it != accept_states.end(); - ++it) { - str << *it << " "; - } + for(const auto &state : accept_states) + str << state << " "; str << std::endl; for (unsigned int i = 0; i < transitions.size(); ++i) { - for (transitionst::iterator it = transitions[i].begin(); - it != transitions[i].end(); - ++it) { - goto_programt::targett l = it->first; - statet j = it->second; + for(const auto &trans : transitions[i]) + { + goto_programt::targett l=trans.first; + statet j=trans.second; str << i << " -- " << l->location_number << " --> " << j << std::endl; } @@ -453,11 +437,8 @@ std::size_t automatont::count_transitions() { std::size_t ret = 0; - for (transition_tablet::iterator it = transitions.begin(); - it != transitions.end(); - ++it) { - ret += it->size(); - } + for(const auto &trans : transitions) + ret+=trans.size(); return ret; } diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 5f02f91a0ee..f27bbd5f19c 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -136,7 +136,7 @@ void collect_conditions_rec(const exprt &src, std::set &dest) return; } - for(const auto & op : src.operands()) + for(const auto &op : src.operands()) collect_conditions_rec(op, dest); if(is_condition(src) && !src.is_constant()) @@ -988,7 +988,7 @@ void collect_decisions_rec(const exprt &src, std::set &dest) } else { - for(const auto & op : src.operands()) + for(const auto &op : src.operands()) collect_decisions_rec(op, dest); } } @@ -1202,7 +1202,7 @@ void instrument_cover_goals( const source_locationt source_location=i_it->source_location; - for(const auto & c : conditions) + for(const auto &c : conditions) { const std::string c_string=from_expr(ns, "", c); @@ -1238,7 +1238,7 @@ void instrument_cover_goals( const source_locationt source_location=i_it->source_location; - for(const auto & d : decisions) + for(const auto &d : decisions) { const std::string d_string=from_expr(ns, "", d); @@ -1284,7 +1284,7 @@ void instrument_cover_goals( const source_locationt source_location=i_it->source_location; - for(const auto & p : both) + for(const auto &p : both) { bool is_decision=decisions.find(p)!=decisions.end(); bool is_condition=conditions.find(p)!=conditions.end(); @@ -1322,7 +1322,7 @@ void instrument_cover_goals( // however, this is not true, e.g., ''? :'' operator. minimize_mcdc_controlling(controlling, *decisions.begin()); - for(const auto & p : controlling) + for(const auto &p : controlling) { std::string p_string=from_expr(ns, "", p); diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp index f6a587274fa..4bd1215ebba 100644 --- a/src/goto-instrument/dot.cpp +++ b/src/goto-instrument/dot.cpp @@ -242,39 +242,36 @@ Function: dott::do_dot_function_calls void dott::do_dot_function_calls( std::ostream &out) { - for(std::list::const_iterator - it=function_calls.begin(); - it!=function_calls.end(); - it++) + for(const auto &expr : function_calls) { std::list::const_iterator cit=clusters.begin(); for(;cit!=clusters.end();cit++) - if(cit->get("name")==it->op1().get(ID_identifier)) + if(cit->get("name")==expr.op1().get(ID_identifier)) break; if(cit!=clusters.end()) { - out << it->op0().id() << + out << expr.op0().id() << " -> " "Node_" << cit->get("nr") << "_0" << - " [lhead=\"cluster_" << it->op1().get(ID_identifier) << "\"," << + " [lhead=\"cluster_" << expr.op1().get(ID_identifier) << "\"," << "color=blue];" << std::endl; } else { - out << "subgraph \"cluster_" << it->op1().get(ID_identifier) << + out << "subgraph \"cluster_" << expr.op1().get(ID_identifier) << "\" {" << std::endl; out << "rank=sink;"<op1().get(ID_identifier) << "\";" << std::endl; + out << "label=\"" << expr.op1().get(ID_identifier) << "\";" << std::endl; out << "Node_" << subgraphscount << "_0 " << "[shape=Mrecord,fontsize=22,label=\"?\"];" << std::endl; out << "}" << std::endl; clusters.push_back(exprt("cluster")); - clusters.back().set("name", it->op1().get(ID_identifier)); + clusters.back().set("name", expr.op1().get(ID_identifier)); clusters.back().set("nr", subgraphscount); - out << it->op0().id() << + out << expr.op0().id() << " -> " "Node_" << subgraphscount << "_0" << - " [lhead=\"cluster_" << it->op1().get("identifier") << "\"," << + " [lhead=\"cluster_" << expr.op1().get("identifier") << "\"," << "color=blue];" << std::endl; subgraphscount++; } @@ -300,14 +297,9 @@ void dott::output(std::ostream &out) std::list clusters; - for(goto_functionst::function_mapt::const_iterator - it=goto_functions.function_map.begin(); - it!=goto_functions.function_map.end(); - it++) - { + forall_goto_functions(it, goto_functions) if(it->second.body_available()) write_dot_subgraph(out, id2string(it->first), it->second.body); - } do_dot_function_calls(out); @@ -329,7 +321,7 @@ Function: dott::escape std::string &dott::escape(std::string &str) { - for(unsigned i=0; iis_goto() && !it->guard.is_false()) { - goto_programt::targetst::const_iterator gtit = it->targets.begin(); - for (; gtit!=it->targets.end(); gtit++) - tres.insert((*gtit)); + for(const auto &target : it->targets) + tres.insert(target); } if(it->is_goto() && it->guard.is_true()) diff --git a/src/goto-instrument/havoc_loops.cpp b/src/goto-instrument/havoc_loops.cpp index 600cfa3c977..fe2266cfd7d 100644 --- a/src/goto-instrument/havoc_loops.cpp +++ b/src/goto-instrument/havoc_loops.cpp @@ -235,11 +235,8 @@ void havoc_loopst::havoc_loops() { // iterate over the (natural) loops in the function - for(natural_loops_mutablet::loop_mapt::const_iterator - l_it=natural_loops.loop_map.begin(); - l_it!=natural_loops.loop_map.end(); - l_it++) - havoc_loop(l_it->first, l_it->second); + for(const auto &loop : natural_loops.loop_map) + havoc_loop(loop.first, loop.second); } /*******************************************************************\ diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp index 3d0235aae96..53fc3d409e1 100644 --- a/src/goto-instrument/unwind.cpp +++ b/src/goto-instrument/unwind.cpp @@ -385,8 +385,7 @@ void goto_unwindt::unwind( { assert(k>=-1); - for(goto_programt::const_targett i_it=goto_program.instructions.begin(); - i_it!=goto_program.instructions.end(); i_it++) + forall_goto_program_instructions(i_it, goto_program) { if(!i_it->is_backwards_goto()) continue; diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index 7f18743cece..bdca381e025 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -336,14 +336,10 @@ void inline instrumentert::cfg_visitort::visit_cfg_propagate( const goto_programt::instructiont& instruction=*i_it; /* propagation */ in_pos[i_it].clear(); - for(target_sett::const_iterator prev=instruction.incoming_edges.begin(); - prev!=instruction.incoming_edges.end(); - ++prev) - if(in_pos.find(*prev)!=in_pos.end()) - for(std::set::const_iterator s_it=in_pos[*prev].begin(); - s_it!=in_pos[*prev].end(); - ++s_it) - in_pos[i_it].insert(*s_it); + for(const auto &in : instruction.incoming_edges) + if(in_pos.find(in)!=in_pos.end()) + for(const auto &node : in_pos[in]) + in_pos[i_it].insert(node); } /*******************************************************************\ @@ -428,21 +424,19 @@ void inline instrumentert::cfg_visitort::visit_cfg_reference_function ( cur!=targ; --cur) { instrumenter.message.debug() << "i" << messaget::eom; - for(std::set::const_iterator - t=cur->incoming_edges.begin(); - t!=cur->incoming_edges.end(); ++t) + for(const auto &in : cur->incoming_edges) { instrumenter.message.debug() << "t" << messaget::eom; - if(in_pos.find(*t)!=in_pos.end() - && updated.find(*t)!=updated.end()) + if(in_pos.find(in)!=in_pos.end() + && updated.find(in)!=updated.end()) { - /* out_pos[*t].insert(in_pos[*t])*/ - add_all_pos(it1, out_pos[*t], in_pos[*t]); + /* out_pos[in].insert(in_pos[in])*/ + add_all_pos(it1, out_pos[in], in_pos[in]); } - else if(in_pos.find(*t)!=in_pos.end()) + else if(in_pos.find(in)!=in_pos.end()) { - /* out_pos[*t].insert(out_pos[cur])*/ - add_all_pos(it2, out_pos[*t], out_pos[cur]); + /* out_pos[in].insert(out_pos[cur])*/ + add_all_pos(it2, out_pos[in], out_pos[cur]); } } } @@ -558,7 +552,7 @@ Function: instrumentert::visit_cfg_visitort::visit_cfg_body \*******************************************************************/ void inline instrumentert::cfg_visitort::visit_cfg_body( - goto_programt::instructionst::iterator i_it, + goto_programt::const_targett i_it, loop_strategyt replicate_body, value_setst& value_sets #ifdef LOCAL_MAY @@ -566,15 +560,11 @@ void inline instrumentert::cfg_visitort::visit_cfg_body( #endif ) { - const goto_programt::instructiont& instruction=*i_it; - /* for each target of the goto */ - for(goto_programt::instructiont::targetst::const_iterator - targ=instruction.targets.begin(); - targ!=instruction.targets.end(); ++targ) + for(const auto &target : i_it->targets) { /* if the target has already been covered by fwd analysis */ - if(in_pos.find(*targ)!=in_pos.end()) + if(in_pos.find(target)!=in_pos.end()) { if(in_pos[i_it].empty()) continue; @@ -583,7 +573,7 @@ void inline instrumentert::cfg_visitort::visit_cfg_body( switch(replicate_body) { case arrays_only: - duplicate_this=contains_shared_array(*targ, i_it, value_sets + duplicate_this=contains_shared_array(target, i_it, value_sets #ifdef LOCAL_MAY , local_may #endif @@ -598,9 +588,9 @@ void inline instrumentert::cfg_visitort::visit_cfg_body( } if(duplicate_this) - visit_cfg_duplicate(*targ, i_it); + visit_cfg_duplicate(target, i_it); else - visit_cfg_backedge(*targ, i_it); + visit_cfg_backedge(target, i_it); } } } @@ -618,13 +608,13 @@ Function: instrumentert::visit_cfg_visitort::visit_cfg_duplicate \*******************************************************************/ void inline instrumentert::cfg_visitort::visit_cfg_duplicate( - goto_programt::targett targ, goto_programt::targett i_it) + goto_programt::const_targett targ, goto_programt::const_targett i_it) { instrumenter.message.status() << "Duplication..." << messaget::eom; const goto_functionst::goto_functiont& fun=instrumenter.goto_functions.function_map[i_it->function]; bool found_pos=false; - goto_programt::instructiont::targett new_targ=targ; + goto_programt::const_targett new_targ=targ; if(in_pos[targ].empty()) { @@ -689,7 +679,7 @@ Function: instrumentert::visit_cfg_visitort::visit_cfg_backedge \*******************************************************************/ void inline instrumentert::cfg_visitort::visit_cfg_backedge( - goto_programt::targett targ, goto_programt::targett i_it) + goto_programt::const_targett targ, goto_programt::const_targett i_it) { /* if in_pos was updated at this program point */ if(updated.find(targ)!=updated.end()) @@ -714,23 +704,21 @@ void inline instrumentert::cfg_visitort::visit_cfg_backedge( instrumenter.message.debug() << "else case" << messaget::eom; /* connects NEXT nodes following the targets -- bwd analysis */ - for(goto_programt::instructionst::iterator cur=i_it; + for(goto_programt::const_targett cur=i_it; cur!=targ; --cur) { - for(std::set::const_iterator - t=cur->incoming_edges.begin(); - t!=cur->incoming_edges.end(); ++t) + for(const auto &in : cur->incoming_edges) { - if(in_pos.find(*t)!=in_pos.end() - && updated.find(*t)!=updated.end()) + if(in_pos.find(in)!=in_pos.end() + && updated.find(in)!=updated.end()) { - /* out_pos[*t].insert(in_pos[*t])*/ - add_all_pos(it1, out_pos[*t], in_pos[*t]); + /* out_pos[in].insert(in_pos[in])*/ + add_all_pos(it1, out_pos[in], in_pos[in]); } - else if(in_pos.find(*t)!=in_pos.end()) + else if(in_pos.find(in)!=in_pos.end()) { - /* out_pos[*t].insert(in_pos[cur])*/ - add_all_pos(it2, out_pos[*t], out_pos[cur]); + /* out_pos[in].insert(in_pos[cur])*/ + add_all_pos(it2, out_pos[in], out_pos[cur]); } } } @@ -815,12 +803,10 @@ void instrumentert::cfg_visitort::visit_cfg_function_call( { const goto_programt::instructiont& instruction=*i_it; std::set s; - for(target_sett::const_iterator prev=instruction.incoming_edges.begin(); - prev!=instruction.incoming_edges.end(); ++prev) - if(in_pos.find(*prev)!=in_pos.end()) - for(std::set::const_iterator s_it=in_pos[*prev].begin(); - s_it!=in_pos[*prev].end(); ++s_it) - s.insert(*s_it); + for(const auto &in : instruction.incoming_edges) + if(in_pos.find(in)!=in_pos.end()) + for(const auto &node : in_pos[in]) + s.insert(node); const exprt& fun=to_code_function_call(instruction.code).function(); const irep_idt& fun_id=to_symbol_expr(fun).get_identifier(); @@ -895,18 +881,16 @@ void instrumentert::cfg_visitort::visit_cfg_lwfence( instrumenter.map_vertex_gnode.insert( std::make_pair(new_fence_node, new_fence_gnode)); - for(target_sett::const_iterator prev=instruction.incoming_edges.begin(); - prev!=instruction.incoming_edges.end(); ++prev) - if(in_pos.find(*prev)!=in_pos.end()) - for(std::set::const_iterator s_it=in_pos[*prev].begin(); - s_it!=in_pos[*prev].end(); ++s_it) + for(const auto &in : instruction.incoming_edges) + if(in_pos.find(in)!=in_pos.end()) + for(const auto &node : in_pos[in]) { - if(egraph[s_it->first].thread!=thread) + if(egraph[node.first].thread!=thread) continue; - instrumenter.message.debug() << s_it->first<<"-po->"<"<first,new_fence_node); - egraph_alt.add_edge(s_it->second,new_fence_gnode); + egraph.add_po_edge(node.first,new_fence_node); + egraph_alt.add_edge(node.second,new_fence_gnode); } in_pos[i_it].clear(); @@ -947,18 +931,16 @@ void instrumentert::cfg_visitort::visit_cfg_asm_fence( instrumenter.map_vertex_gnode.insert( std::make_pair(new_fence_node, new_fence_gnode)); - for(target_sett::const_iterator prev=instruction.incoming_edges.begin(); - prev!=instruction.incoming_edges.end(); ++prev) - if(in_pos.find(*prev)!=in_pos.end()) - for(std::set::const_iterator s_it=in_pos[*prev].begin(); - s_it!=in_pos[*prev].end(); ++s_it) + for(const auto &in : instruction.incoming_edges) + if(in_pos.find(in)!=in_pos.end()) + for(const auto &node : in_pos[in]) { - if(egraph[s_it->first].thread!=thread) + if(egraph[node.first].thread!=thread) continue; - instrumenter.message.debug() << s_it->first<<"-po->"<"<first,new_fence_node); - egraph_alt.add_edge(s_it->second,new_fence_gnode); + egraph.add_po_edge(node.first,new_fence_node); + egraph_alt.add_edge(node.second,new_fence_gnode); } in_pos[i_it].clear(); @@ -1046,21 +1028,17 @@ void instrumentert::cfg_visitort::visit_cfg_assign( std::make_pair(new_read_node,new_read_gnode)); /* creates ... -po-> Read */ - for(target_sett::const_iterator prev=instruction.incoming_edges.begin(); - prev!=instruction.incoming_edges.end(); - ++prev) + for(const auto &in : instruction.incoming_edges) { - if(in_pos.find(*prev)!=in_pos.end()) - for(std::set::const_iterator s_it=in_pos[*prev].begin(); - s_it!=in_pos[*prev].end(); - ++s_it) + if(in_pos.find(in)!=in_pos.end()) + for(const auto &node : in_pos[in]) { - if(egraph[s_it->first].thread!=thread) + if(egraph[node.first].thread!=thread) continue; - instrumenter.message.debug() << s_it->first<<"-po->" + instrumenter.message.debug() << node.first<<"-po->" <first,new_read_node); - egraph_alt.add_edge(s_it->second,new_read_gnode); + egraph.add_po_edge(node.first,new_read_node); + egraph_alt.add_edge(node.second,new_read_gnode); } } @@ -1154,21 +1132,17 @@ void instrumentert::cfg_visitort::visit_cfg_assign( egraph_alt.add_edge(previous_gnode,new_write_gnode); } else - for(target_sett::const_iterator prev=instruction.incoming_edges.begin(); - prev!=instruction.incoming_edges.end(); - ++prev) + for(const auto &in : instruction.incoming_edges) { - if(in_pos.find(*prev)!=in_pos.end()) - for(std::set::const_iterator s_it=in_pos[*prev].begin(); - s_it!=in_pos[*prev].end(); - ++s_it) + if(in_pos.find(in)!=in_pos.end()) + for(const auto &node : in_pos[in]) { - if(egraph[s_it->first].thread!=thread) + if(egraph[node.first].thread!=thread) continue; - instrumenter.message.debug() << s_it->first<<"-po->" + instrumenter.message.debug() << node.first<<"-po->" <first,new_write_node); - egraph_alt.add_edge(s_it->second,new_write_gnode); + egraph.add_po_edge(node.first,new_write_node); + egraph_alt.add_edge(node.second,new_write_gnode); } } @@ -1322,18 +1296,14 @@ void instrumentert::cfg_visitort::visit_cfg_fence( instrumenter.map_vertex_gnode.insert( std::make_pair(new_fence_node, new_fence_gnode)); - for(target_sett::const_iterator prev=instruction.incoming_edges.begin(); - prev!=instruction.incoming_edges.end(); - ++prev) - if(in_pos.find(*prev)!=in_pos.end()) - for(std::set::const_iterator s_it=in_pos[*prev].begin(); - s_it!=in_pos[*prev].end(); - ++s_it) + for(const auto &in : instruction.incoming_edges) + if(in_pos.find(in)!=in_pos.end()) + for(const auto &node : in_pos[in]) { - instrumenter.message.debug() << s_it->first<<"-po->"<"<first,new_fence_node); - egraph_alt.add_edge(s_it->second,new_fence_gnode); + egraph.add_po_edge(node.first,new_fence_node); + egraph_alt.add_edge(node.second,new_fence_gnode); } #if 0 std::set s; @@ -1520,15 +1490,12 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet& cyc) Forall_goto_program_instructions(int_it, interleaving) if(int_it->is_goto()) { - for(goto_programt::instructiont::targetst::const_iterator label= - int_it->targets.begin(); - label!=int_it->targets.end(); - label++) + for(const auto &t : int_it->targets) { bool target_in_cycle = false; - Forall_goto_program_instructions(targ, interleaving) - if(targ==*label) + forall_goto_program_instructions(targ, interleaving) + if(targ==t) { target_in_cycle = true; break; @@ -1536,10 +1503,7 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet& cyc) if(!target_in_cycle) { - goto_programt::instructiont new_inst; - new_inst.make_assertion(false_exprt()); - int_it->swap(new_inst); - // delete new_inst + int_it->make_assertion(false_exprt()); break; } } diff --git a/src/goto-instrument/wmm/goto2graph.h b/src/goto-instrument/wmm/goto2graph.h index 05e5b2c37ec..3e13bcc3d6c 100644 --- a/src/goto-instrument/wmm/goto2graph.h +++ b/src/goto-instrument/wmm/goto2graph.h @@ -112,17 +112,17 @@ class instrumentert void visit_cfg_thread() const; void visit_cfg_propagate(goto_programt::instructionst::iterator i_it); void visit_cfg_body( - goto_programt::instructionst::iterator i_it, + goto_programt::const_targett i_it, loop_strategyt replicate_body, value_setst& value_sets #ifdef LOCAL_MAY , local_may_aliast& local_may #endif ); // deprecated - void inline visit_cfg_backedge(goto_programt::targett targ, - goto_programt::targett i_it); - void inline visit_cfg_duplicate(goto_programt::targett targ, - goto_programt::targett i_it); + void inline visit_cfg_backedge(goto_programt::const_targett targ, + goto_programt::const_targett i_it); + void inline visit_cfg_duplicate(goto_programt::const_targett targ, + goto_programt::const_targett i_it); void visit_cfg_assign(value_setst& value_sets, namespacet& ns, goto_programt::instructionst::iterator& i_it, bool no_dependencies #ifdef LOCAL_MAY @@ -169,11 +169,11 @@ class instrumentert /* previous nodes (fwd analysis) */ typedef std::pair nodet; - typedef std::map > + typedef std::map > incoming_post; incoming_post in_pos; - std::set updated; + std::set updated; /* "next nodes" (bwd steps in fwd/bck analysis) */ incoming_post out_pos; diff --git a/src/goto-programs/basic_blocks.cpp b/src/goto-programs/basic_blocks.cpp index 3289a6f530a..9ac1b69e0cc 100644 --- a/src/goto-programs/basic_blocks.cpp +++ b/src/goto-programs/basic_blocks.cpp @@ -33,11 +33,8 @@ void basic_blocks(goto_programt &goto_program, i_it!=goto_program.instructions.end(); i_it++) if(i_it->is_goto()) - for(goto_programt::instructiont::targetst::iterator - t_it=i_it->targets.begin(); - t_it!=i_it->targets.end(); - t_it++) - targets.insert(*t_it); + for(const auto &target : i_it->targets) + targets.insert(target); // Scan program for(goto_programt::instructionst::iterator diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index fdf09c2c670..687b13a664a 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -294,7 +294,7 @@ void goto_convertt::do_scanf( std::size_t argument_number=1; - for(const auto & t : token_list) + for(const auto &t : token_list) { typet type=get_type(t); diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h index bbba1120574..7c339782937 100644 --- a/src/goto-programs/cfg.h +++ b/src/goto-programs/cfg.h @@ -216,15 +216,9 @@ void cfg_baset::compute_edges_goto( !instruction.guard.is_true()) this->add_edge(entry, entry_map[next_PC]); - for(goto_programt::instructiont::targetst::const_iterator - t_it=instruction.targets.begin(); - t_it!=instruction.targets.end(); - t_it++) - { - goto_programt::const_targett t=*t_it; + for(const auto &t : instruction.targets) if(t!=goto_program.instructions.end()) this->add_edge(entry, entry_map[t]); - } } /*******************************************************************\ @@ -252,15 +246,9 @@ void cfg_baset::compute_edges_catch( // Not ideal, but preserves targets // Ideally, the throw statements should have those as successors - for(goto_programt::instructiont::targetst::const_iterator - t_it=instruction.targets.begin(); - t_it!=instruction.targets.end(); - t_it++) - { - goto_programt::const_targett t=*t_it; + for(const auto &t : instruction.targets) if(t!=goto_program.instructions.end()) this->add_edge(entry, entry_map[t]); - } } /*******************************************************************\ @@ -333,15 +321,9 @@ void concurrent_cfg_baset::compute_edges_start_thread( next_PC, entry); - for(goto_programt::instructiont::targetst::const_iterator - t_it=instruction.targets.begin(); - t_it!=instruction.targets.end(); - t_it++) - { - goto_programt::const_targett t=*t_it; + for(const auto &t : instruction.targets) if(t!=goto_program.instructions.end()) this->add_edge(entry, this->entry_map[t]); - } } /*******************************************************************\ diff --git a/src/goto-programs/class_hierarchy.cpp b/src/goto-programs/class_hierarchy.cpp index af6a5ea882d..1988cae7471 100644 --- a/src/goto-programs/class_hierarchy.cpp +++ b/src/goto-programs/class_hierarchy.cpp @@ -39,7 +39,7 @@ void class_hierarchyt::operator()(const symbol_tablet &symbol_table) const irept::subt &bases= struct_type.find(ID_bases).get_sub(); - for(const auto & base : bases) + for(const auto &base : bases) { irep_idt parent=base.find(ID_type).get(ID_identifier); if(parent.empty()) continue; @@ -71,11 +71,11 @@ void class_hierarchyt::get_children_trans_rec( if(it==class_map.end()) return; const entryt &entry=it->second; - for(const auto & child : entry.children) + for(const auto &child : entry.children) dest.push_back(child); // recursive calls - for(const auto & child : entry.children) + for(const auto &child : entry.children) get_children_trans_rec(child, dest); } @@ -99,11 +99,11 @@ void class_hierarchyt::get_parents_trans_rec( if(it==class_map.end()) return; const entryt &entry=it->second; - for(const auto & child : entry.parents) + for(const auto &child : entry.parents) dest.push_back(child); // recursive calls - for(const auto & child : entry.parents) + for(const auto &child : entry.parents) get_parents_trans_rec(child, dest); } @@ -121,13 +121,13 @@ Function: class_hierarchyt::output void class_hierarchyt::output(std::ostream &out) const { - for(const auto & c : class_map) + for(const auto &c : class_map) { - for(const auto & pa : c.second.parents) + for(const auto &pa : c.second.parents) out << "Parent of " << c.first << ": " << pa << '\n'; - for(const auto & ch : c.second.children) + for(const auto &ch : c.second.children) out << "Child of " << c.first << ": " << ch << '\n'; } diff --git a/src/goto-programs/get_goto_model.cpp b/src/goto-programs/get_goto_model.cpp index fd47031a1f3..5afef435596 100644 --- a/src/goto-programs/get_goto_model.cpp +++ b/src/goto-programs/get_goto_model.cpp @@ -46,7 +46,7 @@ bool get_goto_modelt::operator()(const std::vector &files) binaries.reserve(files.size()); sources.reserve(files.size()); - for(const auto & file : files) + for(const auto &file : files) { if(is_goto_binary(file)) binaries.push_back(file); @@ -60,7 +60,7 @@ bool get_goto_modelt::operator()(const std::vector &files) language_files.set_message_handler(get_message_handler()); - for(const auto & filename : sources) + for(const auto &filename : sources) { #ifdef _MSC_VER std::ifstream infile(widen(filename)); @@ -122,11 +122,11 @@ bool get_goto_modelt::operator()(const std::vector &files) } } - for(const auto & it : binaries) + for(const auto &file : binaries) { status() << "Reading GOTO program from file" << eom; - if(read_object_and_link(it, *this, get_message_handler())) + if(read_object_and_link(file, *this, get_message_handler())) return true; } diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 2a1c8bad6f5..e161fe0a5bc 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -59,9 +59,9 @@ Function: goto_convertt::finish_gotos void goto_convertt::finish_gotos() { - for(const auto & it : targets.gotos) + for(const auto &g_it : targets.gotos) { - goto_programt::instructiont &i=*it; + goto_programt::instructiont &i=*g_it; if(i.code.get_statement()=="non-deterministic-goto") { @@ -141,7 +141,7 @@ Function: goto_convertt::finish_computed_gotos void goto_convertt::finish_computed_gotos(goto_programt &goto_program) { - for(auto & g_it : targets.computed_gotos) + for(auto &g_it : targets.computed_gotos) { goto_programt::instructiont &i=*g_it; exprt destination=i.code.op0(); @@ -156,13 +156,10 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program) i.code=code_expressiont(pointer); // insert huge case-split - for(labelst::const_iterator - l_it=targets.labels.begin(); - l_it!=targets.labels.end(); - l_it++) + for(const auto &label : targets.labels) { exprt label_expr(ID_label, empty_typet()); - label_expr.set(ID_identifier, l_it->first); + label_expr.set(ID_identifier, label.first); equal_exprt guard; @@ -172,7 +169,7 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program) goto_programt::targett t= goto_program.insert_after(g_it); - t->make_goto(l_it->second); + t->make_goto(label.second); t->source_location=i.source_location; t->guard=guard; } @@ -1434,16 +1431,16 @@ void goto_convertt::convert_switch( goto_programt tmp_cases; - for(auto & it : targets.cases) + for(auto &case_pair : targets.cases) { - const caset &case_ops=it.second; + const caset &case_ops=case_pair.second; assert(!case_ops.empty()); exprt guard_expr=case_guard(argument, case_ops); goto_programt::targett x=tmp_cases.add_instruction(); - x->make_goto(it.first); + x->make_goto(case_pair.first); x->guard.swap(guard_expr); x->source_location=case_ops.front().find_source_location(); } diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index c6d7be47258..c4ec6ea43c7 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -86,12 +86,9 @@ void goto_convert_functionst::goto_convert() symbol_list.push_back(it->first); } - for(symbol_listt::const_iterator - it=symbol_list.begin(); - it!=symbol_list.end(); - it++) + for(const auto &id : symbol_list) { - convert_function(*it); + convert_function(id); } functions.compute_location_numbers(); @@ -122,19 +119,11 @@ Function: goto_convert_functionst::hide bool goto_convert_functionst::hide(const goto_programt &goto_program) { - for(goto_programt::instructionst::const_iterator - i_it=goto_program.instructions.begin(); - i_it!=goto_program.instructions.end(); - i_it++) + forall_goto_program_instructions(i_it, goto_program) { - for(goto_programt::instructiont::labelst::const_iterator - l_it=i_it->labels.begin(); - l_it!=i_it->labels.end(); - l_it++) - { - if(*l_it=="__CPROVER_HIDE") + for(const auto &label : i_it->labels) + if(label=="__CPROVER_HIDE") return true; - } } return false; diff --git a/src/goto-programs/goto_convert_new_switch_case.cpp b/src/goto-programs/goto_convert_new_switch_case.cpp index 1bbde509419..bc6ebcc05b6 100644 --- a/src/goto-programs/goto_convert_new_switch_case.cpp +++ b/src/goto-programs/goto_convert_new_switch_case.cpp @@ -59,11 +59,9 @@ Function: goto_convertt::finish_gotos void goto_convertt::finish_gotos() { - for(gotost::const_iterator it=targets.gotos.begin(); - it!=targets.gotos.end(); - it++) + for(const auto &target : targets.gotos) { - goto_programt::instructiont &i=**it; + goto_programt::instructiont &i=*target; if(i.code.get_statement()=="non-deterministic-goto") { @@ -146,12 +144,9 @@ Function: goto_convertt::finish_computed_gotos void goto_convertt::finish_computed_gotos(goto_programt &goto_program) { - for(computed_gotost::const_iterator - g_it=targets.computed_gotos.begin(); - g_it!=targets.computed_gotos.end(); - g_it++) + for(const auto &target : targets.computed_gotos) { - goto_programt::instructiont &i=**g_it; + goto_programt::instructiont &i=*target; exprt destination=i.code.op0(); assert(destination.id()==ID_dereference); @@ -164,13 +159,10 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program) i.code=code_expressiont(pointer); // insert huge case-split - for(labelst::const_iterator - l_it=targets.labels.begin(); - l_it!=targets.labels.end(); - l_it++) + for(const auto &label : targets.labels) { exprt label_expr(ID_label, empty_typet()); - label_expr.set(ID_identifier, l_it->first); + label_expr.set(ID_identifier, label.first); equal_exprt guard; @@ -178,9 +170,9 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program) guard.rhs()=address_of_exprt(label_expr); goto_programt::targett t= - goto_program.insert_after(*g_it); + goto_program.insert_after(target); - t->make_goto(l_it->second); + t->make_goto(label.second); t->source_location=i.source_location; t->guard=guard; } diff --git a/src/goto-programs/goto_functions.cpp b/src/goto-programs/goto_functions.cpp index ceec1cf97f0..3e3d7d966d8 100644 --- a/src/goto-programs/goto_functions.cpp +++ b/src/goto-programs/goto_functions.cpp @@ -32,12 +32,9 @@ void get_local_identifiers( goto_function.type.parameters(); // add parameters - for(code_typet::parameterst::const_iterator - a_it=parameters.begin(); - a_it!=parameters.end(); - a_it++) + for(const auto ¶m : parameters) { - const irep_idt &identifier=a_it->get_identifier(); + const irep_idt &identifier=param.get_identifier(); if(identifier!="") dest.insert(identifier); } } diff --git a/src/goto-programs/goto_functions_template.h b/src/goto-programs/goto_functions_template.h index 6f33cfc1613..44f7f6b1e49 100644 --- a/src/goto-programs/goto_functions_template.h +++ b/src/goto-programs/goto_functions_template.h @@ -132,11 +132,8 @@ class goto_functions_templatet void copy_from(const goto_functions_templatet &other) { - for(typename function_mapt::const_iterator - f_it=other.function_map.begin(); - f_it!=other.function_map.end(); - f_it++) - function_map[f_it->first].copy_from(f_it->second); + for(const auto &fun : other.function_map) + function_map[fun.first].copy_from(fun.second); } }; @@ -158,18 +155,15 @@ void goto_functions_templatet::output( const namespacet &ns, std::ostream& out) const { - for(typename function_mapt::const_iterator - it=function_map.begin(); - it!=function_map.end(); - it++) + for(const auto &fun : function_map) { - if(it->second.body_available()) + if(fun.second.body_available()) { out << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n"; - const symbolt &symbol=ns.lookup(it->first); + const symbolt &symbol=ns.lookup(fun.first); out << symbol.display_name() << " /* " << symbol.name << " */\n"; - it->second.body.output(ns, symbol.name, out); + fun.second.body.output(ns, symbol.name, out); out << std::flush; } diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp index 21fd341d538..765aa290d7c 100644 --- a/src/goto-programs/goto_inline.cpp +++ b/src/goto-programs/goto_inline.cpp @@ -45,13 +45,8 @@ void goto_inlinet::parameter_assignments( code_type.parameters(); // iterates over the types of the parameters - for(code_typet::parameterst::const_iterator - it2=parameter_types.begin(); - it2!=parameter_types.end(); - it2++) + for(const auto ¶meter : parameter_types) { - const code_typet::parametert ¶meter=*it2; - // this is the type the n-th argument should be const typet &par_type=ns.follow(parameter.type()); @@ -179,13 +174,8 @@ void goto_inlinet::parameter_destruction( code_type.parameters(); // iterates over the types of the parameters - for(code_typet::parameterst::const_iterator - it=parameter_types.begin(); - it!=parameter_types.end(); - it++) + for(const auto ¶meter : parameter_types) { - const code_typet::parametert ¶meter=*it; - const irep_idt &identifier=parameter.get_identifier(); if(identifier==irep_idt()) diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index f914488310a..82f59d7988a 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -44,13 +44,8 @@ std::ostream& goto_programt::output_instruction( if(!it->labels.empty()) { out << " // Labels:"; - for(instructiont::labelst::const_iterator - l_it=it->labels.begin(); - l_it!=it->labels.end(); - l_it++) - { - out << " " << *l_it; - } + for(const auto &label : it->labels) + out << " " << label; out << '\n'; } @@ -133,11 +128,8 @@ std::ostream& goto_programt::output_instruction( const irept::subt &exception_list= it->code.find(ID_exception_list).get_sub(); - for(irept::subt::const_iterator - it=exception_list.begin(); - it!=exception_list.end(); - it++) - out << " " << it->id(); + for(const auto &ex : exception_list) + out << " " << ex.id(); } if(it->code.operands().size()==1) diff --git a/src/goto-programs/goto_program_irep.cpp b/src/goto-programs/goto_program_irep.cpp index efc76ea3069..2f9f491d58e 100644 --- a/src/goto-programs/goto_program_irep.cpp +++ b/src/goto-programs/goto_program_irep.cpp @@ -43,12 +43,9 @@ void convert(const goto_programt::instructiont &instruction, irept &irep) if(!instruction.targets.empty()) { irept &tgts=irep.add(ID_targets); - for(goto_programt::targetst::const_iterator it= - instruction.targets.begin(); - it!=instruction.targets.end(); - it++) + for(const auto &target : instruction.targets) { - irept t(std::to_string((*it)->location_number)); + irept t(std::to_string(target->location_number)); tgts.move_to_sub(t); } } @@ -58,12 +55,9 @@ void convert(const goto_programt::instructiont &instruction, irept &irep) irept &lbls = irep.add(ID_labels); irept::subt &subs = lbls.get_sub(); subs.reserve(instruction.labels.size()); - for(goto_programt::instructiont::labelst::const_iterator it= - instruction.labels.begin(); - it!=instruction.labels.end(); - it++) + for(const auto &label : instruction.labels) { - subs.push_back(irept(*it)); + subs.push_back(irept(label)); } } } @@ -95,12 +89,8 @@ void convert( const irept &lbls=irep.find(ID_labels); const irept::subt &lsubs=lbls.get_sub(); - for (irept::subt::const_iterator it=lsubs.begin(); - it!=lsubs.end(); - it++) - { - instruction.labels.push_back(it->id()); - } + for(const auto &lsub : lsubs) + instruction.labels.push_back(lsub.id()); } /*******************************************************************\ @@ -119,10 +109,7 @@ void convert( const goto_programt &program, irept &irep ) { irep.id("goto-program"); irep.get_sub().reserve(program.instructions.size()); - for (goto_programt::instructionst::const_iterator it= - program.instructions.begin(); - it!=program.instructions.end(); - it++) + forall_goto_program_instructions(it, program) { irep.get_sub().push_back(irept()); convert(*it, irep.get_sub().back()); @@ -161,13 +148,9 @@ void convert( const irept &irep, goto_programt &program ) number_targets_list.push_back(std::list()); const irept &targets=it->find(ID_targets); const irept::subt &tsubs=targets.get_sub(); - for (irept::subt::const_iterator tit=tsubs.begin(); - tit!=tsubs.end(); - tit++) - { + for (const auto & tsub : tsubs) number_targets_list.back().push_back( - unsafe_string2unsigned(tit->id_string())); - } + unsafe_string2unsigned(tsub.id_string())); } program.compute_location_numbers(); @@ -180,14 +163,12 @@ void convert( const irept &irep, goto_programt &program ) lit!=program.instructions.end() && nit!=number_targets_list.end(); lit++, nit++) { - for (std::list::iterator tit=nit->begin(); - tit!=nit->end(); - tit++) + for(const unsigned t : *nit) { goto_programt::targett fit=program.instructions.begin(); for(;fit!=program.instructions.end();fit++) { - if (fit->location_number==*tit) + if (fit->location_number==t) { lit->targets.push_back(fit); break; diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index 2dfc24ebc77..e8ae0f7eeb3 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -234,7 +234,7 @@ class goto_program_templatet { if(!is_goto()) return false; - for(const auto & t : targets) + for(const auto &t : targets) if(t->location_number<=location_number) return true; @@ -399,7 +399,7 @@ class goto_program_templatet //! Compute location numbers void compute_location_numbers(unsigned &nr) { - for(auto & i : instructions) + for(auto &i : instructions) i.location_number=nr++; } @@ -461,7 +461,7 @@ template void goto_program_templatet::compute_loop_numbers() { unsigned nr=0; - for(auto & i : instructions) + for(auto &i : instructions) if(i.is_backwards_goto()) i.loop_number=nr++; } @@ -481,7 +481,7 @@ void goto_program_templatet::get_successors( if(i.is_goto()) { - for(const auto & t : i.targets) + for(const auto &t : i.targets) successors.push_back(t); if(!i.guard.is_true() && next!=instructions.end()) @@ -489,7 +489,7 @@ void goto_program_templatet::get_successors( } else if(i.is_start_thread()) { - for(const auto & t : i.targets) + for(const auto &t : i.targets) successors.push_back(t); if(next!=instructions.end()) @@ -530,7 +530,7 @@ void goto_program_templatet::get_successors( if(i.is_goto()) { - for(const auto & t : i.targets) + for(const auto &t : i.targets) successors.push_back(t); if(!i.guard.is_true() && next!=instructions.end()) @@ -538,7 +538,7 @@ void goto_program_templatet::get_successors( } else if(i.is_start_thread()) { - for(const auto & t : i.targets) + for(const auto &t : i.targets) successors.push_back(t); if(next!=instructions.end()) @@ -593,14 +593,14 @@ void goto_program_templatet::compute_target_numbers() { // reset marking - for(auto & i : instructions) + for(auto &i : instructions) i.target_number=instructiont::nil_target; // mark the goto targets - for(const auto & i : instructions) + for(const auto &i : instructions) { - for(const auto & t : i.targets) + for(const auto &t : i.targets) { if(t!=instructions.end()) t->target_number=0; @@ -622,9 +622,9 @@ void goto_program_templatet::compute_target_numbers() // check the targets! // (this is a consistency check only) - for(const auto & i : instructions) + for(const auto &i : instructions) { - for(const auto & t : i.targets) + for(const auto &t : i.targets) { if(t!=instructions.end()) { @@ -660,9 +660,9 @@ void goto_program_templatet::copy_from( // Loop over program - 2nd time updates targets - for(auto & i : instructions) + for(auto &i : instructions) { - for(auto & t : i.targets) + for(auto &t : i.targets) { typename targets_mappingt::iterator m_target_it=targets_mapping.find(t); @@ -682,7 +682,7 @@ void goto_program_templatet::copy_from( template bool goto_program_templatet::has_assertion() const { - for(const auto & i : instructions) + for(const auto &i : instructions) if(i.is_assert() && !i.guard.is_true()) return true; @@ -692,7 +692,7 @@ bool goto_program_templatet::has_assertion() const template void goto_program_templatet::compute_incoming_edges() { - for(auto & i : instructions) + for(auto &i : instructions) { i.incoming_edges.clear(); } @@ -706,7 +706,7 @@ void goto_program_templatet::compute_incoming_edges() get_successors(it, successors); - for(const auto & s : successors) + for(const auto &s : successors) { if(s!=instructions.end()) s->incoming_edges.insert(it); diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index c27607129a2..c05d6a4efdc 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -35,10 +35,8 @@ void goto_tracet::output( const class namespacet &ns, std::ostream &out) const { - for(stepst::const_iterator it=steps.begin(); - it!=steps.end(); - it++) - it->output(ns, out); + for(const auto &step : steps) + step.output(ns, out); } /*******************************************************************\ @@ -322,43 +320,40 @@ void show_goto_trace( unsigned prev_step_nr=0; bool first_step=true; - for(goto_tracet::stepst::const_iterator - it=goto_trace.steps.begin(); - it!=goto_trace.steps.end(); - it++) + for(const auto &step : goto_trace.steps) { // hide the hidden ones - if(it->hidden) + if(step.hidden) continue; - switch(it->type) + switch(step.type) { case goto_trace_stept::ASSERT: - if(!it->cond_value) + if(!step.cond_value) { out << "\n"; out << "Violated property:" << "\n"; - if(!it->pc->source_location.is_nil()) - out << " " << it->pc->source_location << "\n"; - out << " " << it->comment << "\n"; + if(!step.pc->source_location.is_nil()) + out << " " << step.pc->source_location << "\n"; + out << " " << step.comment << "\n"; - if(it->pc->is_assert()) - out << " " << from_expr(ns, "", it->pc->guard) << "\n"; + if(step.pc->is_assert()) + out << " " << from_expr(ns, "", step.pc->guard) << "\n"; out << "\n"; } break; case goto_trace_stept::ASSUME: - if(!it->cond_value) + if(!step.cond_value) { out << "\n"; out << "Violated assumption:" << "\n"; - if(!it->pc->source_location.is_nil()) - out << " " << it->pc->source_location << "\n"; + if(!step.pc->source_location.is_nil()) + out << " " << step.pc->source_location << "\n"; - if(it->pc->is_assume()) - out << " " << from_expr(ns, "", it->pc->guard) << "\n"; + if(step.pc->is_assume()) + out << " " << from_expr(ns, "", step.pc->guard) << "\n"; out << "\n"; } @@ -371,56 +366,56 @@ void show_goto_trace( break; case goto_trace_stept::ASSIGNMENT: - if(it->pc->is_assign() || - it->pc->is_return() || // returns have a lhs! - it->pc->is_function_call() || - (it->pc->is_other() && it->lhs_object.is_not_nil())) + if(step.pc->is_assign() || + step.pc->is_return() || // returns have a lhs! + step.pc->is_function_call() || + (step.pc->is_other() && step.lhs_object.is_not_nil())) { - if(prev_step_nr!=it->step_nr || first_step) + if(prev_step_nr!=step.step_nr || first_step) { first_step=false; - prev_step_nr=it->step_nr; - show_state_header(out, *it, it->pc->source_location, it->step_nr); + prev_step_nr=step.step_nr; + show_state_header(out, step, step.pc->source_location, step.step_nr); } // see if the full lhs is something clean - if(is_index_member_symbol(it->full_lhs)) - trace_value(out, ns, it->lhs_object, it->full_lhs, it->full_lhs_value); + if(is_index_member_symbol(step.full_lhs)) + trace_value(out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value); else - trace_value(out, ns, it->lhs_object, it->lhs_object, it->lhs_object_value); + trace_value(out, ns, step.lhs_object, step.lhs_object, step.lhs_object_value); } break; case goto_trace_stept::DECL: - if(prev_step_nr!=it->step_nr || first_step) + if(prev_step_nr!=step.step_nr || first_step) { first_step=false; - prev_step_nr=it->step_nr; - show_state_header(out, *it, it->pc->source_location, it->step_nr); + prev_step_nr=step.step_nr; + show_state_header(out, step, step.pc->source_location, step.step_nr); } - trace_value(out, ns, it->lhs_object, it->full_lhs, it->full_lhs_value); + trace_value(out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value); break; case goto_trace_stept::OUTPUT: - if(it->formatted) + if(step.formatted) { printf_formattert printf_formatter(ns); - printf_formatter(id2string(it->format_string), it->io_args); + printf_formatter(id2string(step.format_string), step.io_args); printf_formatter.print(out); out << "\n"; } else { - show_state_header(out, *it, it->pc->source_location, it->step_nr); - out << " OUTPUT " << it->io_id << ":"; + show_state_header(out, step, step.pc->source_location, step.step_nr); + out << " OUTPUT " << step.io_id << ":"; for(std::list::const_iterator - l_it=it->io_args.begin(); - l_it!=it->io_args.end(); + l_it=step.io_args.begin(); + l_it!=step.io_args.end(); l_it++) { - if(l_it!=it->io_args.begin()) out << ";"; + if(l_it!=step.io_args.begin()) out << ";"; out << " " << from_expr(ns, "", *l_it); // the binary representation @@ -432,15 +427,15 @@ void show_goto_trace( break; case goto_trace_stept::INPUT: - show_state_header(out, *it, it->pc->source_location, it->step_nr); - out << " INPUT " << it->io_id << ":"; + show_state_header(out, step, step.pc->source_location, step.step_nr); + out << " INPUT " << step.io_id << ":"; for(std::list::const_iterator - l_it=it->io_args.begin(); - l_it!=it->io_args.end(); + l_it=step.io_args.begin(); + l_it!=step.io_args.end(); l_it++) { - if(l_it!=it->io_args.begin()) out << ";"; + if(l_it!=step.io_args.begin()) out << ";"; out << " " << from_expr(ns, "", *l_it); // the binary representation diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index eeade00ea04..664580ec397 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -117,7 +117,7 @@ std::string graphml_witnesst::convert_assign_rec( exprt::operandst::const_iterator it= assign.rhs().operands().begin(); - for(const auto & comp : components) + for(const auto &comp : components) { if(comp.type().id()==ID_code || comp.get_is_padding() || diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index d4cfef09b85..c6f80260dbe 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -453,12 +453,8 @@ void interpretert::execute_function_call() std::set locals; get_local_identifiers(f_it->second, locals); - for(std::set::const_iterator - it=locals.begin(); - it!=locals.end(); - it++) + for(const auto &id : locals) { - const irep_idt &id=*it; const symbolt &symbol=ns.lookup(id); unsigned size=get_size(symbol.type); @@ -523,11 +519,8 @@ void interpretert::build_memory_map() memory[0].identifier="NULL-OBJECT"; // now do regular static symbols - for(symbol_tablet::symbolst::const_iterator - it=symbol_table.symbols.begin(); - it!=symbol_table.symbols.end(); - it++) - build_memory_map(it->second); + for(const auto &s : symbol_table.symbols) + build_memory_map(s.second); // for the locals stack_pointer=memory.size(); @@ -595,12 +588,9 @@ unsigned interpretert::get_size(const typet &type) const unsigned sum=0; - for(struct_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - it++) + for(const auto &comp : components) { - const typet &sub_type=it->type(); + const typet &sub_type=comp.type(); if(sub_type.id()!=ID_code) sum+=get_size(sub_type); @@ -615,12 +605,9 @@ unsigned interpretert::get_size(const typet &type) const unsigned max_size=0; - for(union_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - it++) + for(const auto &comp : components) { - const typet &sub_type=it->type(); + const typet &sub_type=comp.type(); if(sub_type.id()!=ID_code) max_size=std::max(max_size, get_size(sub_type)); diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index f402d077bfc..57c761ebc6a 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -492,18 +492,12 @@ mp_integer interpretert::evaluate_address(const exprt &expr) const unsigned offset=0; - const struct_typet::componentst &components= - struct_type.components(); - - for(struct_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - it++) + for(const auto &comp : struct_type.components()) { - if(it->get_name()==component_name) + if(comp.get_name()==component_name) break; - offset+=get_size(it->type()); + offset+=get_size(comp.type()); } return evaluate_address(expr.op0())+offset; diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index 48964921aa7..4d4239ef182 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -37,9 +37,9 @@ void convert( source_locationt previous_source_location; - for(const auto & it : goto_trace.steps) + for(const auto &step : goto_trace.steps) { - const source_locationt &source_location=it.pc->source_location; + const source_locationt &source_location=step.pc->source_location; jsont json_location; @@ -48,28 +48,28 @@ void convert( else json_location=json_nullt(); - switch(it.type) + switch(step.type) { case goto_trace_stept::ASSERT: - if(!it.cond_value) + if(!step.cond_value) { irep_idt property_id; - if(it.pc->is_assert()) + if(step.pc->is_assert()) property_id=source_location.get_property_id(); - else if(it.pc->is_goto()) // unwinding, we suspect + else if(step.pc->is_goto()) // unwinding, we suspect { property_id= - id2string(it.pc->source_location.get_function())+".unwind."+ - std::to_string(it.pc->loop_number); + id2string(step.pc->source_location.get_function())+ + ".unwind."+std::to_string(step.pc->loop_number); } json_objectt &json_failure=dest_array.push_back().make_object(); json_failure["stepType"]=json_stringt("failure"); - json_failure["hidden"]=jsont::json_boolean(it.hidden); - json_failure["thread"]=json_numbert(std::to_string(it.thread_nr)); - json_failure["reason"]=json_stringt(id2string(it.comment)); + json_failure["hidden"]=jsont::json_boolean(step.hidden); + json_failure["thread"]=json_numbert(std::to_string(step.thread_nr)); + json_failure["reason"]=json_stringt(id2string(step.comment)); json_failure["property"]=json_stringt(id2string(property_id)); if(!json_location.is_null()) @@ -80,7 +80,7 @@ void convert( case goto_trace_stept::ASSIGNMENT: case goto_trace_stept::DECL: { - irep_idt identifier=it.lhs_object.get_identifier(); + irep_idt identifier=step.lhs_object.get_identifier(); json_objectt &json_assignment=dest_array.push_back().make_object(); json_assignment["stepType"]=json_stringt("assignment"); @@ -91,16 +91,16 @@ void convert( std::string value_string, binary_string, type_string, full_lhs_string; json_objectt full_lhs_value; - if(it.full_lhs.is_not_nil()) - full_lhs_string=from_expr(ns, identifier, it.full_lhs); + if(step.full_lhs.is_not_nil()) + full_lhs_string=from_expr(ns, identifier, step.full_lhs); #if 0 if(it.full_lhs_value.is_not_nil()) full_lhs_value_string=from_expr(ns, identifier, it.full_lhs_value); #endif - if(it.full_lhs_value.is_not_nil()) - full_lhs_value = json(it.full_lhs_value, ns); + if(step.full_lhs_value.is_not_nil()) + full_lhs_value = json(step.full_lhs_value, ns); const symbolt *symbol; irep_idt base_name, display_name; @@ -117,11 +117,11 @@ void convert( json_assignment["value"]=full_lhs_value; json_assignment["lhs"]=json_stringt(full_lhs_string); - json_assignment["hidden"]=jsont::json_boolean(it.hidden); - json_assignment["thread"]=json_numbert(std::to_string(it.thread_nr)); + json_assignment["hidden"]=jsont::json_boolean(step.hidden); + json_assignment["thread"]=json_numbert(std::to_string(step.thread_nr)); json_assignment["assignmentType"]= - json_stringt(it.assignment_type==goto_trace_stept::ACTUAL_PARAMETER? + json_stringt(step.assignment_type==goto_trace_stept::ACTUAL_PARAMETER? "actual-parameter":"variable"); } break; @@ -131,18 +131,18 @@ void convert( json_objectt &json_output=dest_array.push_back().make_object(); json_output["stepType"]=json_stringt("output"); - json_output["hidden"]=jsont::json_boolean(it.hidden); - json_output["thread"]=json_numbert(std::to_string(it.thread_nr)); - json_output["outputID"]=json_stringt(id2string(it.io_id)); + json_output["hidden"]=jsont::json_boolean(step.hidden); + json_output["thread"]=json_numbert(std::to_string(step.thread_nr)); + json_output["outputID"]=json_stringt(id2string(step.io_id)); json_arrayt &json_values=json_output["values"].make_array(); - for(const auto l_it : it.io_args) + for(const auto &arg : step.io_args) { - if(l_it.is_nil()) + if(arg.is_nil()) json_values.push_back(json_stringt("")); else - json_values.push_back(json(l_it, ns)); + json_values.push_back(json(arg, ns)); } if(!json_location.is_null()) @@ -155,18 +155,18 @@ void convert( json_objectt &json_input=dest_array.push_back().make_object(); json_input["stepType"]=json_stringt("input"); - json_input["hidden"]=jsont::json_boolean(it.hidden); - json_input["thread"]=json_numbert(std::to_string(it.thread_nr)); - json_input["inputID"]=json_stringt(id2string(it.io_id)); + json_input["hidden"]=jsont::json_boolean(step.hidden); + json_input["thread"]=json_numbert(std::to_string(step.thread_nr)); + json_input["inputID"]=json_stringt(id2string(step.io_id)); json_arrayt &json_values=json_input["values"].make_array(); - for(const auto l_it : it.io_args) + for(const auto &arg : step.io_args) { - if(l_it.is_nil()) + if(arg.is_nil()) json_values.push_back(json_stringt("")); else - json_values.push_back(json(l_it, ns)); + json_values.push_back(json(arg, ns)); } if(!json_location.is_null()) @@ -178,19 +178,19 @@ void convert( case goto_trace_stept::FUNCTION_RETURN: { std::string tag= - (it.type==goto_trace_stept::FUNCTION_CALL)? + (step.type==goto_trace_stept::FUNCTION_CALL)? "function-call":"function-return"; json_objectt &json_call_return=dest_array.push_back().make_object(); json_call_return["stepType"]=json_stringt(tag); - json_call_return["hidden"]=jsont::json_boolean(it.hidden); - json_call_return["thread"]=json_numbert(std::to_string(it.thread_nr)); + json_call_return["hidden"]=jsont::json_boolean(step.hidden); + json_call_return["thread"]=json_numbert(std::to_string(step.thread_nr)); - const symbolt &symbol=ns.lookup(it.identifier); + const symbolt &symbol=ns.lookup(step.identifier); json_objectt &json_function=json_call_return["function"].make_object(); json_function["displayName"]= json_stringt(id2string(symbol.display_name())); - json_function["identifier"]=json_stringt(id2string(it.identifier)); + json_function["identifier"]=json_stringt(id2string(step.identifier)); json_function["sourceLocation"]=json(symbol.location); if(!json_location.is_null()) @@ -206,8 +206,8 @@ void convert( { json_objectt &json_location_only=dest_array.push_back().make_object(); json_location_only["stepType"]=json_stringt("location-only"); - json_location_only["hidden"]=jsont::json_boolean(it.hidden); - json_location_only["thread"]=json_numbert(std::to_string(it.thread_nr)); + json_location_only["hidden"]=jsont::json_boolean(step.hidden); + json_location_only["thread"]=json_numbert(std::to_string(step.thread_nr)); json_location_only["sourceLocation"]=json_location; } } diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp index edfe507f651..83ff6015f88 100644 --- a/src/goto-programs/link_to_library.cpp +++ b/src/goto-programs/link_to_library.cpp @@ -65,25 +65,22 @@ void link_to_library( std::set missing_functions; - for(std::set::const_iterator - it=called_functions.begin(); - it!=called_functions.end(); - it++) + for(const auto &id : called_functions) { goto_functionst::function_mapt::const_iterator - f_it=goto_functions.function_map.find(*it); + f_it=goto_functions.function_map.find(id); if(f_it!=goto_functions.function_map.end() && f_it->second.body_available()) { // it's overridden! } - else if(added_functions.find(*it)!=added_functions.end()) + else if(added_functions.find(id)!=added_functions.end()) { // already added } else - missing_functions.insert(*it); + missing_functions.insert(id); } // done? @@ -92,15 +89,12 @@ void link_to_library( add_cprover_library(missing_functions, symbol_table, message_handler); // convert to CFG - for(std::set::const_iterator - it=missing_functions.begin(); - it!=missing_functions.end(); - it++) + for(const auto &id : missing_functions) { - if(symbol_table.symbols.find(*it)!=symbol_table.symbols.end()) - goto_convert(*it, symbol_table, goto_functions, message_handler); + if(symbol_table.symbols.find(id)!=symbol_table.symbols.end()) + goto_convert(id, symbol_table, goto_functions, message_handler); - added_functions.insert(*it); + added_functions.insert(id); } } diff --git a/src/goto-programs/loop_ids.cpp b/src/goto-programs/loop_ids.cpp index 30c0ce838f0..e4e4a280a7a 100644 --- a/src/goto-programs/loop_ids.cpp +++ b/src/goto-programs/loop_ids.cpp @@ -54,9 +54,7 @@ void show_loop_ids( { case ui_message_handlert::PLAIN: { - for(goto_programt::instructionst::const_iterator - it=goto_program.instructions.begin(); - it!=goto_program.instructions.end(); it++) + forall_goto_program_instructions(it, goto_program) { if(it->is_backwards_goto()) { @@ -73,9 +71,7 @@ void show_loop_ids( } case ui_message_handlert::XML_UI: { - for(goto_programt::instructionst::const_iterator - it=goto_program.instructions.begin(); - it!=goto_program.instructions.end(); it++) + forall_goto_program_instructions(it, goto_program) { if(it->is_backwards_goto()) { @@ -103,9 +99,7 @@ void show_loop_ids_json( { assert(ui==ui_message_handlert::JSON_UI); //use function above - for(goto_programt::instructionst::const_iterator - it=goto_program.instructions.begin(); - it!=goto_program.instructions.end(); it++) + forall_goto_program_instructions(it, goto_program) { if(it->is_backwards_goto()) { diff --git a/src/goto-programs/property_checker.cpp b/src/goto-programs/property_checker.cpp index f94d94f4dc5..01c8d2f08ae 100644 --- a/src/goto-programs/property_checker.cpp +++ b/src/goto-programs/property_checker.cpp @@ -66,30 +66,24 @@ Function: property_checkert::initialize_property_map void property_checkert::initialize_property_map( const goto_functionst &goto_functions) { - for(goto_functionst::function_mapt::const_iterator - it=goto_functions.function_map.begin(); - it!=goto_functions.function_map.end(); - it++) + forall_goto_functions(it, goto_functions) if(!it->second.is_inlined() || it->first==goto_functions.entry_point()) { const goto_programt &goto_program=it->second.body; - for(goto_programt::instructionst::const_iterator - it=goto_program.instructions.begin(); - it!=goto_program.instructions.end(); - it++) + forall_goto_program_instructions(i_it, goto_program) { - if(!it->is_assert()) + if(!i_it->is_assert()) continue; - const source_locationt &source_location=it->source_location; + const source_locationt &source_location=i_it->source_location; irep_idt property_id=source_location.get_property_id(); property_statust &property_status=property_map[property_id]; property_status.result=UNKNOWN; - property_status.location=it; + property_status.location=i_it; } } } diff --git a/src/goto-programs/remove_asm.cpp b/src/goto-programs/remove_asm.cpp index ef35f700f36..11cc5ce94a1 100644 --- a/src/goto-programs/remove_asm.cpp +++ b/src/goto-programs/remove_asm.cpp @@ -154,22 +154,15 @@ void remove_asmt::process_instruction( bool unknown=false; bool x86_32_locked_atomic=false; - for(std::list::const_iterator - it=assembler_parser.instructions.begin(); - it!=assembler_parser.instructions.end(); - it++) + for(const auto &instruction : assembler_parser.instructions) { - const assembler_parsert::instructiont &instruction=*it; if(instruction.empty()) continue; #if 0 std::cout << "A ********************\n"; - for(assembler_parsert::instructiont::const_iterator - t_it=instruction.begin(); - t_it!=instruction.end(); - t_it++) + for(const auto &ins : instruction) { - std::cout << "XX: " << t_it->pretty() << std::endl; + std::cout << "XX: " << ins.pretty() << std::endl; } std::cout << "B ********************\n"; diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index a58770bd1c8..7a25def3823 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -76,11 +76,8 @@ class remove_function_pointerst { const symbol_tablet &symbol_table=ns.get_symbol_table(); - const symbol_tablet::symbolst &s=symbol_table.symbols; - - for(symbol_tablet::symbolst::const_iterator - it=s.begin(); it!=s.end(); ++it) - compute_address_taken_functions(it->second.value, address_taken); + for(const auto &s : symbol_table.symbols) + compute_address_taken_functions(s.second.value, address_taken); } }; @@ -109,10 +106,7 @@ remove_function_pointerst::remove_function_pointerst( compute_address_taken_functions(goto_functions, address_taken); // build type map - for(goto_functionst::function_mapt::const_iterator f_it= - goto_functions.function_map.begin(); - f_it!=goto_functions.function_map.end(); - f_it++) + forall_goto_functions(f_it, goto_functions) type_map[f_it->first]=f_it->second.type; } @@ -386,25 +380,22 @@ void remove_function_pointerst::remove_function_pointer( // get all type-compatible functions // whose address is ever taken - for(type_mapt::const_iterator f_it= - type_map.begin(); - f_it!=type_map.end(); - f_it++) + for(const auto &t : type_map) { // address taken? - if(address_taken.find(f_it->first)==address_taken.end()) + if(address_taken.find(t.first)==address_taken.end()) continue; // type-compatible? - if(!is_type_compatible(return_value_used, call_type, f_it->second)) + if(!is_type_compatible(return_value_used, call_type, t.second)) continue; - if(f_it->first=="pthread_mutex_cleanup") + if(t.first=="pthread_mutex_cleanup") continue; symbol_exprt expr; - expr.type()=f_it->second; - expr.set_identifier(f_it->first); + expr.type()=t.second; + expr.set_identifier(t.first); functions.push_back(expr); } @@ -419,15 +410,12 @@ void remove_function_pointerst::remove_function_pointer( goto_programt new_code_calls; goto_programt new_code_gotos; - for(functionst::const_iterator - it=functions.begin(); - it!=functions.end(); - it++) + for(const auto &fun : functions) { // call function goto_programt::targett t1=new_code_calls.add_instruction(); t1->make_function_call(code); - to_code_function_call(t1->code).function()=*it; + to_code_function_call(t1->code).function()=fun; // the signature of the function might not match precisely fix_argument_types(to_code_function_call(t1->code)); @@ -439,9 +427,9 @@ void remove_function_pointerst::remove_function_pointer( // goto to call address_of_exprt address_of; - address_of.object()=*it; + address_of.object()=fun; address_of.type()=pointer_typet(); - address_of.type().subtype()=it->type(); + address_of.type().subtype()=fun.type(); if(address_of.type()!=pointer.type()) address_of.make_typecast(pointer.type()); diff --git a/src/goto-programs/remove_skip.cpp b/src/goto-programs/remove_skip.cpp index b2b05e8305f..cb903fd0e0c 100644 --- a/src/goto-programs/remove_skip.cpp +++ b/src/goto-programs/remove_skip.cpp @@ -157,9 +157,8 @@ void remove_skip(goto_programt &goto_program) // now delete the skips -- we do so after adjusting the // gotos to avoid dangling targets - for(new_targetst::const_iterator - it=new_targets.begin(); it!=new_targets.end(); it++) - goto_program.instructions.erase(it->first); + for(const auto &new_target : new_targets) + goto_program.instructions.erase(new_target.first); // remove the last skip statement unless it's a target goto_program.compute_incoming_edges(); diff --git a/src/goto-programs/remove_unreachable.cpp b/src/goto-programs/remove_unreachable.cpp index 97f7f1191b1..38f8e93974a 100644 --- a/src/goto-programs/remove_unreachable.cpp +++ b/src/goto-programs/remove_unreachable.cpp @@ -42,11 +42,8 @@ void remove_unreachable(goto_programt &goto_program) goto_programt::targetst successors; goto_program.get_successors(t, successors); - for(goto_programt::targetst::const_iterator - s_it=successors.begin(); - s_it!=successors.end(); - s_it++) - working.push(*s_it); + for(const auto &succ : successors) + working.push(succ); } } diff --git a/src/goto-programs/remove_unused_functions.cpp b/src/goto-programs/remove_unused_functions.cpp index dcb1ec6d667..75b33c63095 100644 --- a/src/goto-programs/remove_unused_functions.cpp +++ b/src/goto-programs/remove_unused_functions.cpp @@ -49,11 +49,8 @@ void remove_unused_functions( used_functions.size() << " used)" << messaget::eom; } - for(std::list::const_iterator - it=unused_functions.begin(); - it!=unused_functions.end(); - it++) - functions.function_map.erase(*it); + for(const auto &f : unused_functions) + functions.function_map.erase(f); } /*******************************************************************\ diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 15d7583f074..a0d9f551c2e 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -170,15 +170,12 @@ void remove_virtual_functionst::remove_virtual_function( goto_programt new_code_calls; goto_programt new_code_gotos; - for(functionst::const_iterator - it=functions.begin(); - it!=functions.end(); - it++) + for(const auto &fun : functions) { // call function goto_programt::targett t1=new_code_calls.add_instruction(); t1->make_function_call(code); - to_code_function_call(t1->code).function()=it->symbol_expr; + to_code_function_call(t1->code).function()=fun.symbol_expr; // goto final goto_programt::targett t3=new_code_calls.add_instruction(); @@ -188,12 +185,12 @@ void remove_virtual_functionst::remove_virtual_function( if(this_expr.type().id()!=ID_pointer || this_expr.type().id()!=ID_struct) { - symbol_typet symbol_type(it->class_id); + symbol_typet symbol_type(fun.class_id); this_expr=typecast_exprt(this_expr, pointer_typet(symbol_type)); } exprt deref=dereference_exprt(this_expr, this_expr.type().subtype()); - exprt c_id1=constant_exprt(it->class_id, string_typet()); + exprt c_id1=constant_exprt(fun.class_id, string_typet()); exprt c_id2=build_class_identifier(deref); goto_programt::targett t4=new_code_gotos.add_instruction(); @@ -251,7 +248,7 @@ void remove_virtual_functionst::get_functions( std::vector children= class_hierarchy.get_children_trans(class_id); - for(const auto & child : children) + for(const auto &child : children) { exprt method=get_method(child, component_name); if(method.is_not_nil()) diff --git a/src/goto-programs/set_properties.cpp b/src/goto-programs/set_properties.cpp index 095fb43d235..4f345e5eab0 100644 --- a/src/goto-programs/set_properties.cpp +++ b/src/goto-programs/set_properties.cpp @@ -170,16 +170,9 @@ void set_properties( { std::unordered_set property_set; - for(std::list::const_iterator - it=properties.begin(); - it!=properties.end(); - it++) - property_set.insert(*it); + property_set.insert(properties.begin(), properties.end()); - for(goto_functionst::function_mapt::iterator - it=goto_functions.function_map.begin(); - it!=goto_functions.function_map.end(); - it++) + Forall_goto_functions(it, goto_functions) if(!it->second.is_inlined()) set_properties(it->second.body, property_set); diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp index ef600a748cc..99cdc36d84c 100644 --- a/src/goto-programs/show_goto_functions.cpp +++ b/src/goto-programs/show_goto_functions.cpp @@ -43,10 +43,7 @@ void show_goto_functions( { //This only prints the list of functions xmlt xml_functions("functions"); - for(goto_functionst::function_mapt::const_iterator - it=goto_functions.function_map.begin(); - it!=goto_functions.function_map.end(); - it++) + forall_goto_functions(it, goto_functions) { xmlt &xml_function=xml_functions.new_element("function"); xml_function.set_attribute("name", id2string(it->first)); @@ -60,10 +57,7 @@ void show_goto_functions( { //This only prints the list of functions json_arrayt json_functions; - for(goto_functionst::function_mapt::const_iterator - it=goto_functions.function_map.begin(); - it!=goto_functions.function_map.end(); - it++) + forall_goto_functions(it, goto_functions) { json_objectt &json_function= json_functions.push_back(jsont()).make_object(); diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index fb078873f1d..6deddc286da 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -37,12 +37,12 @@ void show_properties( ui_message_handlert::uit ui, const goto_programt &goto_program) { - for(const auto & it : goto_program.instructions) + for(const auto &ins : goto_program.instructions) { - if(!it.is_assert()) + if(!ins.is_assert()) continue; - const source_locationt &source_location=it.source_location; + const source_locationt &source_location=ins.source_location; const irep_idt &comment=source_location.get_comment(); //const irep_idt &function=location.get_function(); @@ -79,10 +79,11 @@ void show_properties( xml_property.set_attribute("class", id2string(property_class)); // use this one xmlt &property_l=xml_property.new_element(); - property_l=xml(it.source_location); + property_l=xml(source_location); xml_property.new_element("description").data=id2string(description); - xml_property.new_element("expression").data=from_expr(ns, identifier, it.guard); + xml_property.new_element("expression").data= + from_expr(ns, identifier, ins.guard); std::cout << xml_property << std::endl; } @@ -95,9 +96,10 @@ void show_properties( case ui_message_handlert::PLAIN: std::cout << "Property " << property_id << ":" << std::endl; - std::cout << " " << it.source_location << std::endl + std::cout << " " << ins.source_location << std::endl << " " << description << std::endl - << " " << from_expr(ns, identifier, it.guard) << std::endl; + << " " << from_expr(ns, identifier, ins.guard) + << std::endl; std::cout << std::endl; break; @@ -127,12 +129,12 @@ void show_properties_json( const irep_idt &identifier, const goto_programt &goto_program) { - for(const auto & it : goto_program.instructions) + for(const auto &ins : goto_program.instructions) { - if(!it.is_assert()) + if(!ins.is_assert()) continue; - const source_locationt &source_location=it.source_location; + const source_locationt &source_location=ins.source_location; const irep_idt &comment=source_location.get_comment(); //const irep_idt &function=location.get_function(); @@ -146,10 +148,10 @@ void show_properties_json( json_properties.push_back(jsont()).make_object(); json_property["name"]=json_stringt(id2string(property_id)); json_property["class"]=json_stringt(id2string(property_class)); - json_property["sourceLocation"]=json(it.source_location); + json_property["sourceLocation"]=json(source_location); json_property["description"]=json_stringt(id2string(description)); json_property["expression"]= - json_stringt(from_expr(ns, identifier, it.guard)); + json_stringt(from_expr(ns, identifier, ins.guard)); } } @@ -171,11 +173,13 @@ void show_properties_json( { json_arrayt json_properties; - for(const auto & it : goto_functions.function_map) - { - if(!it.second.is_inlined()) - show_properties_json(json_properties, ns, it.first, it.second.body); - } + for(const auto &fct : goto_functions.function_map) + if(!fct.second.is_inlined()) + show_properties_json( + json_properties, + ns, + fct.first, + fct.second.body); json_objectt json_result; json_result["properties"] = json_properties; @@ -202,9 +206,9 @@ void show_properties( if(ui == ui_message_handlert::JSON_UI) show_properties_json(ns, goto_functions); else - for(const auto & it : goto_functions.function_map) - if(!it.second.is_inlined()) - show_properties(ns, it.first, ui, it.second.body); + for(const auto &fct : goto_functions.function_map) + if(!fct.second.is_inlined()) + show_properties(ns, fct.first, ui, fct.second.body); } /*******************************************************************\ diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 3c5e736e2b8..114eddb2d3e 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -390,14 +390,12 @@ void string_abstractiont::declare_define_locals(goto_programt &dest) to_code_decl(it->code).get_identifier(), it)); // declare (and, if necessary, define) locals - for(localst::const_iterator l_it=locals.begin(); - l_it!=locals.end(); - ++l_it) + for(const auto &l : locals) { goto_programt::targett ref_instr=dest.instructions.begin(); bool has_decl=false; - available_declst::const_iterator entry=available_decls.find(l_it->first); + available_declst::const_iterator entry=available_decls.find(l.first); if(available_declst::const_iterator(available_decls.end())!=entry) { @@ -406,7 +404,7 @@ void string_abstractiont::declare_define_locals(goto_programt &dest) } goto_programt tmp; - make_decl_and_def(tmp, ref_instr, l_it->second, l_it->first); + make_decl_and_def(tmp, ref_instr, l.second, l.first); if(has_decl) ++ref_instr; dest.insert_before_swap(ref_instr, tmp); @@ -974,22 +972,17 @@ const typet& string_abstractiont::build_abstraction_type_rec(const typet &type, else if(eff_type.id()==ID_struct || eff_type.id()==ID_union) { const struct_union_typet &struct_union_type=to_struct_union_type(eff_type); - const struct_union_typet::componentst &components= - struct_union_type.components(); struct_union_typet::componentst new_comp; - for(struct_union_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - it++) + for(const auto &comp : struct_union_type.components()) { - if(it->get_anonymous()) continue; - typet subt=build_abstraction_type_rec(it->type(), known); + if(comp.get_anonymous()) continue; + typet subt=build_abstraction_type_rec(comp.type(), known); if(subt.is_nil()) continue; // also precludes structs with pointers to the same datatype new_comp.push_back(struct_union_typet::componentt()); - new_comp.back().set_name(it->get_name()); - new_comp.back().set_pretty_name(it->get_pretty_name()); + new_comp.back().set_name(comp.get_name()); + new_comp.back().set_pretty_name(comp.get_pretty_name()); new_comp.back().type()=subt; } if(!new_comp.empty()) @@ -1639,19 +1632,14 @@ goto_programt::targett string_abstractiont::value_assignments( else if(lhs.type().id()==ID_struct || lhs.type().id()==ID_union) { const struct_union_typet &struct_union_type=to_struct_union_type(lhs.type()); - const struct_union_typet::componentst &components= - struct_union_type.components(); - for(struct_union_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - it++) + for(const auto &comp : struct_union_type.components()) { - assert(!it->get_name().empty()); + assert(!comp.get_name().empty()); target=value_assignments(dest, target, - member_exprt(lhs, it->get_name(), it->type()), - member_exprt(rhs, it->get_name(), it->type())); + member_exprt(lhs, comp.get_name(), comp.type()), + member_exprt(rhs, comp.get_name(), comp.type())); } } diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp index 21f7e9367ed..d5a269a6018 100644 --- a/src/goto-programs/string_instrumentation.cpp +++ b/src/goto-programs/string_instrumentation.cpp @@ -527,11 +527,9 @@ void string_instrumentationt::do_format_string_read( unsigned args=0; - for(format_token_listt::const_iterator it=token_list.begin(); - it!=token_list.end(); - it++) + for(const auto &token : token_list) { - if(it->type==format_tokent::STRING) + if(token.type==format_tokent::STRING) { const exprt &arg = arguments[argument_start_inx+args]; const typet &arg_type = ns.follow(arg.type()); @@ -560,11 +558,11 @@ void string_instrumentationt::do_format_string_read( } } - if(it->type!=format_tokent::TEXT && - it->type!=format_tokent::UNKNOWN) args++; + if(token.type!=format_tokent::TEXT && + token.type!=format_tokent::UNKNOWN) args++; - if(find(it->flags.begin(), it->flags.end(), format_tokent::ASTERISK)!= - it->flags.end()) + if(find(token.flags.begin(), token.flags.end(), format_tokent::ASTERISK)!= + token.flags.end()) args++; // just eat the additional argument } } @@ -641,15 +639,13 @@ void string_instrumentationt::do_format_string_write( unsigned args=0; - for(format_token_listt::const_iterator it=token_list.begin(); - it!=token_list.end(); - it++) + for(const auto &token : token_list) { - if(find(it->flags.begin(), it->flags.end(), format_tokent::ASTERISK)!= - it->flags.end()) + if(find(token.flags.begin(), token.flags.end(), format_tokent::ASTERISK)!= + token.flags.end()) continue; // asterisk means `ignore this' - switch(it->type) + switch(token.type) { case format_tokent::STRING: { @@ -664,9 +660,9 @@ void string_instrumentationt::do_format_string_write( comment += function_name; assertion->source_location.set_comment(comment); - if(it->field_width!=0) + if(token.field_width!=0) { - exprt fwidth = from_integer(it->field_width, unsigned_int_type()); + exprt fwidth = from_integer(token.field_width, unsigned_int_type()); exprt fw_1(ID_plus, unsigned_int_type()); exprt one = gen_one(unsigned_int_type()); fw_1.move_to_operands(fwidth); @@ -694,7 +690,7 @@ void string_instrumentationt::do_format_string_write( } // now kill the contents - invalidate_buffer(dest, target, argument, arg_type, it->field_width); + invalidate_buffer(dest, target, argument, arg_type, token.field_width); args++; break; diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp index e4f7eec02bd..76446cfd095 100644 --- a/src/goto-programs/vcd_goto_trace.cpp +++ b/src/goto-programs/vcd_goto_trace.cpp @@ -85,14 +85,7 @@ std::string as_vcd_binary( width=pointer_offset_size(type, ns)*8; if(width>=0) - { - std::string result; - - for(; width!=0; --width) - result+='x'; - - return result; - } + return std::string(integer2size_t(width), 'x'); return ""; } @@ -125,12 +118,12 @@ void output_vcd( numbering n; - for(const auto & it : goto_trace.steps) + for(const auto &step : goto_trace.steps) { - if(it.is_assignment()) + if(step.is_assignment()) { - irep_idt identifier=it.lhs_object.get_identifier(); - const typet &type=it.lhs_object.type(); + irep_idt identifier=step.lhs_object.get_identifier(); + const typet &type=step.lhs_object.type(); const auto number=n.number(identifier); @@ -152,14 +145,14 @@ void output_vcd( unsigned timestamp=0; - for(const auto & it : goto_trace.steps) + for(const auto &step : goto_trace.steps) { - switch(it.type) + switch(step.type) { case goto_trace_stept::ASSIGNMENT: { - irep_idt identifier=it.lhs_object.get_identifier(); - const typet &type=it.lhs_object.type(); + irep_idt identifier=step.lhs_object.get_identifier(); + const typet &type=step.lhs_object.type(); out << '#' << timestamp << "\n"; timestamp++; @@ -169,16 +162,16 @@ void output_vcd( // booleans are special in VCD if(type.id()==ID_bool) { - if(it.lhs_object_value.is_true()) + if(step.lhs_object_value.is_true()) out << "1" << "V" << number << "\n"; - else if(it.lhs_object_value.is_false()) + else if(step.lhs_object_value.is_false()) out << "0" << "V" << number << "\n"; else out << "x" << "V" << number << "\n"; } else { - std::string binary=as_vcd_binary(it.lhs_object_value, ns); + std::string binary=as_vcd_binary(step.lhs_object_value, ns); if(binary!="") out << "b" << binary << " V" << number << " " << "\n"; diff --git a/src/goto-programs/write_goto_binary.cpp b/src/goto-programs/write_goto_binary.cpp index ff0a98790b3..021ba3e51bd 100644 --- a/src/goto-programs/write_goto_binary.cpp +++ b/src/goto-programs/write_goto_binary.cpp @@ -86,17 +86,17 @@ bool write_goto_binary_v3( write_gb_word(out, cnt); - for(const auto & it : functions.function_map) + for(const auto &fct : functions.function_map) { - if(it.second.body_available()) + if(fct.second.body_available()) { // Since version 2, goto functions are not converted to ireps, // instead they are saved in a custom binary format - write_gb_string(out, id2string(it.first)); // name - write_gb_word(out, it.second.body.instructions.size()); // # instructions + write_gb_string(out, id2string(fct.first)); // name + write_gb_word(out, fct.second.body.instructions.size()); // # instructions - forall_goto_program_instructions(i_it, it.second.body) + forall_goto_program_instructions(i_it, fct.second.body) { const goto_programt::instructiont &instruction = *i_it; @@ -110,12 +110,12 @@ bool write_goto_binary_v3( write_gb_word(out, instruction.targets.size()); - for(const auto & t_it : instruction.targets) + for(const auto &t_it : instruction.targets) write_gb_word(out, t_it->target_number); write_gb_word(out, instruction.labels.size()); - for(const auto & l_it : instruction.labels) + for(const auto &l_it : instruction.labels) irepconverter.write_string_ref(out, l_it); } } diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index ac46ba776d7..b1a5e44fb51 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -39,36 +39,36 @@ void convert( source_locationt previous_source_location; - for(const auto & it : goto_trace.steps) + for(const auto &step : goto_trace.steps) { - const source_locationt &source_location=it.pc->source_location; + const source_locationt &source_location=step.pc->source_location; xmlt xml_location; if(source_location.is_not_nil() && source_location.get_file()!="") xml_location=xml(source_location); - switch(it.type) + switch(step.type) { case goto_trace_stept::ASSERT: - if(!it.cond_value) + if(!step.cond_value) { irep_idt property_id; - if(it.pc->is_assert()) + if(step.pc->is_assert()) property_id=source_location.get_property_id(); - else if(it.pc->is_goto()) // unwinding, we suspect + else if(step.pc->is_goto()) // unwinding, we suspect { property_id= - id2string(it.pc->source_location.get_function())+".unwind."+ - std::to_string(it.pc->loop_number); + id2string(step.pc->source_location.get_function())+ + ".unwind."+std::to_string(step.pc->loop_number); } xmlt &xml_failure=dest.new_element("failure"); - xml_failure.set_attribute_bool("hidden", it.hidden); - xml_failure.set_attribute("thread", std::to_string(it.thread_nr)); - xml_failure.set_attribute("step_nr", std::to_string(it.step_nr)); - xml_failure.set_attribute("reason", id2string(it.comment)); + xml_failure.set_attribute_bool("hidden", step.hidden); + xml_failure.set_attribute("thread", std::to_string(step.thread_nr)); + xml_failure.set_attribute("step_nr", std::to_string(step.step_nr)); + xml_failure.set_attribute("reason", id2string(step.comment)); xml_failure.set_attribute("property", id2string(property_id)); if(xml_location.name!="") @@ -79,7 +79,7 @@ void convert( case goto_trace_stept::ASSIGNMENT: case goto_trace_stept::DECL: { - irep_idt identifier=it.lhs_object.get_identifier(); + irep_idt identifier=step.lhs_object.get_identifier(); xmlt &xml_assignment=dest.new_element("assignment"); if(xml_location.name!="") @@ -88,17 +88,19 @@ void convert( std::string value_string, binary_string, type_string, full_lhs_string, full_lhs_value_string; - if(it.lhs_object_value.is_not_nil()) - value_string=from_expr(ns, identifier, it.lhs_object_value); + if(step.lhs_object_value.is_not_nil()) + value_string=from_expr(ns, identifier, step.lhs_object_value); - if(it.full_lhs.is_not_nil()) - full_lhs_string=from_expr(ns, identifier, it.full_lhs); + if(step.full_lhs.is_not_nil()) + full_lhs_string=from_expr(ns, identifier, step.full_lhs); - if(it.full_lhs_value.is_not_nil()) - full_lhs_value_string=from_expr(ns, identifier, it.full_lhs_value); + if(step.full_lhs_value.is_not_nil()) + full_lhs_value_string= + from_expr(ns, identifier, step.full_lhs_value); - if(it.lhs_object_value.type().is_not_nil()) - type_string=from_type(ns, identifier, it.lhs_object_value.type()); + if(step.lhs_object_value.type().is_not_nil()) + type_string= + from_type(ns, identifier, step.lhs_object_value.type()); const symbolt *symbol; irep_idt base_name, display_name; @@ -118,43 +120,44 @@ void convert( xml_assignment.new_element("full_lhs_value").data=full_lhs_value_string; xml_assignment.new_element("value").data=value_string; - xml_assignment.set_attribute_bool("hidden", it.hidden); - xml_assignment.set_attribute("thread", std::to_string(it.thread_nr)); + xml_assignment.set_attribute_bool("hidden", step.hidden); + xml_assignment.set_attribute("thread", std::to_string(step.thread_nr)); xml_assignment.set_attribute("identifier", id2string(identifier)); xml_assignment.set_attribute("base_name", id2string(base_name)); xml_assignment.set_attribute("display_name", id2string(display_name)); - xml_assignment.set_attribute("step_nr", std::to_string(it.step_nr)); + xml_assignment.set_attribute("step_nr", std::to_string(step.step_nr)); xml_assignment.set_attribute("assignment_type", - it.assignment_type==goto_trace_stept::ACTUAL_PARAMETER?"actual_parameter": + step.assignment_type==goto_trace_stept::ACTUAL_PARAMETER?"actual_parameter": "state"); - if(it.lhs_object_value.is_not_nil()) - xml_assignment.new_element("value_expression").new_element(xml(it.lhs_object_value, ns)); + if(step.lhs_object_value.is_not_nil()) + xml_assignment.new_element("value_expression"). + new_element(xml(step.lhs_object_value, ns)); } break; case goto_trace_stept::OUTPUT: { printf_formattert printf_formatter(ns); - printf_formatter(id2string(it.format_string), it.io_args); + printf_formatter(id2string(step.format_string), step.io_args); std::string text=printf_formatter.as_string(); xmlt &xml_output=dest.new_element("output"); xml_output.new_element("text").data=text; - xml_output.set_attribute_bool("hidden", it.hidden); - xml_output.set_attribute("thread", std::to_string(it.thread_nr)); - xml_output.set_attribute("step_nr", std::to_string(it.step_nr)); + xml_output.set_attribute_bool("hidden", step.hidden); + xml_output.set_attribute("thread", std::to_string(step.thread_nr)); + xml_output.set_attribute("step_nr", std::to_string(step.step_nr)); if(xml_location.name!="") xml_output.new_element().swap(xml_location); - for(const auto l_it : it.io_args) + for(const auto &arg : step.io_args) { - xml_output.new_element("value").data=from_expr(ns, "", l_it); + xml_output.new_element("value").data=from_expr(ns, "", arg); xml_output.new_element("value_expression"). - new_element(xml(l_it, ns)); + new_element(xml(arg, ns)); } } break; @@ -162,17 +165,17 @@ void convert( case goto_trace_stept::INPUT: { xmlt &xml_input=dest.new_element("input"); - xml_input.new_element("input_id").data=id2string(it.io_id); + xml_input.new_element("input_id").data=id2string(step.io_id); - xml_input.set_attribute_bool("hidden", it.hidden); - xml_input.set_attribute("thread", std::to_string(it.thread_nr)); - xml_input.set_attribute("step_nr", std::to_string(it.step_nr)); + xml_input.set_attribute_bool("hidden", step.hidden); + xml_input.set_attribute("thread", std::to_string(step.thread_nr)); + xml_input.set_attribute("step_nr", std::to_string(step.step_nr)); - for(const auto & l_it : it.io_args) + for(const auto &arg : step.io_args) { - xml_input.new_element("value").data=from_expr(ns, "", l_it); + xml_input.new_element("value").data=from_expr(ns, "", arg); xml_input.new_element("value_expression"). - new_element(xml(l_it, ns)); + new_element(xml(arg, ns)); } if(xml_location.name!="") @@ -184,17 +187,18 @@ void convert( case goto_trace_stept::FUNCTION_RETURN: { std::string tag= - (it.type==goto_trace_stept::FUNCTION_CALL)?"function_call":"function_return"; + (step.type==goto_trace_stept::FUNCTION_CALL)? + "function_call":"function_return"; xmlt &xml_call_return=dest.new_element(tag); - xml_call_return.set_attribute_bool("hidden", it.hidden); - xml_call_return.set_attribute("thread", std::to_string(it.thread_nr)); - xml_call_return.set_attribute("step_nr", std::to_string(it.step_nr)); + xml_call_return.set_attribute_bool("hidden", step.hidden); + xml_call_return.set_attribute("thread", std::to_string(step.thread_nr)); + xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr)); - const symbolt &symbol=ns.lookup(it.identifier); + const symbolt &symbol=ns.lookup(step.identifier); xmlt &xml_function=xml_call_return.new_element("function"); xml_function.set_attribute("display_name", id2string(symbol.display_name())); - xml_function.set_attribute("identifier", id2string(it.identifier)); + xml_function.set_attribute("identifier", id2string(step.identifier)); xml_function.new_element()=xml(symbol.location); if(xml_location.name!="") @@ -210,9 +214,9 @@ void convert( { xmlt &xml_location_only=dest.new_element("location-only"); - xml_location_only.set_attribute_bool("hidden", it.hidden); - xml_location_only.set_attribute("thread", std::to_string(it.thread_nr)); - xml_location_only.set_attribute("step_nr", std::to_string(it.step_nr)); + xml_location_only.set_attribute_bool("hidden", step.hidden); + xml_location_only.set_attribute("thread", std::to_string(step.thread_nr)); + xml_location_only.set_attribute("step_nr", std::to_string(step.step_nr)); xml_location_only.new_element().swap(xml_location); } diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp index a561984bf30..1b3e6f2d636 100644 --- a/src/goto-symex/auto_objects.cpp +++ b/src/goto-symex/auto_objects.cpp @@ -64,17 +64,13 @@ void goto_symext::initialize_auto_object( if(type.id()==ID_struct) { const struct_typet &struct_type=to_struct_type(type); - const struct_typet::componentst &components=struct_type.components(); - for(struct_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - it++) + for(const auto &comp : struct_type.components()) { member_exprt member_expr; member_expr.struct_op()=expr; - member_expr.set_component_name(it->get_name()); - member_expr.type()=it->type(); + member_expr.set_component_name(comp.get_name()); + member_expr.type()=comp.type(); initialize_auto_object(member_expr, state); } diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index 4c1a718d846..82c724cf3c5 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -258,7 +258,7 @@ void build_goto_trace( simplify(goto_trace_step.full_lhs_value, ns); } - for(const auto & j : SSA_step.converted_io_args) + for(const auto &j : SSA_step.converted_io_args) { if(j.is_constant() || j.id()==ID_string_constant) @@ -283,13 +283,13 @@ void build_goto_trace( // Now assemble into a single goto_trace. // This expoits sorted-ness of the map. - for(auto & t_it : time_map) + for(auto &t_it : time_map) goto_trace.steps.splice(goto_trace.steps.end(), t_it.second); // produce the step numbers unsigned step_nr=0; - for(auto & s_it : goto_trace.steps) + for(auto &s_it : goto_trace.steps) s_it.step_nr=++step_nr; } diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 8c4e48f8a2e..8b2aecfbcaa 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -647,10 +647,10 @@ Function: symex_target_equationt::convert_assignments void symex_target_equationt::convert_assignments( decision_proceduret &decision_procedure) const { - for(const auto & it : SSA_steps) + for(const auto &step : SSA_steps) { - if(it.is_assignment() && !it.ignore) - decision_procedure.set_to_true(it.cond_expr); + if(step.is_assignment() && !step.ignore) + decision_procedure.set_to_true(step.cond_expr); } } @@ -669,13 +669,13 @@ Function: symex_target_equationt::convert_decls void symex_target_equationt::convert_decls( prop_convt &prop_conv) const { - for(const auto & it : SSA_steps) + for(const auto &step : SSA_steps) { - if(it.is_decl() && !it.ignore) + if(step.is_decl() && !step.ignore) { // The result is not used, these have no impact on // the satisfiability of the formula. - prop_conv.convert(it.cond_expr); + prop_conv.convert(step.cond_expr); } } } @@ -695,12 +695,12 @@ Function: symex_target_equationt::convert_guards void symex_target_equationt::convert_guards( prop_convt &prop_conv) { - for(auto & it : SSA_steps) + for(auto &step : SSA_steps) { - if(it.ignore) - it.guard_literal=const_literal(false); + if(step.ignore) + step.guard_literal=const_literal(false); else - it.guard_literal=prop_conv.convert(it.guard); + step.guard_literal=prop_conv.convert(step.guard); } } @@ -719,14 +719,14 @@ Function: symex_target_equationt::convert_assumptions void symex_target_equationt::convert_assumptions( prop_convt &prop_conv) { - for(auto & it : SSA_steps) + for(auto &step : SSA_steps) { - if(it.is_assume()) + if(step.is_assume()) { - if(it.ignore) - it.cond_literal=const_literal(true); + if(step.ignore) + step.cond_literal=const_literal(true); else - it.cond_literal=prop_conv.convert(it.cond_expr); + step.cond_literal=prop_conv.convert(step.cond_expr); } } } @@ -746,14 +746,14 @@ Function: symex_target_equationt::convert_goto_instructions void symex_target_equationt::convert_goto_instructions( prop_convt &prop_conv) { - for(auto & it : SSA_steps) + for(auto &step : SSA_steps) { - if(it.is_goto()) + if(step.is_goto()) { - if(it.ignore) - it.cond_literal=const_literal(true); + if(step.ignore) + step.cond_literal=const_literal(true); else - it.cond_literal=prop_conv.convert(it.cond_expr); + step.cond_literal=prop_conv.convert(step.cond_expr); } } } @@ -773,14 +773,14 @@ Function: symex_target_equationt::convert_constraints void symex_target_equationt::convert_constraints( decision_proceduret &decision_procedure) const { - for(const auto & it : SSA_steps) + for(const auto &step : SSA_steps) { - if(it.is_constraint()) + if(step.is_constraint()) { - if(it.ignore) + if(step.ignore) continue; - decision_procedure.set_to_true(it.cond_expr); + decision_procedure.set_to_true(step.cond_expr); } } } @@ -810,16 +810,16 @@ void symex_target_equationt::convert_assertions( if(number_of_assertions==1) { - for(auto & it : SSA_steps) + for(auto &step : SSA_steps) { - if(it.is_assert()) + if(step.is_assert()) { - prop_conv.set_to_false(it.cond_expr); - it.cond_literal=const_literal(false); + prop_conv.set_to_false(step.cond_expr); + step.cond_literal=const_literal(false); return; // prevent further assumptions! } - else if(it.is_assume()) - prop_conv.set_to_true(it.cond_expr); + else if(step.is_assume()) + prop_conv.set_to_true(step.cond_expr); } assert(false); // unreachable @@ -832,29 +832,29 @@ void symex_target_equationt::convert_assertions( exprt assumption=true_exprt(); - for(auto & it : SSA_steps) + for(auto &step : SSA_steps) { - if(it.is_assert()) + if(step.is_assert()) { implies_exprt implication( assumption, - it.cond_expr); + step.cond_expr); // do the conversion - it.cond_literal=prop_conv.convert(implication); + step.cond_literal=prop_conv.convert(implication); // store disjunct - disjuncts.push_back(literal_exprt(!it.cond_literal)); + disjuncts.push_back(literal_exprt(!step.cond_literal)); } - else if(it.is_assume()) + else if(step.is_assume()) { // the assumptions have been converted before // avoid deep nesting of ID_and expressions if(assumption.id()==ID_and) - assumption.copy_to_operands(literal_exprt(it.cond_literal)); + assumption.copy_to_operands(literal_exprt(step.cond_literal)); else assumption= - and_exprt(assumption, literal_exprt(it.cond_literal)); + and_exprt(assumption, literal_exprt(step.cond_literal)); } } @@ -879,27 +879,25 @@ void symex_target_equationt::convert_io( { unsigned io_count=0; - for(auto & it : SSA_steps) - if(!it.ignore) + for(auto &step : SSA_steps) + if(!step.ignore) { - for(const auto & o_it : it.io_args) + for(const auto &arg : step.io_args) { - exprt tmp=o_it; - - if(tmp.is_constant() || - tmp.id()==ID_string_constant) - it.converted_io_args.push_back(tmp); + if(arg.is_constant() || + arg.id()==ID_string_constant) + step.converted_io_args.push_back(arg); else { symbol_exprt symbol; - symbol.type()=tmp.type(); + symbol.type()=arg.type(); symbol.set_identifier("symex::io::"+std::to_string(io_count++)); - equal_exprt eq(tmp, symbol); + equal_exprt eq(arg, symbol); merge_irep(eq); dec_proc.set_to(eq, true); - it.converted_io_args.push_back(symbol); + step.converted_io_args.push_back(symbol); } } } @@ -929,8 +927,8 @@ void symex_target_equationt::merge_ireps(SSA_stept &SSA_step) merge_irep(SSA_step.cond_expr); - for(auto & it : SSA_step.io_args) - merge_irep(it); + for(auto &step : SSA_step.io_args) + merge_irep(step); // converted_io_args is merged in convert_io } @@ -949,9 +947,9 @@ Function: symex_target_equationt::output void symex_target_equationt::output(std::ostream &out) const { - for(const auto & it : SSA_steps) + for(const auto &step : SSA_steps) { - it.output(ns, out); + step.output(ns, out); out << "--------------\n"; } } diff --git a/src/java_bytecode/jar_file.cpp b/src/java_bytecode/jar_file.cpp index 5d8663c32a1..5e59aadc12e 100644 --- a/src/java_bytecode/jar_file.cpp +++ b/src/java_bytecode/jar_file.cpp @@ -144,7 +144,7 @@ jar_filet::manifestt jar_filet::get_manifest() std::size_t i=0; bool found=false; - for(const auto & e : index) + for(const auto &e : index) { if(e=="META-INF/MANIFEST.MF") { diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 04fcc3cebe5..2db872c3f45 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -89,11 +89,9 @@ void java_bytecode_convert_classt::convert(const classt &c) } // interfaces are recorded as bases - const std::list &ifc=c.implements; - - for(const auto & it : ifc) + for(const auto &interface : c.implements) { - symbol_typet base("java::"+id2string(it)); + symbol_typet base("java::"+id2string(interface)); class_type.add_base(base); } @@ -117,13 +115,13 @@ void java_bytecode_convert_classt::convert(const classt &c) } // now do fields - for(const auto & it : c.fields) - convert(*class_symbol, it); + for(const auto &field : c.fields) + convert(*class_symbol, field); // now do methods - for(const auto & it : c.methods) + for(const auto &method : c.methods) java_bytecode_convert_method( - *class_symbol, it, symbol_table, get_message_handler()); + *class_symbol, method, symbol_table, get_message_handler()); // is this a root class? if(c.extends.empty()) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 49b621aed89..ccdd54db7e2 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -95,12 +95,12 @@ class java_bytecode_convert_methodt:public messaget } instruction_sizet; // return corresponding reference of variable - variablet &find_variable_for_slot( + const variablet &find_variable_for_slot( size_t address, variablest &var_list, instruction_sizet inst_size) { - for(variablet &var : var_list) + for(const variablet &var : var_list) { size_t start_pc=var.start_pc; size_t length=var.length; @@ -140,7 +140,7 @@ class java_bytecode_convert_methodt:public messaget variablest &var_list=variables[number_int]; // search variable in list for correct frame / address if necessary - variablet &var= + const variablet &var= find_variable_for_slot(address, var_list, inst_size); if(var.symbol_expr.get_identifier().empty()) @@ -312,7 +312,7 @@ void java_bytecode_convert_methodt::convert( // to calculate which variable to use, one uses the address of the instruction // that uses the variable, the size of the instruction and the start_pc / // length values in the local variable table - for(const auto & v : m.local_variable_table) + for(const auto &v : m.local_variable_table) { typet t=java_type_from_string(v.signature); std::ostringstream id_oss; @@ -328,25 +328,25 @@ void java_bytecode_convert_methodt::convert( } // set up variables array - for(std::size_t i=0, param_index=0; - i::max(); variables[param_index][0].is_parameter=true; param_index+=slots; + assert(param_index>0); } const bool is_virtual=!m.is_static && !m.is_final; @@ -590,33 +591,28 @@ codet java_bytecode_convert_methodt::convert_instructions( i_it->statement=="lookupswitch") { bool is_label=true; - for(instructiont::argst::const_iterator - a_it=i_it->args.begin(); - a_it!=i_it->args.end(); - a_it++, is_label=!is_label) + for(const auto &arg : i_it->args) { if(is_label) { const unsigned target=safe_string2unsigned( - id2string(to_constant_expr(*a_it).get_value())); + id2string(to_constant_expr(arg).get_value())); targets.insert(target); a_entry.first->second.successors.push_back(target); } + is_label=!is_label; } } } - for(address_mapt::iterator - it=address_map.begin(); - it!=address_map.end(); - ++it) + for(const auto &address : address_map) { - for(unsigned s : it->second.successors) + for(unsigned s : address.second.successors) { address_mapt::iterator a_it=address_map.find(s); assert(a_it!=address_map.end()); - a_it->second.predecessors.insert(it->first); + a_it->second.predecessors.insert(address.first); } } @@ -1475,12 +1471,9 @@ codet java_bytecode_convert_methodt::convert_instructions( push(results); a_it->second.done=true; - for(std::list::iterator - it=a_it->second.successors.begin(); - it!=a_it->second.successors.end(); - ++it) + for(const unsigned address : a_it->second.successors) { - address_mapt::iterator a_it2=address_map.find(*it); + address_mapt::iterator a_it2=address_map.find(address); assert(a_it2!=address_map.end()); if(!stack.empty() && a_it2->second.predecessors.size()>1) @@ -1507,17 +1500,15 @@ codet java_bytecode_convert_methodt::convert_instructions( { assert(a_it2->second.stack.size()==stack.size()); stackt::const_iterator os_it=a_it2->second.stack.begin(); - for(stackt::iterator s_it=stack.begin(); - s_it!=stack.end(); - ++s_it) + for(auto &expr : stack) { assert(has_prefix(os_it->get_string(ID_C_base_name), "$stack")); symbol_exprt lhs=to_symbol_expr(*os_it); - code_assignt a(lhs, *s_it); + code_assignt a(lhs, expr); more_code.copy_to_operands(a); - s_it->swap(lhs); + expr.swap(lhs); ++os_it; } } @@ -1544,7 +1535,7 @@ codet java_bytecode_convert_methodt::convert_instructions( code_blockt code; // locals - for(const auto & var : used_local_names) + for(const auto &var : used_local_names) { code.add(code_declt(var)); symbolt new_symbol; @@ -1561,16 +1552,16 @@ codet java_bytecode_convert_methodt::convert_instructions( symbol_table.add(new_symbol); } // temporaries - for(const auto & var : tmp_vars) + for(const auto &var : tmp_vars) { code.add(code_declt(var)); } - for(const auto & it : address_map) + for(const auto &address_pair : address_map) { - const unsigned address=it.first; - assert(it.first==it.second.source->address); - const codet &c=it.second.code; + const unsigned address=address_pair.first; + assert(address_pair.first==address_pair.second.source->address); + const codet &c=address_pair.second.code; if(targets.find(address)!=targets.end()) code.add(code_labelt(label(std::to_string(address)), c)); diff --git a/src/java_bytecode/java_bytecode_parse_tree.cpp b/src/java_bytecode/java_bytecode_parse_tree.cpp index 2ada0464475..b7f3be50007 100644 --- a/src/java_bytecode/java_bytecode_parse_tree.cpp +++ b/src/java_bytecode/java_bytecode_parse_tree.cpp @@ -81,7 +81,7 @@ Function: java_bytecode_parse_treet::classt::output void java_bytecode_parse_treet::classt::output(std::ostream &out) const { - for(const auto & annotation : annotations) + for(const auto &annotation : annotations) { annotation.output(out); out << '\n'; @@ -137,7 +137,7 @@ void java_bytecode_parse_treet::annotationt::output(std::ostream &out) const out << '('; bool first=true; - for(const auto & element_value_pair : element_value_pairs) + for(const auto &element_value_pair : element_value_pairs) { if(first) first=false; else out << ", "; element_value_pair.output(out); @@ -185,7 +185,7 @@ void java_bytecode_parse_treet::methodt::output(std::ostream &out) const symbol_tablet symbol_table; namespacet ns(symbol_table); - for(const auto & annotation : annotations) + for(const auto &annotation : annotations) { out << " "; annotation.output(out); @@ -222,7 +222,7 @@ void java_bytecode_parse_treet::methodt::output(std::ostream &out) const out << " {" << '\n'; - for(const auto & i : instructions) + for(const auto &i : instructions) { if(i.source_location.get_line()!=irep_idt()) out << " // " << i.source_location << '\n'; @@ -249,7 +249,7 @@ void java_bytecode_parse_treet::methodt::output(std::ostream &out) const out << '\n'; out << " Locals:\n"; - for(const auto & v : local_variable_table) + for(const auto &v : local_variable_table) { out << " " << v.index << ": " << v.name << ' ' << v.signature << '\n'; @@ -272,7 +272,7 @@ Function: java_bytecode_parse_treet::fieldt::output void java_bytecode_parse_treet::fieldt::output(std::ostream &out) const { - for(const auto & annotation : annotations) + for(const auto &annotation : annotations) { out << " "; annotation.output(out); diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 45cbffa1035..2f79c7bce89 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -335,7 +335,7 @@ void java_bytecode_parsert::get_class_refs() // Get the class references for the benefit of a dependency // analysis. - for(const auto & c : constant_pool) + for(const auto &c : constant_pool) { switch(c.tag) { @@ -354,17 +354,17 @@ void java_bytecode_parsert::get_class_refs() } } - for(const auto & m : parse_tree.parsed_class.fields) + for(const auto &m : parse_tree.parsed_class.fields) { typet t=java_type_from_string(m.signature); get_class_refs_rec(t); } - for(const auto & m : parse_tree.parsed_class.methods) + for(const auto &m : parse_tree.parsed_class.methods) { typet t=java_type_from_string(m.signature); get_class_refs_rec(t); - for(const auto & var : m.local_variable_table) + for(const auto &var : m.local_variable_table) { typet var_type=java_type_from_string(var.signature); get_class_refs_rec(var_type); @@ -391,7 +391,7 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src) const code_typet &ct=to_code_type(src); const typet &rt=ct.return_type(); get_class_refs_rec(rt); - for(const auto & p : ct.parameters()) + for(const auto &p : ct.parameters()) get_class_refs_rec(p.type()); } else if(src.id()==ID_symbol) @@ -409,7 +409,7 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src) else if(src.id()==ID_struct) { const struct_typet &struct_type=to_struct_type(src); - for(const auto & c : struct_type.components()) + for(const auto &c : struct_type.components()) get_class_refs_rec(c.type()); } else if(src.id()==ID_pointer) @@ -1301,7 +1301,7 @@ void java_bytecode_parsert::relement_value_pairs( u2 num_element_value_pairs=read_u2(); element_value_pairs.resize(num_element_value_pairs); - for(auto & element_value_pair : element_value_pairs) + for(auto &element_value_pair : element_value_pairs) { u2 element_name_index=read_u2(); element_value_pair.element_name=pool_entry(element_name_index).s; diff --git a/src/java_bytecode/java_class_loader.cpp b/src/java_bytecode/java_class_loader.cpp index f6e82443d59..3d0f8338caf 100644 --- a/src/java_bytecode/java_class_loader.cpp +++ b/src/java_bytecode/java_class_loader.cpp @@ -80,7 +80,7 @@ java_bytecode_parse_treet &java_class_loadert::get_parse_tree( java_bytecode_parse_treet &parse_tree=class_map[class_name]; // First check given JAR files - for(const auto & jf : jar_files) + for(const auto &jf : jar_files) { read_jar_file(jf); @@ -108,7 +108,7 @@ java_bytecode_parse_treet &java_class_loadert::get_parse_tree( // See if we can find it in the class path - for(const auto & cp : config.java.classpath) + for(const auto &cp : config.java.classpath) { // in a JAR? if(has_suffix(cp, ".jar")) diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 1e49b8933b8..ee0c0c1c2ae 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -292,7 +292,7 @@ bool java_entry_point( std::string prefix=main_identifier+':'; std::set matches; - for(const auto & s : symbol_table.symbols) + for(const auto &s : symbol_table.symbols) if(has_prefix(id2string(s.first), prefix) && s.second.type.id()==ID_code) matches.insert(s.first); @@ -313,7 +313,7 @@ bool java_entry_point( message.error() << "main symbol `" << config.main << "' is ambiguous:\n"; - for(const auto & s : matches) + for(const auto &s : matches) message.error() << " " << s << '\n'; message.error() << messaget::eom; diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 15735f62539..6eeba5e23eb 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -101,7 +101,7 @@ void gen_nondet_init( recursion_set.insert(struct_tag); assert(!recursion_set.empty()); - for(const auto & component : components) + for(const auto &component : components) { const typet &component_type=component.type(); irep_idt name=component.get_name(); diff --git a/src/musketeer/musketeer_parse_options.cpp b/src/musketeer/musketeer_parse_options.cpp index 28accf23fa2..4912db95dd3 100644 --- a/src/musketeer/musketeer_parse_options.cpp +++ b/src/musketeer/musketeer_parse_options.cpp @@ -11,6 +11,7 @@ Module: Main Module #include #include +#include #include #include diff --git a/src/solvers/prop/aig_prop.cpp b/src/solvers/prop/aig_prop.cpp index da966b3b111..ea64eb0405f 100644 --- a/src/solvers/prop/aig_prop.cpp +++ b/src/solvers/prop/aig_prop.cpp @@ -773,7 +773,7 @@ void aig_prop_solvert::convert_aig() // 3. Do constraints - for(const auto & c_it : aig.constraints) + for(const auto &c_it : aig.constraints) solver.l_set_to(c_it, true); // HACK! diff --git a/src/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp index fdbef952af4..699177b25ad 100644 --- a/src/solvers/prop/cover_goals.cpp +++ b/src/solvers/prop/cover_goals.cpp @@ -42,10 +42,10 @@ Function: cover_goalst::mark void cover_goalst::mark() { // notify observers - for(const auto & o : observers) + for(const auto &o : observers) o->satisfying_assignment(); - for(auto & g : goals) + for(auto &g : goals) if(g.status==goalt::statust::UNKNOWN && prop_conv.l_get(g.condition).is_true()) { @@ -53,7 +53,7 @@ void cover_goalst::mark() _number_covered++; // notify observers - for(const auto & o : observers) + for(const auto &o : observers) o->goal_covered(g); } } diff --git a/src/solvers/smt1/smt1_conv.cpp b/src/solvers/smt1/smt1_conv.cpp index 44bb59cb63c..b769d3b052e 100644 --- a/src/solvers/smt1/smt1_conv.cpp +++ b/src/solvers/smt1/smt1_conv.cpp @@ -2179,8 +2179,8 @@ void smt1_convt::convert_is_dynamic_object( { out << "(or"; - for(const auto & it : dynamic_objects) - out << " (= bv" << it + for(const auto &obj : dynamic_objects) + out << " (= bv" << obj << "[" << BV_ADDR_BITS << "] ?obj)"; out << ")"; // or @@ -3550,16 +3550,16 @@ void smt1_convt::find_symbols_rec( const struct_union_typet::componentst &components= to_struct_union_type(type).components(); - for(std::size_t i=0; isecond, it->first); - } + for(const auto &object : object_sizes) + define_object_size(object.second, object.first); out << "(check-sat)" << "\n"; out << "\n"; if (solver!=BOOLECTOR) { - for(smt2_identifierst::const_iterator - it=smt2_identifiers.begin(); - it!=smt2_identifiers.end(); - it++) - out << "(get-value (|" << *it << "|))" << "\n"; + for(const auto &id : smt2_identifiers) + out << "(get-value (|" << id << "|))" << "\n"; } out << "\n"; @@ -204,23 +197,19 @@ void smt2_convt::define_object_size( std::size_t h = pointer_width - 1; std::size_t l = pointer_width - BV_ADDR_BITS; - for(pointer_logict::objectst::const_iterator it = pointer_logic.objects.begin(); - it != pointer_logic.objects.end(); - ++it, number++) + for(const auto &o : pointer_logic.objects) { - const exprt &o = *it; const typet &type = ns.follow(o.type()); exprt size_expr = size_of_expr(type, ns); mp_integer object_size; - if (o.id() != ID_symbol) - continue; - - if (size_expr.is_nil()) - continue; - - if (to_integer(size_expr, object_size)) + if(o.id()!=ID_symbol || + size_expr.is_nil() || + to_integer(size_expr, object_size)) + { + ++number; continue; + } out << "(assert (implies (= " << "((_ extract " << h << " " << l << ") "; @@ -228,6 +217,8 @@ void smt2_convt::define_object_size( out << ") (_ bv" << number << " " << BV_ADDR_BITS << "))" << "(= " << id << " (_ bv" << object_size.to_ulong() << " " << size_width << "))))\n"; + + ++number; } } @@ -3062,8 +3053,8 @@ void smt2_convt::convert_is_dynamic_object(const exprt &expr) { out << "(or"; - for(const auto & it : dynamic_objects) - out << " (= (_ bv" << it + for(const auto &object : dynamic_objects) + out << " (= (_ bv" << object << " " << BV_ADDR_BITS << ") ?obj)"; out << ")"; // or @@ -5075,8 +5066,8 @@ void smt2_convt::find_symbols_rec( const struct_typet::componentst &components= to_struct_type(type).components(); - for(std::size_t i=0; i tests; - for(const auto & it : property_map) - if(it.second.is_failure()) - tests.insert(get_test(it.second.error_trace)); + for(const auto &prop_pair : property_map) + if(prop_pair.second.is_failure()) + tests.insert(get_test(prop_pair.second.error_trace)); std::cout << "Test suite:" << '\n'; - for(const auto & t : tests) + for(const auto &t : tests) std::cout << t << '\n'; } } diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp index a3ffc20a021..898c235db05 100644 --- a/src/util/base_type.cpp +++ b/src/util/base_type.cpp @@ -55,8 +55,8 @@ void base_type_rec( struct_union_typet::componentst &components= to_struct_union_type(type).components(); - for(auto & it : components) - base_type_rec(it.type(), ns, symb); + for(auto &component : components) + base_type_rec(component.type(), ns, symb); } else if(type.id()==ID_pointer) { diff --git a/src/util/get_module.cpp b/src/util/get_module.cpp index 6f1ea627967..63eea030fb1 100644 --- a/src/util/get_module.cpp +++ b/src/util/get_module.cpp @@ -131,7 +131,7 @@ const symbolt &get_module( message.error() << "multiple modules found, please select one:\n"; - for(const auto & s_it : modules) + for(const auto &s_it : modules) message.error() << " " << s_it << '\n'; message.error() << messaget::eom; diff --git a/src/util/json.cpp b/src/util/json.cpp index 61f2fea3735..75a9b5d3f42 100644 --- a/src/util/json.cpp +++ b/src/util/json.cpp @@ -26,14 +26,14 @@ Function: jsont::escape_string void jsont::escape_string(const std::string &src, std::ostream &out) { - for(const auto & it : src) + for(const auto &ch : src) { - switch(it) + switch(ch) { case '\\': case '"': out << '\\'; - out << it; + out << ch; break; case '\b': @@ -57,7 +57,7 @@ void jsont::escape_string(const std::string &src, std::ostream &out) break; default: - out << it; + out << ch; } } } diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp index 2986decd223..e1d1baf8a6c 100644 --- a/src/util/json_expr.cpp +++ b/src/util/json_expr.cpp @@ -132,11 +132,11 @@ json_objectt json( json_arrayt &members=result["members"].make_array(); const struct_typet::componentst &components= to_struct_type(type).components(); - for(const auto & it : components) + for(const auto &component : components) { json_objectt &e=members.push_back().make_object(); - e["name"]=json_stringt(id2string(it.get_name())); - e["type"]=json(it.type(), ns); + e["name"]=json_stringt(id2string(component.get_name())); + e["type"]=json(component.type(), ns); } } else if(type.id()==ID_union) @@ -145,11 +145,11 @@ json_objectt json( json_arrayt &members=result["members"].make_array(); const union_typet::componentst &components= to_union_type(type).components(); - for(const auto & it : components) + for(const auto &component : components) { json_objectt &e=members.push_back().make_object(); - e["name"]=json_stringt(id2string(it.get_name())); - e["type"]=json(it.type(), ns); + e["name"]=json_stringt(id2string(component.get_name())); + e["type"]=json(component.type(), ns); } } else diff --git a/src/util/signal_catcher.cpp b/src/util/signal_catcher.cpp index 1ff611f8953..942f3925435 100644 --- a/src/util/signal_catcher.cpp +++ b/src/util/signal_catcher.cpp @@ -105,7 +105,7 @@ void signal_catcher(int sig) killpg(0, sig); #else // pass on to any children - for(const auto & pid : pids_of_children) + for(const auto &pid : pids_of_children) kill(pid, sig); #endif diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 2894544b8db..03785f54e30 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -428,17 +428,17 @@ bool simplify_exprt::simplify_typecast(exprt &expr) const unsignedbv_typet size_t_type(config.ansi_c.pointer_width); expr.op0().type()=size_t_type; - for(auto & it : expr.op0().operands()) + for(auto &op : expr.op0().operands()) { - if(it.type().id()==ID_pointer) + if(op.type().id()==ID_pointer) { - it.make_typecast(size_t_type); + op.make_typecast(size_t_type); } else { - it.make_typecast(size_t_type); + op.make_typecast(size_t_type); if(step>1) - it=mult_exprt(from_integer(step, size_t_type), it); + op=mult_exprt(from_integer(step, size_t_type), op); } } @@ -1500,19 +1500,16 @@ bool simplify_exprt::simplify_update(exprt &expr) exprt updated_value=to_update_expr(expr).old(); exprt *value_ptr=&updated_value; - for(exprt::operandst::const_iterator - it=designator.begin(); - it!=designator.end(); - it++) + for(const auto &e : designator) { const typet &value_ptr_type=ns.follow(value_ptr->type()); - if(it->id()==ID_index_designator && + if(e.id()==ID_index_designator && value_ptr->id()==ID_array) { mp_integer i; - if(to_integer(it->op0(), i)) + if(to_integer(e.op0(), i)) return true; if(i<0 || i>=value_ptr->operands().size()) @@ -1520,11 +1517,11 @@ bool simplify_exprt::simplify_update(exprt &expr) value_ptr=&value_ptr->operands()[integer2size_t(i)]; } - else if(it->id()==ID_member_designator && + else if(e.id()==ID_member_designator && value_ptr->id()==ID_struct) { const irep_idt &component_name= - it->get(ID_component_name); + e.get(ID_component_name); if(!to_struct_type(value_ptr_type). has_component(component_name)) @@ -1707,16 +1704,13 @@ exprt simplify_exprt::bits2expr( const union_typet::componentst &components= union_type.components(); - for(union_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - ++it) + for(const auto &component : components) { - exprt val=bits2expr(bits, it->type(), little_endian); + exprt val=bits2expr(bits, component.type(), little_endian); if(val.is_nil()) continue; - return union_exprt(it->get_name(), val, type); + return union_exprt(component.get_name(), val, type); } } else if(type.id()==ID_struct) @@ -1729,12 +1723,9 @@ exprt simplify_exprt::bits2expr( result.reserve_operands(components.size()); mp_integer m_offset_bits=0; - for(struct_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - ++it) + for(const auto &component : components) { - mp_integer m_size=pointer_offset_bits(it->type(), ns); + mp_integer m_size=pointer_offset_bits(component.type(), ns); assert(m_size>=0); std::string comp_bits= @@ -1742,7 +1733,7 @@ exprt simplify_exprt::bits2expr( bits, integer2size_t(m_offset_bits), integer2size_t(m_size)); - exprt comp=bits2expr(comp_bits, it->type(), little_endian); + exprt comp=bits2expr(comp_bits, component.type(), little_endian); if(comp.is_nil()) return nil_exprt(); result.move_to_operands(comp); @@ -2075,21 +2066,18 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr) struct_type.components(); mp_integer m_offset_bits=0; - for(struct_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - ++it) + for(const auto &component : components) { mp_integer m_size= - pointer_offset_bits(it->type(), ns); + pointer_offset_bits(component.type(), ns); if(m_size<=0) break; if(offset*8==m_offset_bits && el_size==m_size && - base_type_eq(expr.type(), it->type(), ns)) + base_type_eq(expr.type(), component.type(), ns)) { - member_exprt member(expr.op(), it->get_name(), it->type()); + member_exprt member(expr.op(), component.get_name(), component.type()); simplify_member(member); expr.swap(member); @@ -2099,7 +2087,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr) offset*8+el_size<=m_offset_bits+m_size && m_offset_bits%8==0) { - expr.op()=member_exprt(expr.op(), it->get_name(), it->type()); + expr.op()=member_exprt(expr.op(), component.get_name(), component.type()); simplify_member(expr.op()); expr.offset()= from_integer(offset-m_offset_bits/8, expr.offset().type()); @@ -2271,14 +2259,11 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr) const struct_typet::componentst &components= struct_type.components(); - for(struct_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - ++it) + for(const auto &component : components) { mp_integer m_offset= - member_offset(struct_type, it->get_name(), ns); - mp_integer m_size_bits=pointer_offset_bits(it->type(), ns); + member_offset(struct_type, component.get_name(), ns); + mp_integer m_size_bits=pointer_offset_bits(component.type(), ns); mp_integer m_size_bytes=m_size_bits/8; // can we determine the current offset, and is it a byte-sized @@ -2302,7 +2287,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr) result_expr=expr.op(); exprt member_name(ID_member_name); - member_name.set(ID_component_name, it->get_name()); + member_name.set(ID_component_name, component.get_name()); result_expr=with_exprt(result_expr, member_name, nil_exprt()); // are we updating on member boundaries? @@ -2313,7 +2298,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr) { byte_update_exprt v( ID_byte_update_little_endian, - member_exprt(root, it->get_name(), it->type()), + member_exprt(root, component.get_name(), component.type()), from_integer(offset_int-m_offset, offset.type()), value); @@ -2332,7 +2317,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr) ID_byte_extract_little_endian, value, from_integer(m_offset-offset_int, offset.type()), - it->type()); + component.type()); to_with_expr(result_expr).new_value().swap(v); } diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index e990fb29865..ae5a0f60fd7 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -352,7 +352,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr) exprt::operandst ptr_expr; exprt::operandst int_expr; - for(const auto & op : ptr.operands()) + for(const auto &op : ptr.operands()) { if(op.type().id()==ID_pointer) ptr_expr.push_back(op); diff --git a/src/util/unicode.cpp b/src/util/unicode.cpp index 442d87f2f3c..4502605c600 100644 --- a/src/util/unicode.cpp +++ b/src/util/unicode.cpp @@ -198,8 +198,8 @@ std::string utf32_to_utf8(const std::basic_string &s) result.reserve(s.size()); // at least that long - for(const auto it : s) - utf32_to_utf8(it, result); + for(const auto c : s) + utf32_to_utf8(c, result); return result; } @@ -222,8 +222,8 @@ std::string utf16_to_utf8(const std::basic_string &s) result.reserve(s.size()); // at least that long - for(const auto it : s) - utf32_to_utf8(it, result); + for(const auto c : s) + utf32_to_utf8(c, result); return result; } diff --git a/src/util/xml.cpp b/src/util/xml.cpp index 957424302f3..1cea04a0bfa 100644 --- a/src/util/xml.cpp +++ b/src/util/xml.cpp @@ -74,13 +74,13 @@ void xmlt::output(std::ostream &out, unsigned indent) const out << '<' << name; - for(const auto & it : attributes) + for(const auto &attribute : attributes) { // it.first needs to be non-empty - if(it.first=="") continue; - out << ' ' << it.first + if(attribute.first.empty()) continue; + out << ' ' << attribute.first << '=' << '"'; - escape_attribute(it.second, out); + escape_attribute(attribute.second, out); out << '"'; } @@ -98,8 +98,8 @@ void xmlt::output(std::ostream &out, unsigned indent) const { out << "\n"; - for(const auto & it : elements) - it.output(out, indent+2); + for(const auto &element : elements) + element.output(out, indent+2); do_indent(out, indent); } @@ -170,7 +170,7 @@ Function: xmlt::escape_attribute void xmlt::escape_attribute(const std::string &s, std::ostream &out) { - for(const auto & ch : s) + for(const auto ch : s) { switch(ch) { @@ -214,8 +214,7 @@ Function: xmlt::do_indent void xmlt::do_indent(std::ostream &out, unsigned indent) { - for(unsigned i=0; i public: inline bool has_node(const std::string &node_name) const { - for(const auto & n : nodes) + for(const auto &n : nodes) if(n.node_name==node_name) return true;