Merge pull request #859 from reuk/goto-prog-style

Daniel Kroening · web-flow · commit cf1b4b4b7209 · 2017-05-03T16:20:57.000+01:00
Improve style in goto_program_template.h
diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
@@ -412,11 +412,7 @@ bool ai_baset::visit(
 
   statet &current=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
@@ -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
@@ -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
@@ -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<ftype>(&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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
diff --git a/src/goto-programs/remove_unreachable.cpp b/src/goto-programs/remove_unreachable.cpp

Original file line number	Diff line number	Diff line change
`@@ -69,8 +69,7 @@ int all_paths_enumeratort::backtrack(patht &path)`
`69`	`69`	`path.pop_back();`
`70`	`70`
`71`	`71`	`path_nodet &parent=path.back();`
`72`		`- goto_programt::targetst succs;`
`73`		`- goto_program.get_successors(parent.loc, succs);`
	`72`	`+ const auto succs=goto_program.get_successors(parent.loc);`
`74`	`73`
`75`	`74`	`unsigned int ret=0;`
`76`	`75`
`@@ -119,12 +118,9 @@ void all_paths_enumeratort::extend_path(`
`119`	`118`	`int succ)`
`120`	`119`	`{`
`121`	`120`	`goto_programt::targett next;`
`122`		`- goto_programt::targetst succs;`
`123`	`121`	`exprt guard=true_exprt();`
`124`	`122`
`125`		`- goto_program.get_successors(t, succs);`
`126`		`-`
`127`		`- for(const auto &s : succs)`
	`123`	`+ for(const auto &s : goto_program.get_successors(t))`
`128`	`124`	`{`
`129`	`125`	`if(succ==0)`
`130`	`126`	`{`
Original file line number	Diff line number	Diff line change
`@@ -757,23 +757,19 @@ void disjunctive_polynomial_accelerationt::find_distinguishing_points()`
`757`	`757`	`it!=loop.end();`
`758`	`758`	`++it)`
`759`	`759`	`{`
`760`		`- goto_programt::targetst succs;`
`761`		`-`
`762`		`- goto_program.get_successors(*it, succs);`
	`760`	`+ const auto succs=goto_program.get_successors(*it);`
`763`	`761`
`764`	`762`	`if(succs.size() > 1)`
`765`	`763`	`{`
`766`	`764`	`// This location has multiple successors -- each successor is a`
`767`	`765`	`// distinguishing point.`
`768`		`- for(goto_programt::targetst::iterator jt=succs.begin();`
`769`		`- jt!=succs.end();`
`770`		`- ++jt)`
	`766`	`+ for(const auto &jt : succs)`
`771`	`767`	`{`
`772`	`768`	`symbolt distinguisher_sym =`
`773`	`769`	`utils.fresh_symbol("polynomial::distinguisher", bool_typet());`
`774`	`770`	`symbol_exprt distinguisher=distinguisher_sym.symbol_expr();`
`775`	`771`
`776`		`- distinguishing_points[*jt]=distinguisher;`
	`772`	`+ distinguishing_points[jt]=distinguisher;`
`777`	`773`	`distinguishers.push_back(distinguisher);`
`778`	`774`	`}`
`779`	`775`	`}`
`@@ -788,9 +784,8 @@ void disjunctive_polynomial_accelerationt::build_path(`
`788`	`784`	`do`
`789`	`785`	`{`
`790`	`786`	`goto_programt::targett next;`
`791`		`- goto_programt::targetst succs;`
`792`	`787`
`793`		`- goto_program.get_successors(t, succs);`
	`788`	`+ const auto succs=goto_program.get_successors(t);`
`794`	`789`
`795`	`790`	`// We should have a looping path, so we should never hit a location`
`796`	`791`	`// with no successors.`
Original file line number	Diff line number	Diff line change
`@@ -109,9 +109,7 @@ void sat_path_enumeratort::find_distinguishing_points()`
`109`	`109`	`it!=loop.end();`
`110`	`110`	`++it)`
`111`	`111`	`{`
`112`		`- goto_programt::targetst succs;`
`113`		`-`
`114`		`- goto_program.get_successors(*it, succs);`
	`112`	`+ const auto succs=goto_program.get_successors(*it);`
`115`	`113`
`116`	`114`	`if(succs.size()>1)`
`117`	`115`	`{`
`@@ -139,9 +137,7 @@ void sat_path_enumeratort::build_path(`
`139`	`137`	`do`
`140`	`138`	`{`
`141`	`139`	`goto_programt::targett next;`
`142`		`- goto_programt::targetst succs;`
`143`		`-`
`144`		`- goto_program.get_successors(t, succs);`
	`140`	`+ const auto succs=goto_program.get_successors(t);`
`145`	`141`
`146`	`142`	`// We should have a looping path, so we should never hit a location`
`147`	`143`	`// with no successors.`
Original file line number	Diff line number	Diff line change
`@@ -38,10 +38,7 @@ void trace_automatont::build_alphabet(goto_programt &program)`
`38`	`38`	`{`
`39`	`39`	`Forall_goto_program_instructions(it, program)`
`40`	`40`	`{`
`41`		`- goto_programt::targetst succs;`
`42`		`-`
`43`		`- program.get_successors(it, succs);`
`44`		`-`
	`41`	`+ const auto succs=program.get_successors(it);`
`45`	`42`	`if(succs.size()>1)`
`46`	`43`	`{`
`47`	`44`	`alphabet.insert(succs.begin(), succs.end());`
Original file line number	Diff line number	Diff line change
`@@ -62,14 +62,11 @@ void show_call_sequences(`
`62`	`62`	`continue; // abort search`
`63`	`63`	`}`
`64`	`64`
`65`		`- // get successors`
`66`		`- goto_programt::const_targetst s;`
`67`		`- goto_program.get_successors(t, s);`
`68`		`-`
`69`		`- // add to stack`
`70`		`- for(goto_programt::const_targetst::const_iterator`
`71`		`- it=s.begin(); it!=s.end(); it++)`
`72`		`- stack.push(*it);`
	`65`	`+ // get successors and add to stack`
	`66`	`+ for(const auto &it : goto_program.get_successors(t))`
	`67`	`+ {`
	`68`	`+ stack.push(it);`
	`69`	`+ }`
`73`	`70`	`}`
`74`	`71`	`}`
`75`	`72`
Original file line number	Diff line number	Diff line change
`@@ -217,8 +217,7 @@ void dott::write_dot_subgraph(`
`217`	`217`	`write_edge(out, it, *frit, flabel);`
`218`	`218`
`219`	`219`	`seen.insert(it);`
`220`		`- goto_programt::const_targetst temp;`
`221`		`- goto_program.get_successors(it, temp);`
	`220`	`+ const auto temp=goto_program.get_successors(it);`
`222`	`221`	`worklist.insert(worklist.end(), temp.begin(), temp.end());`
`223`	`222`	`}`
`224`	`223`	`}`