Merge pull request #3680 from tautschnig/vs-shadow-cbmc

Avoid shadowing in directory cbmc/ [blocks: #2310]

Author: Daniel Kroening

src/cbmc/all_properties.cpp

@@ -293,11 +293,10 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
   }
 }
 
-safety_checkert::resultt bmct::all_properties(
-  const goto_functionst &goto_functions,
-  prop_convt &solver)
+safety_checkert::resultt
+bmct::all_properties(const goto_functionst &goto_functions)
 {
-  bmc_all_propertiest bmc_all_properties(goto_functions, solver, *this);
+  bmc_all_propertiest bmc_all_properties(goto_functions, prop_conv, *this);
   bmc_all_properties.set_message_handler(get_message_handler());
   return bmc_all_properties();
 }

src/cbmc/bmc.cpp

@@ -126,8 +126,7 @@ void bmct::do_conversion()
   freeze_program_variables();
 }
 
-decision_proceduret::resultt
-bmct::run_decision_procedure(prop_convt &prop_conv)
+decision_proceduret::resultt bmct::run_decision_procedure()
 {
   status() << "Passing problem to "
            << prop_conv.decision_procedure_text() << eom;
@@ -343,7 +342,7 @@ safety_checkert::resultt bmct::execute(
     }
 
     if(!options.is_set("paths") || symex.path_segment_vccs > 0)
-      return decide(goto_functions, prop_conv);
+      return decide(goto_functions);
 
     return safety_checkert::resultt::PAUSED;
   }
@@ -426,16 +425,14 @@ safety_checkert::resultt bmct::run(
   return execute(goto_model);
 }
 
-safety_checkert::resultt bmct::decide(
-  const goto_functionst &goto_functions,
-  prop_convt &prop_conv)
+safety_checkert::resultt bmct::decide(const goto_functionst &goto_functions)
 {
   prop_conv.set_message_handler(get_message_handler());
 
   if(options.get_bool_option("stop-on-fail"))
-    return stop_on_fail(prop_conv);
+    return stop_on_fail();
   else
-    return all_properties(goto_functions, prop_conv);
+    return all_properties(goto_functions);
 }
 
 void bmct::show()
@@ -451,9 +448,9 @@ void bmct::show()
   }
 }
 
-safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)
+safety_checkert::resultt bmct::stop_on_fail()
 {
-  switch(run_decision_procedure(prop_conv))
+  switch(run_decision_procedure())
   {
   case decision_proceduret::resultt::D_UNSATISFIABLE:
     report_success();
@@ -643,7 +640,7 @@ void bmct::perform_symbolic_execution(
 
   if(options.get_bool_option("validate-ssa-equation"))
   {
-    symex.validate(ns, validation_modet::INVARIANT);
+    symex.validate(validation_modet::INVARIANT);
   }
 
   INVARIANT(

src/cbmc/bmc.h

@@ -177,12 +177,9 @@ class bmct:public safety_checkert
   // use gui format
   ui_message_handlert &ui_message_handler;
 
-  virtual decision_proceduret::resultt
-    run_decision_procedure(prop_convt &prop_conv);
+  virtual decision_proceduret::resultt run_decision_procedure();
 
-  virtual resultt decide(
-    const goto_functionst &,
-    prop_convt &);
+  virtual resultt decide(const goto_functionst &);
 
   void do_conversion();
 
@@ -193,10 +190,8 @@ class bmct:public safety_checkert
     return trace_optionst(options);
   }
 
-  virtual resultt all_properties(
-    const goto_functionst &goto_functions,
-    prop_convt &solver);
-  virtual resultt stop_on_fail(prop_convt &solver);
+  virtual resultt all_properties(const goto_functionst &goto_functions);
+  virtual resultt stop_on_fail();
   virtual void report_success();
   virtual void report_failure();
 

src/cbmc/symex_coverage.cpp

@@ -91,7 +91,6 @@ class goto_program_coverage_recordt:public coverage_recordt
 
   void compute_coverage_lines(
     const goto_programt &goto_program,
-    const irep_idt &file_name,
     const symex_coveraget::coveraget &coverage,
     coverage_lines_mapt &dest);
 };
@@ -155,7 +154,6 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
   coverage_lines_mapt coverage_lines_map;
   compute_coverage_lines(
     gf_it->second.body,
-    file_name,
     coverage,
     coverage_lines_map);
 
@@ -220,7 +218,6 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
 
 void goto_program_coverage_recordt::compute_coverage_lines(
     const goto_programt &goto_program,
-    const irep_idt &file_name,
     const symex_coveraget::coveraget &coverage,
     coverage_lines_mapt &dest)
 {

src/goto-symex/goto_symex.h

@@ -468,7 +468,7 @@ class goto_symext
     return _remaining_vccs;
   }
 
-  void validate(const namespacet &ns, const validation_modet vm) const
+  void validate(const validation_modet vm) const
   {
     target.validate(ns, vm);
   }