Merge pull request #2881 from peterschrammel/remove-bv-cbmc

tautschnig · web-flow · commit dda0689eb0e9 · 2018-09-03T16:11:39.000+01:00
Remove bv_cbmct
diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile
@@ -41,7 +41,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/cbmc/bv_cbmc$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/cbmc_dimacs$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile
@@ -60,7 +60,6 @@ java-testing-utils.dir:
 BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
-          $(CPROVER_DIR)/src/cbmc/bv_cbmc$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/cbmc_dimacs$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/cbmc_languages$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/cbmc_parse_options$(OBJEXT) \
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
@@ -1,7 +1,6 @@
 SRC = all_properties.cpp \
       bmc.cpp \
       bmc_cover.cpp \
-      bv_cbmc.cpp \
       cbmc_dimacs.cpp \
       cbmc_languages.cpp \
       cbmc_main.cpp \
diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp
@@ -23,8 +23,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/xml_goto_trace.h>
 #include <goto-programs/json_goto_trace.h>
 
-#include "bv_cbmc.h"
-
 void bmc_all_propertiest::goal_covered(const cover_goalst::goalt &)
 {
   for(auto &g : goal_map)
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
@@ -525,7 +525,7 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)
     {
       if(options.get_bool_option("beautify"))
         counterexample_beautificationt()(
-          dynamic_cast<bv_cbmct &>(prop_conv), equation);
+          dynamic_cast<boolbvt &>(prop_conv), equation);
 
       error_trace();
       output_graphml(resultt::UNSAFE);
diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp
@@ -29,8 +29,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/language_util.h>
 
-#include "bv_cbmc.h"
-
 class bmc_covert:
   public cover_goalst::observert,
   public messaget
diff --git a/src/cbmc/bv_cbmc.cpp b/src/cbmc/bv_cbmc.cpp
diff --git a/src/cbmc/bv_cbmc.h b/src/cbmc/bv_cbmc.h
diff --git a/src/cbmc/cbmc_dimacs.h b/src/cbmc/cbmc_dimacs.h
@@ -12,17 +12,16 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_CBMC_CBMC_DIMACS_H
 #define CPROVER_CBMC_CBMC_DIMACS_H
 
-#include "bv_cbmc.h"
+#include <solvers/flattening/bv_pointers.h>
 
-class cbmc_dimacst:public bv_cbmct
+class cbmc_dimacst : public bv_pointerst
 {
 public:
   cbmc_dimacst(
     const namespacet &_ns,
     propt &_prop,
-    const std::string &_filename):
-    bv_cbmct(_ns, _prop),
-    filename(_filename)
+    const std::string &_filename)
+    : bv_pointerst(_ns, _prop), filename(_filename)
   {
   }
 
diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp
@@ -25,7 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <solvers/smt2/smt2_dec.h>
 #include <solvers/sat/dimacs_cnf.h>
 
-#include "bv_cbmc.h"
 #include "cbmc_dimacs.h"
 #include "counterexample_beautification.h"
 
@@ -72,14 +71,14 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
 
   solver->prop().set_message_handler(get_message_handler());
 
-  auto bv_cbmc=util_make_unique<bv_cbmct>(ns, solver->prop());
+  auto bv_pointers = util_make_unique<bv_pointerst>(ns, solver->prop());
 
   if(options.get_option("arrays-uf")=="never")
-    bv_cbmc->unbounded_array=bv_cbmct::unbounded_arrayt::U_NONE;
+    bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;
   else if(options.get_option("arrays-uf")=="always")
-    bv_cbmc->unbounded_array=bv_cbmct::unbounded_arrayt::U_ALL;
+    bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_ALL;
 
-  solver->set_prop_conv(std::move(bv_cbmc));
+  solver->set_prop_conv(std::move(bv_pointers));
 
   return solver;
 }
diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h
@@ -26,8 +26,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <solvers/smt2/smt2_dec.h>
 #include <goto-symex/symex_target_equation.h>
 
-#include "bv_cbmc.h"
-
 class cbmc_solverst:public messaget
 {
 public:
diff --git a/src/cbmc/counterexample_beautification.cpp b/src/cbmc/counterexample_beautification.cpp
@@ -78,20 +78,19 @@ counterexample_beautificationt::get_failed_property(
   return equation.SSA_steps.end();
 }
 
-void counterexample_beautificationt::operator()(
-  bv_cbmct &bv_cbmc,
-  const symex_target_equationt &equation)
+void counterexample_beautificationt::
+operator()(boolbvt &boolbv, const symex_target_equationt &equation)
 {
   // find failed property
 
-  failed=get_failed_property(bv_cbmc, equation);
+  failed = get_failed_property(boolbv, equation);
 
   // lock the failed assertion
-  bv_cbmc.set_to(literal_exprt(failed->cond_literal), false);
+  boolbv.set_to(literal_exprt(failed->cond_literal), false);
 
   {
-    bv_cbmc.status() << "Beautifying counterexample (guards)"
-                     << messaget::eom;
+    boolbv.status() << "Beautifying counterexample (guards)"
+                    << messaget::eom;
 
     // compute weights for guards
     typedef std::map<literalt, unsigned> guard_countt;
@@ -114,8 +113,8 @@ void counterexample_beautificationt::operator()(
     }
 
     // give to propositional minimizer
-    prop_minimizet prop_minimize(bv_cbmc);
-    prop_minimize.set_message_handler(bv_cbmc.get_message_handler());
+    prop_minimizet prop_minimize(boolbv);
+    prop_minimize.set_message_handler(boolbv.get_message_handler());
 
     for(const auto &g : guard_count)
       prop_minimize.objective(g.first, g.second);
@@ -125,17 +124,17 @@ void counterexample_beautificationt::operator()(
   }
 
   {
-    bv_cbmc.status() << "Beautifying counterexample (values)"
-                     << messaget::eom;
+    boolbv.status() << "Beautifying counterexample (values)"
+                    << messaget::eom;
 
     // get symbols we care about
     minimization_listt minimization_list;
 
-    get_minimization_list(bv_cbmc, equation, minimization_list);
+    get_minimization_list(boolbv, equation, minimization_list);
 
     // minimize
-    bv_minimizet bv_minimize(bv_cbmc);
-    bv_minimize.set_message_handler(bv_cbmc.get_message_handler());
+    bv_minimizet bv_minimize(boolbv);
+    bv_minimize.set_message_handler(boolbv.get_message_handler());
     bv_minimize(minimization_list);
   }
 }
diff --git a/src/cbmc/counterexample_beautification.h b/src/cbmc/counterexample_beautification.h
@@ -18,18 +18,15 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <solvers/flattening/bv_minimize.h>
 
-#include "bv_cbmc.h"
-
 class counterexample_beautificationt
 {
 public:
   virtual ~counterexample_beautificationt()
   {
   }
 
-  void operator()(
-    bv_cbmct &bv_cbmc,
-    const symex_target_equationt &equation);
+  void
+  operator()(boolbvt &boolbv, const symex_target_equationt &equation);
 
 protected:
   void get_minimization_list(
diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp
@@ -280,7 +280,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()
     {
       if(options.get_bool_option("beautify"))
         counterexample_beautificationt()(
-          dynamic_cast<bv_cbmct &>(bmc.prop_conv), bmc.equation);
+          dynamic_cast<boolbvt &>(bmc.prop_conv), bmc.equation);
 
       bmc.error_trace();
     }
diff --git a/unit/Makefile b/unit/Makefile
@@ -62,7 +62,6 @@ testing-utils.dir:
 BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \
           ../src/cbmc/bmc$(OBJEXT) \
           ../src/cbmc/bmc_cover$(OBJEXT) \
-          ../src/cbmc/bv_cbmc$(OBJEXT) \
           ../src/cbmc/cbmc_dimacs$(OBJEXT) \
           ../src/cbmc/cbmc_languages$(OBJEXT) \
           ../src/cbmc/cbmc_parse_options$(OBJEXT) \

Original file line number	Diff line number	Diff line change
`@@ -23,8 +23,6 @@ Author: Daniel Kroening, [email protected]`
`23`	`23`	`#include <goto-programs/xml_goto_trace.h>`
`24`	`24`	`#include <goto-programs/json_goto_trace.h>`
`25`	`25`
`26`		`-#include "bv_cbmc.h"`
`27`		`-`
`28`	`26`	`void bmc_all_propertiest::goal_covered(const cover_goalst::goalt &)`
`29`	`27`	`{`
`30`	`28`	`for(auto &g : goal_map)`
Original file line number	Diff line number	Diff line change
`@@ -525,7 +525,7 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)`
`525`	`525`	`{`
`526`	`526`	`if(options.get_bool_option("beautify"))`
`527`	`527`	`counterexample_beautificationt()(`
`528`		`- dynamic_cast<bv_cbmct &>(prop_conv), equation);`
	`528`	`+ dynamic_cast<boolbvt &>(prop_conv), equation);`
`529`	`529`
`530`	`530`	`error_trace();`
`531`	`531`	`output_graphml(resultt::UNSAFE);`
Original file line number	Diff line number	Diff line change
`@@ -12,17 +12,16 @@ Author: Daniel Kroening, [email protected]`
`12`	`12`	`#ifndef CPROVER_CBMC_CBMC_DIMACS_H`
`13`	`13`	`#define CPROVER_CBMC_CBMC_DIMACS_H`
`14`	`14`
`15`		`-#include "bv_cbmc.h"`
	`15`	`+#include <solvers/flattening/bv_pointers.h>`
`16`	`16`
`17`		`-class cbmc_dimacst:public bv_cbmct`
	`17`	`+class cbmc_dimacst : public bv_pointerst`
`18`	`18`	`{`
`19`	`19`	`public:`
`20`	`20`	`cbmc_dimacst(`
`21`	`21`	`const namespacet &_ns,`
`22`	`22`	`propt &_prop,`
`23`		`- const std::string &_filename):`
`24`		`- bv_cbmct(_ns, _prop),`
`25`		`- filename(_filename)`
	`23`	`+ const std::string &_filename)`
	`24`	`+ : bv_pointerst(_ns, _prop), filename(_filename)`
`26`	`25`	`{`
`27`	`26`	`}`
`28`	`27`