Remove unused parameters in goto-instrument/wmm

tautschnig · tautschnig · commit 461754d2dbad · 2018-06-25T22:30:02.000+01:00
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -1245,9 +1245,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
         /* default: instruments all unsafe pairs */
         inst_strategy=all;
 
-      const unsigned unwind_loops=
-        cmdline.isset("unwind")?
-        unsafe_string2unsigned(cmdline.get_value("unwind")):0;
       const unsigned max_var=
         cmdline.isset("max-var")?
         unsafe_string2unsigned(cmdline.get_value("max-var")):0;
@@ -1295,7 +1292,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
           goto_model,
           cmdline.isset("scc"),
           inst_strategy,
-          unwind_loops,
           !cmdline.isset("cfg-kill"),
           cmdline.isset("no-dependencies"),
           loops,
diff --git a/src/goto-instrument/wmm/event_graph.cpp b/src/goto-instrument/wmm/event_graph.cpp
@@ -1098,8 +1098,7 @@ std::string event_grapht::critical_cyclet::print_output() const
 std::string event_grapht::critical_cyclet::print_detail(
   const critical_cyclet &reduced,
   std::map<std::string, std::string> &map_id2var,
-  std::map<std::string, std::string> &map_var2id,
-  memory_modelt model) const
+  std::map<std::string, std::string> &map_var2id) const
 {
   std::string cycle;
   for(const_iterator it=reduced.begin(); it!=reduced.end(); ++it)
@@ -1140,13 +1139,13 @@ std::string event_grapht::critical_cyclet::print_all(
     critical_cyclet reduced(egraph, id);
     this->hide_internals(reduced);
     assert(reduced.size() > 0);
-    cycle+=print_detail(reduced, map_id2var, map_var2id, model);
+    cycle+=print_detail(reduced, map_id2var, map_var2id);
     cycle+=": ";
     cycle+=print_name(reduced, model);
   }
   else
   {
-    cycle+=print_detail(*this, map_id2var, map_var2id, model);
+    cycle+=print_detail(*this, map_id2var, map_var2id);
     cycle+=": ";
     cycle+=print_name(*this, model);
   }
diff --git a/src/goto-instrument/wmm/event_graph.h b/src/goto-instrument/wmm/event_graph.h
@@ -48,8 +48,7 @@ class event_grapht
 
     std::string print_detail(const critical_cyclet &reduced,
       std::map<std::string, std::string> &map_id2var,
-      std::map<std::string, std::string> &map_var2id,
-      memory_modelt model) const;
+      std::map<std::string, std::string> &map_var2id) const;
     std::string print_name(const critical_cyclet &redyced,
       memory_modelt model) const;
 
@@ -377,7 +376,7 @@ class event_grapht
     {}
 
     void set_naive() {naive=true;}
-    void collect_pairs(namespacet &ns);
+    void collect_pairs();
   };
 
 public:
@@ -577,17 +576,17 @@ class event_grapht
 
   /* collects all the pairs of events with respectively at least one cmp,
      regardless of the architecture (Pensieve'05 strategy) */
-  void collect_pairs(namespacet &ns)
+  void collect_pairs()
   {
     graph_pensieve_explorert exploration(*this, max_var, max_po_trans);
-    exploration.collect_pairs(ns);
+    exploration.collect_pairs();
   }
 
-  void collect_pairs_naive(namespacet &ns)
+  void collect_pairs_naive()
   {
     graph_pensieve_explorert exploration(*this, max_var, max_po_trans);
     exploration.set_naive();
-    exploration.collect_pairs(ns);
+    exploration.collect_pairs();
   }
 };
 #endif // CPROVER_GOTO_INSTRUMENT_WMM_EVENT_GRAPH_H
diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp
@@ -152,8 +152,6 @@ void instrumentert::cfg_visitort::visit_cfg_function(
     loop_strategyt replicate_body,
     /* function to analyse */
     const irep_idt &function,
-    /* incoming edges */
-    const std::set<instrumentert::cfg_visitort::nodet> &initial_vertex,
     /* outcoming edges */
     std::set<instrumentert::cfg_visitort::nodet> &ending_vertex)
 {
@@ -657,11 +655,6 @@ void instrumentert::cfg_visitort::visit_cfg_function_call(
   loop_strategyt replicate_body)
 {
   const goto_programt::instructiont &instruction=*i_it;
-  std::set<nodet> s;
-  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();
@@ -689,7 +682,7 @@ void instrumentert::cfg_visitort::visit_cfg_function_call(
       {
         /* just inlines */
         /* TODO */
-        visit_cfg_function(value_sets, model, no_dependencies, fun_id, s,
+        visit_cfg_function(value_sets, model, no_dependencies, fun_id,
           in_pos[i_it]);
         updated.insert(i_it);
       }
@@ -699,7 +692,7 @@ void instrumentert::cfg_visitort::visit_cfg_function_call(
     {
       /* normal inlining strategy */
       visit_cfg_function(value_sets, model, no_dependencies, replicate_body,
-        fun_id, s, in_pos[i_it]);
+        fun_id, in_pos[i_it]);
       updated.insert(i_it);
     }
 
diff --git a/src/goto-instrument/wmm/goto2graph.h b/src/goto-instrument/wmm/goto2graph.h
@@ -245,10 +245,9 @@ class instrumentert
       {
         /* forbids recursive function */
         enter_function(function);
-        const std::set<nodet> empty_in;
         std::set<nodet> end_out;
         visit_cfg_function(value_sets, model, no_dependencies, duplicate_body,
-          function, empty_in, end_out);
+          function, end_out);
         leave_function(function);
       }
       catch(const std::string &s)
@@ -266,8 +265,6 @@ class instrumentert
       loop_strategyt duplicate_body,
       /// function to analyse
       const irep_idt &function,
-      /// incoming edges
-      const std::set<nodet> &initial_vertex,
       /// outcoming edges
       std::set<nodet> &ending_vertex);
 
diff --git a/src/goto-instrument/wmm/instrumenter_pensieve.h b/src/goto-instrument/wmm/instrumenter_pensieve.h
@@ -26,15 +26,15 @@ class instrumenter_pensievet:public instrumentert
   {
   }
 
-  void collect_pairs_naive(namespacet &ns)
+  void collect_pairs_naive()
   {
-    egraph.collect_pairs_naive(ns);
+    egraph.collect_pairs_naive();
   }
 
   /* collects directly all the pairs in the graph */
-  void collect_pairs(namespacet &ns)
+  void collect_pairs()
   {
-    egraph.collect_pairs(ns);
+    egraph.collect_pairs();
   }
 };
 
diff --git a/src/goto-instrument/wmm/pair_collection.cpp b/src/goto-instrument/wmm/pair_collection.cpp
@@ -22,7 +22,7 @@ Date: 2013
 #define OUTPUT(s, fence, file, line, id, type)  \
   s<<fence<<"|"<<file<<"|"<<line<<"|"<<id<<"|"<<type<<'\n'
 
-void event_grapht::graph_pensieve_explorert::collect_pairs(namespacet &ns)
+void event_grapht::graph_pensieve_explorert::collect_pairs()
 {
   std::ofstream res;
   res.open("results.txt");
diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp
@@ -970,11 +970,10 @@ bool shared_bufferst::is_buffered(
   if(instrumentations.find(identifier)!=instrumentations.end())
     return false; // these are instrumentations
 
-  return is_buffered_in_general(ns, symbol_expr, is_write);
+  return is_buffered_in_general(symbol_expr, is_write);
 }
 
 bool shared_bufferst::is_buffered_in_general(
-  const namespacet &ns,
   const symbol_exprt &symbol_expr,
   bool is_write
   // are we asking for the variable (false), or for the variable and the
@@ -1042,7 +1041,7 @@ void shared_bufferst::affected_by_delay(
             message.debug() <<"debug: "<<id2string(w_it->second.object)
               <<" reads from "<<id2string(r_it->second.object)
               <<messaget::eom;
-            if(is_buffered_in_general(ns, r_it->second.symbol_expr, true))
+            if(is_buffered_in_general(r_it->second.symbol_expr, true))
               // shouldn't it be true? false => overapprox
               affected_by_delay_set.insert(w_it->second.object);
           }
diff --git a/src/goto-instrument/wmm/shared_buffers.h b/src/goto-instrument/wmm/shared_buffers.h
@@ -173,7 +173,6 @@ class shared_bufferst
     bool is_write);
 
   bool is_buffered_in_general(
-    const namespacet&,
     const symbol_exprt&,
     bool is_write);
 
diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp
@@ -107,7 +107,6 @@ void weak_memory(
   goto_modelt &goto_model,
   bool SCC,
   instrumentation_strategyt event_strategy,
-  unsigned unwinding_bound,
   bool no_cfg_kill,
   bool no_dependencies,
   loop_strategyt duplicate_body,
diff --git a/src/goto-instrument/wmm/weak_memory.h b/src/goto-instrument/wmm/weak_memory.h
@@ -31,7 +31,6 @@ void weak_memory(
   goto_modelt &,
   bool SCC,
   instrumentation_strategyt event_stategy,
-  unsigned unwinding_bound,
   bool no_cfg_kill,
   bool no_dependencies,
   loop_strategyt duplicate_body,

Original file line number	Diff line number	Diff line change
`@@ -152,8 +152,6 @@ void instrumentert::cfg_visitort::visit_cfg_function(`
`152`	`152`	`loop_strategyt replicate_body,`
`153`	`153`	`/* function to analyse */`
`154`	`154`	`const irep_idt &function,`
`155`		`- /* incoming edges */`
`156`		`- const std::set<instrumentert::cfg_visitort::nodet> &initial_vertex,`
`157`	`155`	`/* outcoming edges */`
`158`	`156`	`std::set<instrumentert::cfg_visitort::nodet> &ending_vertex)`
`159`	`157`	`{`
`@@ -657,11 +655,6 @@ void instrumentert::cfg_visitort::visit_cfg_function_call(`
`657`	`655`	`loop_strategyt replicate_body)`
`658`	`656`	`{`
`659`	`657`	`const goto_programt::instructiont &instruction=*i_it;`
`660`		`- std::set<nodet> s;`
`661`		`- for(const auto &in : instruction.incoming_edges)`
`662`		`- if(in_pos.find(in)!=in_pos.end())`
`663`		`- for(const auto &node : in_pos[in])`
`664`		`- s.insert(node);`
`665`	`658`
`666`	`659`	`const exprt &fun=to_code_function_call(instruction.code).function();`
`667`	`660`	`const irep_idt &fun_id=to_symbol_expr(fun).get_identifier();`
`@@ -689,7 +682,7 @@ void instrumentert::cfg_visitort::visit_cfg_function_call(`
`689`	`682`	`{`
`690`	`683`	`/* just inlines */`
`691`	`684`	`/* TODO */`
`692`		`- visit_cfg_function(value_sets, model, no_dependencies, fun_id, s,`
	`685`	`+ visit_cfg_function(value_sets, model, no_dependencies, fun_id,`
`693`	`686`	`in_pos[i_it]);`
`694`	`687`	`updated.insert(i_it);`
`695`	`688`	`}`
`@@ -699,7 +692,7 @@ void instrumentert::cfg_visitort::visit_cfg_function_call(`
`699`	`692`	`{`
`700`	`693`	`/* normal inlining strategy */`
`701`	`694`	`visit_cfg_function(value_sets, model, no_dependencies, replicate_body,`
`702`		`- fun_id, s, in_pos[i_it]);`
	`695`	`+ fun_id, in_pos[i_it]);`
`703`	`696`	`updated.insert(i_it);`
`704`	`697`	`}`
`705`	`698`
Original file line number	Diff line number	Diff line change
`@@ -26,15 +26,15 @@ class instrumenter_pensievet:public instrumentert`
`26`	`26`	`{`
`27`	`27`	`}`
`28`	`28`
`29`		`- void collect_pairs_naive(namespacet &ns)`
	`29`	`+ void collect_pairs_naive()`
`30`	`30`	`{`
`31`		`- egraph.collect_pairs_naive(ns);`
	`31`	`+ egraph.collect_pairs_naive();`
`32`	`32`	`}`
`33`	`33`
`34`	`34`	`/* collects directly all the pairs in the graph */`
`35`		`- void collect_pairs(namespacet &ns)`
	`35`	`+ void collect_pairs()`
`36`	`36`	`{`
`37`		`- egraph.collect_pairs(ns);`
	`37`	`+ egraph.collect_pairs();`
`38`	`38`	`}`
`39`	`39`	`};`
`40`	`40`
Original file line number	Diff line number	Diff line change
`@@ -22,7 +22,7 @@ Date: 2013`
`22`	`22`	`#define OUTPUT(s, fence, file, line, id, type) \`
`23`	`23`	`s<<fence<<"\|"<<file<<"\|"<<line<<"\|"<<id<<"\|"<<type<<'\n'`
`24`	`24`
`25`		`-void event_grapht::graph_pensieve_explorert::collect_pairs(namespacet &ns)`
	`25`	`+void event_grapht::graph_pensieve_explorert::collect_pairs()`
`26`	`26`	`{`
`27`	`27`	`std::ofstream res;`
`28`	`28`	`res.open("results.txt");`