diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index 2d1f4f6b986..45d4b83c92c 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -412,11 +412,7 @@ bool ai_baset::visit( statet ¤t=get_state(l); - goto_programt::const_targetst successors; - - goto_program.get_successors(l, successors); - - for(const auto &to_l : successors) + for(const auto &to_l : goto_program.get_successors(l)) { if(to_l==goto_program.instructions.end()) continue; diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp index c2cd188352d..bc4dd11e889 100644 --- a/src/analyses/flow_insensitive_analysis.cpp +++ b/src/analyses/flow_insensitive_analysis.cpp @@ -256,16 +256,13 @@ bool flow_insensitive_analysis_baset::visit( l->location_number << std::endl; #endif - goto_programt::const_targetst successors; - goto_program.get_successors(l, successors); - seen_locations.insert(l); if(statistics.find(l)==statistics.end()) statistics[l]=1; else statistics[l]++; - for(const auto &to_l : successors) + for(const auto &to_l : goto_program.get_successors(l)) { if(to_l==goto_program.instructions.end()) continue; diff --git a/src/analyses/static_analysis.cpp b/src/analyses/static_analysis.cpp index 96d7e5a9d9a..8309566f27d 100644 --- a/src/analyses/static_analysis.cpp +++ b/src/analyses/static_analysis.cpp @@ -356,11 +356,7 @@ bool static_analysis_baset::visit( current.seen=true; - goto_programt::const_targetst successors; - - goto_program.get_successors(l, successors); - - for(const auto &to_l : successors) + for(const auto &to_l : goto_program.get_successors(l)) { if(to_l==goto_program.instructions.end()) continue; diff --git a/src/cegis/cegis-util/program_helper.cpp b/src/cegis/cegis-util/program_helper.cpp index 88520f879f6..e1dc0ff3d6f 100644 --- a/src/cegis/cegis-util/program_helper.cpp +++ b/src/cegis/cegis-util/program_helper.cpp @@ -350,18 +350,23 @@ goto_programt::targett insert_preserving_source_location( goto_programt::targett insert_after_preserving_source_location( goto_programt &body, goto_programt::targett pos) { - const auto op=std::bind1st(std::mem_fun(&goto_programt::insert_after), &body); - return insert_preserving_source_location(pos, op); + return insert_preserving_source_location( + pos, + [&](goto_programt::const_targett target) + { + return body.insert_after(target); + }); } goto_programt::targett insert_before_preserving_source_location( goto_programt &body, goto_programt::targett pos) { - typedef goto_programt::targett (goto_programt::*ftype)( - goto_programt::targett); - const auto op=std::bind1st( - std::mem_fun(static_cast(&goto_programt::insert_before)), &body); - return insert_preserving_source_location(pos, op); + return insert_preserving_source_location( + pos, + [&](goto_programt::const_targett target) + { + return body.insert_before(target); + }); } void assign_in_cprover_init(goto_functionst &gf, symbolt &symbol, diff --git a/src/goto-instrument/accelerate/all_paths_enumerator.cpp b/src/goto-instrument/accelerate/all_paths_enumerator.cpp index 8b1038d426d..b8db795bdfd 100644 --- a/src/goto-instrument/accelerate/all_paths_enumerator.cpp +++ b/src/goto-instrument/accelerate/all_paths_enumerator.cpp @@ -69,8 +69,7 @@ int all_paths_enumeratort::backtrack(patht &path) path.pop_back(); path_nodet &parent=path.back(); - goto_programt::targetst succs; - goto_program.get_successors(parent.loc, succs); + const auto succs=goto_program.get_successors(parent.loc); unsigned int ret=0; @@ -119,12 +118,9 @@ void all_paths_enumeratort::extend_path( int succ) { goto_programt::targett next; - goto_programt::targetst succs; exprt guard=true_exprt(); - goto_program.get_successors(t, succs); - - for(const auto &s : succs) + for(const auto &s : goto_program.get_successors(t)) { if(succ==0) { diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp index 29d5ac0f81b..e2ede0567cb 100644 --- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp +++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp @@ -757,23 +757,19 @@ void disjunctive_polynomial_accelerationt::find_distinguishing_points() it!=loop.end(); ++it) { - goto_programt::targetst succs; - - goto_program.get_successors(*it, succs); + const auto succs=goto_program.get_successors(*it); 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 &jt : succs) { symbolt distinguisher_sym = utils.fresh_symbol("polynomial::distinguisher", bool_typet()); symbol_exprt distinguisher=distinguisher_sym.symbol_expr(); - distinguishing_points[*jt]=distinguisher; + distinguishing_points[jt]=distinguisher; distinguishers.push_back(distinguisher); } } @@ -788,9 +784,8 @@ void disjunctive_polynomial_accelerationt::build_path( do { goto_programt::targett next; - goto_programt::targetst succs; - goto_program.get_successors(t, succs); + const auto succs=goto_program.get_successors(t); // We should have a looping path, so we should never hit a location // with no successors. diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp index d8067ec3640..2a64a2d5949 100644 --- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp +++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp @@ -109,9 +109,7 @@ void sat_path_enumeratort::find_distinguishing_points() it!=loop.end(); ++it) { - goto_programt::targetst succs; - - goto_program.get_successors(*it, succs); + const auto succs=goto_program.get_successors(*it); if(succs.size()>1) { @@ -139,9 +137,7 @@ void sat_path_enumeratort::build_path( do { goto_programt::targett next; - goto_programt::targetst succs; - - goto_program.get_successors(t, succs); + const auto succs=goto_program.get_successors(t); // We should have a looping path, so we should never hit a location // with no successors. diff --git a/src/goto-instrument/accelerate/trace_automaton.cpp b/src/goto-instrument/accelerate/trace_automaton.cpp index 10682862e7b..086b1be7d31 100644 --- a/src/goto-instrument/accelerate/trace_automaton.cpp +++ b/src/goto-instrument/accelerate/trace_automaton.cpp @@ -38,10 +38,7 @@ void trace_automatont::build_alphabet(goto_programt &program) { Forall_goto_program_instructions(it, program) { - goto_programt::targetst succs; - - program.get_successors(it, succs); - + const auto succs=program.get_successors(it); if(succs.size()>1) { alphabet.insert(succs.begin(), succs.end()); diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-instrument/call_sequences.cpp index 875d89051a6..d8c651bd1a7 100644 --- a/src/goto-instrument/call_sequences.cpp +++ b/src/goto-instrument/call_sequences.cpp @@ -62,14 +62,11 @@ void show_call_sequences( continue; // abort search } - // get successors - goto_programt::const_targetst s; - goto_program.get_successors(t, s); - - // add to stack - for(goto_programt::const_targetst::const_iterator - it=s.begin(); it!=s.end(); it++) - stack.push(*it); + // get successors and add to stack + for(const auto &it : goto_program.get_successors(t)) + { + stack.push(it); + } } } diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp index 8fc7cd3449a..455381c4c51 100644 --- a/src/goto-instrument/dot.cpp +++ b/src/goto-instrument/dot.cpp @@ -217,8 +217,7 @@ void dott::write_dot_subgraph( write_edge(out, *it, **frit, flabel); seen.insert(it); - goto_programt::const_targetst temp; - goto_program.get_successors(it, temp); + const auto temp=goto_program.get_successors(it); worklist.insert(worklist.end(), temp.begin(), temp.end()); } } diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index bdd97555c06..beb96579f34 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -1541,7 +1541,7 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet &cyc) map.insert(p); goto_functionst this_interleaving; - this_interleaving.function_map=map; + this_interleaving.function_map=std::move(map); optionst no_option; null_message_handlert no_message; diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index 14f9e4a519e..6b42ad250ea 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -60,24 +60,13 @@ class goto_program_templatet \param[in] src an empty goto program \remark Use copy_from to copy non-empty goto-programs */ - goto_program_templatet(const goto_program_templatet &src) - { - // DO NOT COPY ME! I HAVE POINTERS IN ME! - assert(src.instructions.empty()); - } + goto_program_templatet(const goto_program_templatet &src)=delete; /*! \brief assignment operator \param[in] src an empty goto program \remark Use copy_from to copy non-empty goto-programs */ - goto_program_templatet &operator=(const goto_program_templatet &src) - { - // DO NOT COPY ME! I HAVE POINTERS IN ME! - assert(src.instructions.empty()); - instructions.clear(); - update(); - return *this; - } + goto_program_templatet &operator=(const goto_program_templatet &src)=delete; /*! \brief Container for an instruction of the goto-program */ @@ -193,11 +182,7 @@ class goto_program_templatet bool is_end_function () const { return type==END_FUNCTION; } instructiont(): - source_location(static_cast(get_nil_irep())), - type(NO_INSTRUCTION_TYPE), - guard(true_exprt()), - location_number(0), - target_number(nil_target) + instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit) { } @@ -206,6 +191,7 @@ class goto_program_templatet type(_type), guard(true_exprt()), location_number(0), + loop_number(0), target_number(nil_target) { } @@ -213,12 +199,13 @@ class goto_program_templatet //! swap two instructions void swap(instructiont &instruction) { - instruction.code.swap(code); - instruction.source_location.swap(source_location); - std::swap(instruction.type, type); - instruction.guard.swap(guard); - instruction.targets.swap(targets); - instruction.function.swap(function); + using std::swap; + swap(instruction.code, code); + swap(instruction.source_location, source_location); + swap(instruction.type, type); + swap(instruction.guard, guard); + swap(instruction.targets, targets); + swap(instruction.function, function); } //! Uniquely identify an invalid target or location @@ -292,7 +279,7 @@ class goto_program_templatet const_targett l) { while(!l->is_end_function()) - l++; + ++l; return l->function; } @@ -305,13 +292,8 @@ class goto_program_templatet return get_function_id(--p.instructions.end()); } - void get_successors( - targett target, - targetst &successors); - - void get_successors( - const_targett target, - const_targetst &successors) const; + template + std::list get_successors(Target target) const; void compute_incoming_edges(); @@ -319,8 +301,7 @@ class goto_program_templatet void insert_before_swap(targett target) { assert(target!=instructions.end()); - targett next=target; - next++; + const auto next=std::next(target); instructions.insert(next, instructiont())->swap(*target); } @@ -342,19 +323,11 @@ class goto_program_templatet if(p.instructions.empty()) return; insert_before_swap(target, p.instructions.front()); - targett next=target; - next++; + auto next=std::next(target); p.instructions.erase(p.instructions.begin()); instructions.splice(next, p.instructions); } - //! Insertion before the given target - //! \return newly inserted location - targett insert_before(targett target) - { - return instructions.insert(target, instructiont()); - } - //! Insertion before the given target //! \return newly inserted location targett insert_before(const_targett target) @@ -364,11 +337,9 @@ class goto_program_templatet //! Insertion after the given target //! \return newly inserted location - targett insert_after(targett target) + targett insert_after(const_targett target) { - targett t=target; - t++; - return instructions.insert(t, instructiont()); + return instructions.insert(std::next(target), instructiont()); } //! Appends the given program, which is destroyed @@ -379,16 +350,6 @@ class goto_program_templatet // BUG: The iterators to p-instructions are invalidated! } - //! Inserts the given program at the given location. - //! The program is destroyed. - void destructive_insert( - targett target, - goto_program_templatet &p) - { - instructions.splice(target, p.instructions); - // BUG: The iterators to p-instructions are invalidated! - } - //! Inserts the given program at the given location. //! The program is destroyed. void destructive_insert( @@ -494,7 +455,7 @@ class goto_program_templatet targett get_end_function() { assert(!instructions.empty()); - targett end_function=--instructions.end(); + const auto end_function=std::prev(instructions.end()); assert(end_function->is_end_function()); return end_function; } @@ -516,99 +477,63 @@ void goto_program_templatet::compute_loop_numbers() } template -void goto_program_templatet::get_successors( - targett target, - targetst &successors) +template +std::list goto_program_templatet::get_successors( + Target target) const { - successors.clear(); if(target==instructions.end()) - return; + return std::list(); - targett next=target; - next++; + const auto next=std::next(target); const instructiont &i=*target; if(i.is_goto()) { - for(const auto &t : i.targets) - successors.push_back(t); + std::list successors(i.targets.begin(), i.targets.end()); if(!i.guard.is_true() && next!=instructions.end()) successors.push_back(next); + + return successors; } - else if(i.is_start_thread()) + + if(i.is_start_thread()) { - for(const auto &t : i.targets) - successors.push_back(t); + std::list successors(i.targets.begin(), i.targets.end()); if(next!=instructions.end()) successors.push_back(next); + + return successors; } - else if(i.is_end_thread()) + + if(i.is_end_thread()) { // no successors + return std::list(); } - else if(i.is_throw()) + + if(i.is_throw()) { // the successors are non-obvious + return std::list(); } - else if(i.is_assume()) - { - if(!i.guard.is_false() && next!=instructions.end()) - successors.push_back(next); - } - else - { - if(next!=instructions.end()) - successors.push_back(next); - } -} - -template -void goto_program_templatet::get_successors( - const_targett target, - const_targetst &successors) const -{ - successors.clear(); - if(target==instructions.end()) - return; - - const_targett next=target; - next++; - - const instructiont &i=*target; - if(i.is_goto()) + if(i.is_assume()) { - for(const auto &t : i.targets) - successors.push_back(t); - - if(!i.guard.is_true() && next!=instructions.end()) - successors.push_back(next); + return + !i.guard.is_false() && next!=instructions.end() ? + std::list{next} : + std::list(); } - else if(i.is_start_thread()) - { - for(const auto &t : i.targets) - successors.push_back(t); - if(next!=instructions.end()) - successors.push_back(next); - } - else if(i.is_end_thread()) + if(next!=instructions.end()) { - // no successors - } - else if(i.is_assume()) - { - if(!i.guard.is_false() && next!=instructions.end()) - successors.push_back(next); - } - else - { - if(next!=instructions.end()) - successors.push_back(next); + return std::list{next}; } + + return std::list(); } #include @@ -633,7 +558,7 @@ std::ostream &goto_program_templatet::output( for(typename instructionst::const_iterator it=instructions.begin(); it!=instructions.end(); - it++) + ++it) output_instruction(ns, identifier, out, it); return out; @@ -701,9 +626,9 @@ void goto_program_templatet::copy_from( for(typename instructionst::const_iterator it=src.instructions.begin(); it!=src.instructions.end(); - it++) + ++it) { - targett new_instruction=add_instruction(); + auto new_instruction=add_instruction(); targets_mapping[it]=new_instruction; *new_instruction=*it; } @@ -750,13 +675,9 @@ void goto_program_templatet::compute_incoming_edges() for(typename instructionst::iterator it=instructions.begin(); it!=instructions.end(); - it++) + ++it) { - targetst successors; - - get_successors(it, successors); - - for(const auto &s : successors) + for(const auto &s : get_successors(it)) { if(s!=instructions.end()) s->incoming_edges.insert(it); diff --git a/src/goto-programs/remove_unreachable.cpp b/src/goto-programs/remove_unreachable.cpp index 38f8e93974a..14f92e97be1 100644 --- a/src/goto-programs/remove_unreachable.cpp +++ b/src/goto-programs/remove_unreachable.cpp @@ -39,10 +39,8 @@ void remove_unreachable(goto_programt &goto_program) t!=goto_program.instructions.end()) { reachable.insert(t); - goto_programt::targetst successors; - goto_program.get_successors(t, successors); - for(const auto &succ : successors) + for(const auto &succ : goto_program.get_successors(t)) working.push(succ); } }