From 53b665b6a6e81dfb752d35292be665bd7d8fb244 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 1 Dec 2016 22:31:27 +0000 Subject: [PATCH 1/8] Use string constructor instead of for loop --- src/goto-programs/vcd_goto_trace.cpp | 9 +-------- src/util/xml.cpp | 3 +-- 2 files changed, 2 insertions(+), 10 deletions(-) diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp index e4f7eec02bd..59eb2a0ef6b 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 ""; } diff --git a/src/util/xml.cpp b/src/util/xml.cpp index 957424302f3..8d2a85bfac2 100644 --- a/src/util/xml.cpp +++ b/src/util/xml.cpp @@ -214,8 +214,7 @@ Function: xmlt::do_indent void xmlt::do_indent(std::ostream &out, unsigned indent) { - for(unsigned i=0; i Date: Thu, 1 Dec 2016 18:56:50 +0000 Subject: [PATCH 2/8] Fail on duplicate struct members The previous code would scan for duplicate struct members, but not do anything about them either way. GCC now reports these as errors, and so should the C front end. --- regression/ansi-c/struct7/main.c | 11 +++++++++++ regression/ansi-c/struct7/test.desc | 8 ++++++++ src/ansi-c/c_typecheck_type.cpp | 4 +++- 3 files changed, 22 insertions(+), 1 deletion(-) create mode 100644 regression/ansi-c/struct7/main.c create mode 100644 regression/ansi-c/struct7/test.desc 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/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index dcfb2ea5ccf..f5f9c2de4d5 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -926,7 +926,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; } } } From 1814ffb7011714d3a9dc4e251f2a827b8ed76d08 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 21 Dec 2016 13:16:43 +0100 Subject: [PATCH 3/8] Code simplification --- src/goto-instrument/wmm/goto2graph.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index 7f18743cece..9612c84717d 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -1536,10 +1536,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; } } From 11e960c5f3f9ca16d8530a001d4d0d74a12c9ab7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 1 Dec 2016 22:25:38 +0000 Subject: [PATCH 4/8] Use ranged-for C++11 ranged-for permits more concise implementations. Also, do not use "it" as element name in ranged-for as these are objects and not iterators anymore. --- src/aa-path-symex/path_symex_history.cpp | 6 +- src/aa-path-symex/path_symex_state.cpp | 7 +- src/aa-symex/path_search.cpp | 23 +-- src/aa-symex/symex_parseoptions.cpp | 24 +-- src/analyses/ai.cpp | 34 +--- src/analyses/call_graph.cpp | 24 +-- src/analyses/cfg_dominators.h | 41 ++--- src/analyses/constant_propagator.cpp | 37 ++-- src/analyses/custom_bitvector_analysis.cpp | 79 ++++----- src/analyses/dependence_graph.cpp | 75 +++----- src/analyses/dirty.cpp | 7 +- src/analyses/escape_analysis.cpp | 63 +++---- src/analyses/flow_insensitive_analysis.cpp | 15 +- src/analyses/global_may_alias.cpp | 14 +- src/analyses/goto_check.cpp | 13 +- src/analyses/interval_analysis.cpp | 7 +- src/analyses/interval_domain.cpp | 30 ++-- src/analyses/invariant_propagation.cpp | 70 +++----- src/analyses/invariant_set.cpp | 51 ++---- src/analyses/is_threaded.cpp | 13 +- src/analyses/local_bitvector_analysis.cpp | 18 +- src/analyses/local_cfg.cpp | 14 +- src/analyses/locals.cpp | 19 +- src/analyses/natural_loops.h | 29 ++-- src/analyses/reaching_definitions.cpp | 148 ++++++---------- src/analyses/static_analysis.cpp | 27 +-- src/analyses/uninitialized_domain.cpp | 2 +- src/ansi-c/anonymous_member.cpp | 26 ++- src/ansi-c/ansi_c_declaration.cpp | 6 +- src/ansi-c/ansi_c_entry_point.cpp | 4 +- src/ansi-c/ansi_c_parse_tree.cpp | 7 +- src/ansi-c/ansi_c_scope.cpp | 9 +- src/ansi-c/c_misc.cpp | 2 +- src/ansi-c/c_preprocess.cpp | 111 ++++-------- src/ansi-c/c_sizeof.cpp | 29 ++-- src/ansi-c/c_typecast.cpp | 11 +- src/ansi-c/c_typecheck_expr.cpp | 2 +- src/ansi-c/c_typecheck_type.cpp | 66 +++---- src/ansi-c/parser_static.inc | 12 +- src/cbmc/all_properties.cpp | 43 ++--- src/cbmc/all_properties_class.h | 8 +- src/cbmc/bmc.cpp | 2 +- src/cbmc/bmc_cover.cpp | 60 +++---- src/cbmc/cbmc_dimacs.cpp | 36 ++-- src/cbmc/cbmc_parse_options.cpp | 11 +- src/cbmc/counterexample_beautification.cpp | 7 +- src/cbmc/xml_interface.cpp | 7 +- src/clobber/clobber_parse_options.cpp | 26 ++- src/cpp/cpp_typecheck.cpp | 6 +- src/cpp/cpp_typecheck_code.cpp | 2 +- src/cpp/cpp_typecheck_compound_type.cpp | 48 +++--- src/cpp/cpp_typecheck_declaration.cpp | 6 +- src/cpp/cpp_typecheck_method_bodies.cpp | 2 +- src/cpp/cpp_typecheck_type.cpp | 10 +- src/goto-analyzer/taint_analysis.cpp | 8 +- src/goto-analyzer/taint_parser.cpp | 2 +- src/goto-instrument/accelerate/accelerate.cpp | 9 +- .../accelerate/acceleration_utils.cpp | 26 ++- .../accelerate/all_paths_enumerator.cpp | 15 +- .../accelerate/cone_of_influence.cpp | 22 +-- .../disjunctive_polynomial_acceleration.cpp | 32 ++-- src/goto-instrument/accelerate/path.cpp | 15 +- .../accelerate/sat_path_enumerator.cpp | 48 +++--- .../accelerate/trace_automaton.cpp | 95 ++++------ src/goto-instrument/cover.cpp | 12 +- src/goto-instrument/dot.cpp | 26 ++- src/goto-instrument/havoc_loops.cpp | 7 +- src/goto-instrument/wmm/goto2graph.cpp | 163 +++++++----------- src/goto-programs/basic_blocks.cpp | 7 +- src/goto-programs/builtin_functions.cpp | 2 +- src/goto-programs/cfg.h | 24 +-- src/goto-programs/class_hierarchy.cpp | 16 +- src/goto-programs/get_goto_model.cpp | 8 +- src/goto-programs/goto_convert.cpp | 21 +-- src/goto-programs/goto_convert_functions.cpp | 16 +- .../goto_convert_new_switch_case.cpp | 24 +-- src/goto-programs/goto_functions.cpp | 7 +- src/goto-programs/goto_functions_template.h | 18 +- src/goto-programs/goto_inline.cpp | 14 +- src/goto-programs/goto_program.cpp | 16 +- src/goto-programs/goto_program_irep.cpp | 36 ++-- src/goto-programs/goto_program_template.h | 34 ++-- src/goto-programs/goto_trace.cpp | 89 +++++----- src/goto-programs/graphml_witness.cpp | 2 +- src/goto-programs/interpreter.cpp | 27 +-- src/goto-programs/interpreter_evaluate.cpp | 12 +- src/goto-programs/json_goto_trace.cpp | 76 ++++---- src/goto-programs/link_to_library.cpp | 22 +-- src/goto-programs/remove_asm.cpp | 13 +- .../remove_function_pointers.cpp | 33 ++-- src/goto-programs/remove_skip.cpp | 5 +- src/goto-programs/remove_unreachable.cpp | 7 +- src/goto-programs/remove_unused_functions.cpp | 7 +- .../remove_virtual_functions.cpp | 13 +- src/goto-programs/set_properties.cpp | 6 +- src/goto-programs/show_properties.cpp | 44 ++--- src/goto-programs/string_abstraction.cpp | 36 ++-- src/goto-programs/string_instrumentation.cpp | 30 ++-- src/goto-programs/vcd_goto_trace.cpp | 22 +-- src/goto-programs/write_goto_binary.cpp | 14 +- src/goto-programs/xml_goto_trace.cpp | 104 +++++------ src/goto-symex/auto_objects.cpp | 10 +- src/goto-symex/build_goto_trace.cpp | 6 +- src/goto-symex/symex_target_equation.cpp | 104 ++++++----- src/java_bytecode/jar_file.cpp | 2 +- .../java_bytecode_convert_class.cpp | 14 +- .../java_bytecode_convert_method.cpp | 75 ++++---- .../java_bytecode_parse_tree.cpp | 12 +- src/java_bytecode/java_bytecode_parser.cpp | 14 +- src/java_bytecode/java_class_loader.cpp | 4 +- src/java_bytecode/java_entry_point.cpp | 4 +- src/java_bytecode/java_object_factory.cpp | 2 +- src/solvers/prop/aig_prop.cpp | 2 +- src/solvers/prop/cover_goals.cpp | 6 +- src/solvers/smt1/smt1_conv.cpp | 18 +- src/solvers/smt2/smt2_conv.cpp | 54 +++--- src/symex/path_search.cpp | 4 +- src/symex/symex_cover.cpp | 36 ++-- src/util/base_type.cpp | 4 +- src/util/get_module.cpp | 2 +- src/util/json.cpp | 8 +- src/util/json_expr.cpp | 12 +- src/util/signal_catcher.cpp | 2 +- src/util/simplify_expr.cpp | 69 +++----- src/util/simplify_expr_pointer.cpp | 2 +- src/util/unicode.cpp | 8 +- src/util/xml.cpp | 14 +- src/util/xml_expr.cpp | 12 +- src/xmllang/graphml.h | 2 +- 129 files changed, 1288 insertions(+), 1948 deletions(-) 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..8f487ff7fb0 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; } 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..7b211b1ba1c 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,19 @@ 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();) { 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..25bdff938a7 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'; } /*******************************************************************\ @@ -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,17 +454,14 @@ 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->second != it->second) + if(c_it->second!=src_replace_pair.second) { set_to_bottom(); changed = true; @@ -479,7 +470,7 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src) } else { - set_to(it->first, it->second); + 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..dc92bc69ac0 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; } } @@ -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..602de479a4c 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -119,11 +119,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 +193,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 +325,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 +367,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 +425,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 +502,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 +541,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 +628,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; iid()==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= 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..cdd7add1717 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); } } 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..388f5115d20 100644 --- a/src/analyses/static_analysis.cpp +++ b/src/analyses/static_analysis.cpp @@ -370,13 +370,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 +576,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 +683,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 f5f9c2de4d5..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 @@ -1175,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? @@ -1241,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) @@ -1275,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, diff --git a/src/goto-instrument/accelerate/all_paths_enumerator.cpp b/src/goto-instrument/accelerate/all_paths_enumerator.cpp index f9830744c69..ff81306dbd2 100644 --- a/src/goto-instrument/accelerate/all_paths_enumerator.cpp +++ b/src/goto-instrument/accelerate/all_paths_enumerator.cpp @@ -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/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..5e601eed8f2 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++; } @@ -373,9 +370,8 @@ void dott::find_next( { if(it->is_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/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index 9612c84717d..701cb4bb6ce 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]); } } } @@ -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); } } } @@ -717,20 +707,18 @@ void inline instrumentert::cfg_visitort::visit_cfg_backedge( for(goto_programt::instructionst::iterator 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) + if(targ==t) { target_in_cycle = true; break; 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..86d6070f33c 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(); @@ -127,14 +124,9 @@ bool goto_convert_functionst::hide(const goto_programt &goto_program) i_it!=goto_program.instructions.end(); i_it++) { - 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..34fe02b87b2 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()); } /*******************************************************************\ @@ -161,13 +151,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 +166,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/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..cb61294870d 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); } }; @@ -386,25 +383,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 +413,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 +430,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..44c0abcb641 100644 --- a/src/goto-programs/set_properties.cpp +++ b/src/goto-programs/set_properties.cpp @@ -170,11 +170,7 @@ 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(); 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 59eb2a0ef6b..76446cfd095 100644 --- a/src/goto-programs/vcd_goto_trace.cpp +++ b/src/goto-programs/vcd_goto_trace.cpp @@ -118,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); @@ -145,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++; @@ -162,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..58b53270dd5 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -100,7 +100,7 @@ class java_bytecode_convert_methodt:public messaget 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; @@ -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/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 8d2a85bfac2..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) { diff --git a/src/util/xml_expr.cpp b/src/util/xml_expr.cpp index 11a4ac1d2c6..abdb62e71e9 100644 --- a/src/util/xml_expr.cpp +++ b/src/util/xml_expr.cpp @@ -133,11 +133,11 @@ xmlt xml( result.name="struct"; const struct_typet::componentst &components= to_struct_type(type).components(); - for(const auto & it : components) + for(const auto &component : components) { xmlt &e=result.new_element("member"); - e.set_attribute("name", id2string(it.get_name())); - e.new_element("type").new_element()=xml(it.type(), ns); + e.set_attribute("name", id2string(component.get_name())); + e.new_element("type").new_element()=xml(component.type(), ns); } } else if(type.id()==ID_union) @@ -145,11 +145,11 @@ xmlt xml( result.name="union"; const union_typet::componentst &components= to_union_type(type).components(); - for(const auto & it : components) + for(const auto &component : components) { xmlt &e=result.new_element("member"); - e.set_attribute("name", id2string(it.get_name())); - e.new_element("type").new_element()=xml(it.type(), ns); + e.set_attribute("name", id2string(component.get_name())); + e.new_element("type").new_element()=xml(component.type(), ns); } } else diff --git a/src/xmllang/graphml.h b/src/xmllang/graphml.h index 5a56fef1196..e4830f092ff 100644 --- a/src/xmllang/graphml.h +++ b/src/xmllang/graphml.h @@ -42,7 +42,7 @@ class graphmlt:public graph 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; From 1f4be1ecfbaebf18083492bdbf06c85280c3a7a3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 1 Dec 2016 22:40:19 +0000 Subject: [PATCH 5/8] Use const references where possible This permits compiler optimizations and avoids loss of sharing. --- .../accelerate/acceleration_utils.cpp | 29 ++++++++++++------- .../accelerate/acceleration_utils.h | 20 ++++++++----- .../accelerate/all_paths_enumerator.cpp | 2 +- src/goto-instrument/accelerate/path.h | 16 ++++++---- src/goto-instrument/dot.cpp | 2 +- src/goto-instrument/wmm/goto2graph.cpp | 12 ++++---- src/goto-instrument/wmm/goto2graph.h | 14 ++++----- .../java_bytecode_convert_method.cpp | 4 +-- 8 files changed, 58 insertions(+), 41 deletions(-) diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index 6e3ec3cb495..8c39059fe66 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -50,18 +50,23 @@ void acceleration_utilst::gather_rvalues(const exprt &expr, } } -void acceleration_utilst::find_modified(goto_programt &body, - expr_sett &modified) { - find_modified(body.instructions, modified); +void acceleration_utilst::find_modified( + const goto_programt &body, + expr_sett &modified) +{ + forall_goto_program_instructions(it, body) + find_modified(it, modified); } -void acceleration_utilst::find_modified(goto_programt::instructionst &instructions, - expr_sett &modified) { - for (goto_programt::instructionst::iterator it = instructions.begin(); - it != instructions.end(); - ++it) { +void acceleration_utilst::find_modified( + const goto_programt::instructionst &instructions, + expr_sett &modified) +{ + for(goto_programt::instructionst::const_iterator + it=instructions.begin(); + it!=instructions.end(); + ++it) find_modified(it, modified); - } } void acceleration_utilst::find_modified( @@ -80,8 +85,10 @@ void acceleration_utilst::find_modified( 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 ff81306dbd2..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); 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/dot.cpp b/src/goto-instrument/dot.cpp index 5e601eed8f2..dc00fba3dac 100644 --- a/src/goto-instrument/dot.cpp +++ b/src/goto-instrument/dot.cpp @@ -326,7 +326,7 @@ Function: dott::escape std::string &dott::escape(std::string &str) { - for(unsigned i=0; ifunction]; bool found_pos=false; - goto_programt::instructiont::targett new_targ=targ; + goto_programt::const_targett new_targ=targ; if(in_pos[targ].empty()) { @@ -679,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()) @@ -704,7 +704,7 @@ 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(const auto &in : cur->incoming_edges) @@ -1494,7 +1494,7 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet& cyc) { bool target_in_cycle = false; - Forall_goto_program_instructions(targ, interleaving) + forall_goto_program_instructions(targ, interleaving) if(targ==t) { target_in_cycle = true; 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/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 58b53270dd5..ccdd54db7e2 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -95,7 +95,7 @@ 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) @@ -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()) From 91430c6f14d8411985eaf53535ed32529bf60a1c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 17 Dec 2016 18:15:43 +0000 Subject: [PATCH 6/8] Use forall_goto_functions, forall_goto_program_instructions --- src/aa-symex/path_search.cpp | 14 ++++---------- src/analyses/flow_insensitive_analysis.cpp | 10 ++-------- src/analyses/goto_check.cpp | 15 +++------------ src/analyses/static_analysis.cpp | 15 +++------------ src/goto-instrument/dot.cpp | 7 +------ src/goto-instrument/unwind.cpp | 3 +-- src/goto-programs/goto_convert_functions.cpp | 5 +---- src/goto-programs/goto_program_irep.cpp | 5 +---- src/goto-programs/loop_ids.cpp | 12 +++--------- src/goto-programs/property_checker.cpp | 16 +++++----------- src/goto-programs/remove_function_pointers.cpp | 5 +---- src/goto-programs/set_properties.cpp | 5 +---- src/goto-programs/show_goto_functions.cpp | 10 ++-------- 13 files changed, 28 insertions(+), 94 deletions(-) diff --git a/src/aa-symex/path_search.cpp b/src/aa-symex/path_search.cpp index 8f487ff7fb0..9b8d2295a45 100644 --- a/src/aa-symex/path_search.cpp +++ b/src/aa-symex/path_search.cpp @@ -491,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/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp index 32c14bcc197..b2dbb5fe930 100644 --- a/src/analyses/flow_insensitive_analysis.cpp +++ b/src/analyses/flow_insensitive_analysis.cpp @@ -132,10 +132,7 @@ void flow_insensitive_analysis_baset::output( const goto_functionst &goto_functions, std::ostream &out) { - 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) { out << "////" << std::endl; out << "//// Function: " << f_it->first << std::endl; @@ -547,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/goto_check.cpp b/src/analyses/goto_check.cpp index cdd7add1717..131b7890de5 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1729,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()) { @@ -1805,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); } @@ -1833,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/static_analysis.cpp b/src/analyses/static_analysis.cpp index 388f5115d20..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); } diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp index dc00fba3dac..4bd1215ebba 100644 --- a/src/goto-instrument/dot.cpp +++ b/src/goto-instrument/dot.cpp @@ -297,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); 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-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 86d6070f33c..c4ec6ea43c7 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -119,10 +119,7 @@ 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(const auto &label : i_it->labels) if(label=="__CPROVER_HIDE") diff --git a/src/goto-programs/goto_program_irep.cpp b/src/goto-programs/goto_program_irep.cpp index 34fe02b87b2..2f9f491d58e 100644 --- a/src/goto-programs/goto_program_irep.cpp +++ b/src/goto-programs/goto_program_irep.cpp @@ -109,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()); 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_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index cb61294870d..7a25def3823 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -106,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; } diff --git a/src/goto-programs/set_properties.cpp b/src/goto-programs/set_properties.cpp index 44c0abcb641..4f345e5eab0 100644 --- a/src/goto-programs/set_properties.cpp +++ b/src/goto-programs/set_properties.cpp @@ -172,10 +172,7 @@ void set_properties( 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(); From 806d4abd0f7e6b53a8b2bc5451d4322988c6b0bd Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 17 Dec 2016 18:17:20 +0000 Subject: [PATCH 7/8] Adjust spacing, line breaks to coding guidelines Also added to comments to for loops that do not include increments in the loop header. --- src/analyses/cfg_dominators.h | 6 ++++-- src/analyses/constant_propagator.cpp | 8 ++++---- src/analyses/custom_bitvector_analysis.cpp | 2 +- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/analyses/cfg_dominators.h b/src/analyses/cfg_dominators.h index 7b211b1ba1c..01ca0871a16 100644 --- a/src/analyses/cfg_dominators.h +++ b/src/analyses/cfg_dominators.h @@ -221,8 +221,10 @@ void cfg_dominators_templatet::output(std::ostream &out) const out << n << " post-dominated by "; else out << n << " dominated by "; - for(typename target_sett::const_iterator d_it=node.second.dominators.begin(); - d_it!=node.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!=node.second.dominators.end()) diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 25bdff938a7..c7d5879d858 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -398,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()) @@ -459,19 +459,19 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src) 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!=src_replace_pair.second) { set_to_bottom(); - changed = true; + changed=true; break; } } else { set_to(src_replace_pair.first, src_replace_pair.second); - changed = true; + changed=true; } } diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index dc92bc69ac0..5155d13b7e5 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -678,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); From e85e808327ba13e097a06d6db4f01857758e1064 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 20 Dec 2016 22:05:51 +0100 Subject: [PATCH 8/8] Header cleanup --- src/analyses/escape_analysis.cpp | 2 -- src/musketeer/musketeer_parse_options.cpp | 1 + 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index 602de479a4c..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 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