Merge pull request #2136 from diffblue/unwind_module_cleanout

remove two unused hooks in bmct

Author: tautschnig

src/cbmc/bmc.cpp

@@ -35,11 +35,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "counterexample_beautification.h"
 #include "fault_localization.h"
 
-void bmct::do_unwind_module()
-{
-  // this is a hook for hw-cbmc
-}
-
 /// Hook used by CEGIS to selectively freeze variables
 /// in the SAT solver after the SSA formula is added to the solver.
 /// Freezing variables is necessary to make use of incremental
@@ -118,22 +113,11 @@ void bmct::output_graphml(resultt result)
 
 void bmct::do_conversion()
 {
-  // convert HDL (hook for hw-cbmc)
-  do_unwind_module();
-
   status() << "converting SSA" << eom;
 
   // convert SSA
   equation.convert(prop_conv);
 
-  // the 'extra constraints'
-  if(!bmc_constraints.empty())
-  {
-    status() << "converting constraints" << eom;
-
-    for(const auto &constraint : bmc_constraints)
-      prop_conv.set_to_true(constraint);
-  }
   // hook for cegis to freeze synthesis program vars
   freeze_program_variables();
 }

src/cbmc/bmc.h

@@ -94,9 +94,6 @@ class bmct:public safety_checkert
   safety_checkert::resultt execute(abstract_goto_modelt &);
   virtual ~bmct() { }
 
-  // additional stuff
-  std::list<exprt> bmc_constraints;
-
   void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
 
   // the safety_checkert interface
@@ -185,7 +182,6 @@ class bmct:public safety_checkert
 
   // unwinding
   virtual void setup_unwind();
-  virtual void do_unwind_module();
   void do_conversion();
 
   virtual void freeze_program_variables();