Skip to content

Commit dda0689

Browse files
tautschnigtautschnig
authored
Merge pull request #2881 from peterschrammel/remove-bv-cbmc
Remove bv_cbmct
2 parents ecb7b6b + e6a752a commit dda0689

15 files changed

+25
-190
lines changed

‎jbmc/src/jbmc/Makefile

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
4141
../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
4242
../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
4343
../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
44-
../$(CPROVER_DIR)/src/cbmc/bv_cbmc$(OBJEXT) \
4544
../$(CPROVER_DIR)/src/cbmc/cbmc_dimacs$(OBJEXT) \
4645
../$(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \
4746
../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \

‎jbmc/unit/Makefile

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,6 @@ java-testing-utils.dir:
6060
BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
6161
$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
6262
$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
63-
$(CPROVER_DIR)/src/cbmc/bv_cbmc$(OBJEXT) \
6463
$(CPROVER_DIR)/src/cbmc/cbmc_dimacs$(OBJEXT) \
6564
$(CPROVER_DIR)/src/cbmc/cbmc_languages$(OBJEXT) \
6665
$(CPROVER_DIR)/src/cbmc/cbmc_parse_options$(OBJEXT) \

‎src/cbmc/Makefile

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
SRC = all_properties.cpp \
22
bmc.cpp \
33
bmc_cover.cpp \
4-
bv_cbmc.cpp \
54
cbmc_dimacs.cpp \
65
cbmc_languages.cpp \
76
cbmc_main.cpp \

‎src/cbmc/all_properties.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,6 @@ Author: Daniel Kroening, [email protected]
2323
#include <goto-programs/xml_goto_trace.h>
2424
#include <goto-programs/json_goto_trace.h>
2525

26-
#include "bv_cbmc.h"
27-
2826
void bmc_all_propertiest::goal_covered(const cover_goalst::goalt &)
2927
{
3028
for(auto &g : goal_map)

‎src/cbmc/bmc.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -525,7 +525,7 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)
525525
{
526526
if(options.get_bool_option("beautify"))
527527
counterexample_beautificationt()(
528-
dynamic_cast<bv_cbmct &>(prop_conv), equation);
528+
dynamic_cast<boolbvt &>(prop_conv), equation);
529529

530530
error_trace();
531531
output_graphml(resultt::UNSAFE);

‎src/cbmc/bmc_cover.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,8 +29,6 @@ Author: Daniel Kroening, [email protected]
2929

3030
#include <langapi/language_util.h>
3131

32-
#include "bv_cbmc.h"
33-
3432
class bmc_covert:
3533
public cover_goalst::observert,
3634
public messaget

‎src/cbmc/bv_cbmc.cpp

Lines changed: 0 additions & 118 deletions
This file was deleted.

‎src/cbmc/bv_cbmc.h

Lines changed: 0 additions & 31 deletions
This file was deleted.

‎src/cbmc/cbmc_dimacs.h

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -12,17 +12,16 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_CBMC_CBMC_DIMACS_H
1313
#define CPROVER_CBMC_CBMC_DIMACS_H
1414

15-
#include "bv_cbmc.h"
15+
#include <solvers/flattening/bv_pointers.h>
1616

17-
class cbmc_dimacst:public bv_cbmct
17+
class cbmc_dimacst : public bv_pointerst
1818
{
1919
public:
2020
cbmc_dimacst(
2121
const namespacet &_ns,
2222
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)
2625
{
2726
}
2827

‎src/cbmc/cbmc_solvers.cpp

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,6 @@ Author: Daniel Kroening, [email protected]
2525
#include <solvers/smt2/smt2_dec.h>
2626
#include <solvers/sat/dimacs_cnf.h>
2727

28-
#include "bv_cbmc.h"
2928
#include "cbmc_dimacs.h"
3029
#include "counterexample_beautification.h"
3130

@@ -72,14 +71,14 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
7271

7372
solver->prop().set_message_handler(get_message_handler());
7473

75-
auto bv_cbmc=util_make_unique<bv_cbmct>(ns, solver->prop());
74+
auto bv_pointers = util_make_unique<bv_pointerst>(ns, solver->prop());
7675

7776
if(options.get_option("arrays-uf")=="never")
78-
bv_cbmc->unbounded_array=bv_cbmct::unbounded_arrayt::U_NONE;
77+
bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;
7978
else if(options.get_option("arrays-uf")=="always")
80-
bv_cbmc->unbounded_array=bv_cbmct::unbounded_arrayt::U_ALL;
79+
bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_ALL;
8180

82-
solver->set_prop_conv(std::move(bv_cbmc));
81+
solver->set_prop_conv(std::move(bv_pointers));
8382

8483
return solver;
8584
}

‎src/cbmc/cbmc_solvers.h

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,8 +26,6 @@ Author: Daniel Kroening, [email protected]
2626
#include <solvers/smt2/smt2_dec.h>
2727
#include <goto-symex/symex_target_equation.h>
2828

29-
#include "bv_cbmc.h"
30-
3129
class cbmc_solverst:public messaget
3230
{
3331
public:

‎src/cbmc/counterexample_beautification.cpp

Lines changed: 13 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -78,20 +78,19 @@ counterexample_beautificationt::get_failed_property(
7878
return equation.SSA_steps.end();
7979
}
8080

81-
void counterexample_beautificationt::operator()(
82-
bv_cbmct &bv_cbmc,
83-
const symex_target_equationt &equation)
81+
void counterexample_beautificationt::
82+
operator()(boolbvt &boolbv, const symex_target_equationt &equation)
8483
{
8584
// find failed property
8685

87-
failed=get_failed_property(bv_cbmc, equation);
86+
failed = get_failed_property(boolbv, equation);
8887

8988
// lock the failed assertion
90-
bv_cbmc.set_to(literal_exprt(failed->cond_literal), false);
89+
boolbv.set_to(literal_exprt(failed->cond_literal), false);
9190

9291
{
93-
bv_cbmc.status() << "Beautifying counterexample (guards)"
94-
<< messaget::eom;
92+
boolbv.status() << "Beautifying counterexample (guards)"
93+
<< messaget::eom;
9594

9695
// compute weights for guards
9796
typedef std::map<literalt, unsigned> guard_countt;
@@ -114,8 +113,8 @@ void counterexample_beautificationt::operator()(
114113
}
115114

116115
// give to propositional minimizer
117-
prop_minimizet prop_minimize(bv_cbmc);
118-
prop_minimize.set_message_handler(bv_cbmc.get_message_handler());
116+
prop_minimizet prop_minimize(boolbv);
117+
prop_minimize.set_message_handler(boolbv.get_message_handler());
119118

120119
for(const auto &g : guard_count)
121120
prop_minimize.objective(g.first, g.second);
@@ -125,17 +124,17 @@ void counterexample_beautificationt::operator()(
125124
}
126125

127126
{
128-
bv_cbmc.status() << "Beautifying counterexample (values)"
129-
<< messaget::eom;
127+
boolbv.status() << "Beautifying counterexample (values)"
128+
<< messaget::eom;
130129

131130
// get symbols we care about
132131
minimization_listt minimization_list;
133132

134-
get_minimization_list(bv_cbmc, equation, minimization_list);
133+
get_minimization_list(boolbv, equation, minimization_list);
135134

136135
// minimize
137-
bv_minimizet bv_minimize(bv_cbmc);
138-
bv_minimize.set_message_handler(bv_cbmc.get_message_handler());
136+
bv_minimizet bv_minimize(boolbv);
137+
bv_minimize.set_message_handler(boolbv.get_message_handler());
139138
bv_minimize(minimization_list);
140139
}
141140
}

‎src/cbmc/counterexample_beautification.h

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -18,18 +18,15 @@ Author: Daniel Kroening, [email protected]
1818

1919
#include <solvers/flattening/bv_minimize.h>
2020

21-
#include "bv_cbmc.h"
22-
2321
class counterexample_beautificationt
2422
{
2523
public:
2624
virtual ~counterexample_beautificationt()
2725
{
2826
}
2927

30-
void operator()(
31-
bv_cbmct &bv_cbmc,
32-
const symex_target_equationt &equation);
28+
void
29+
operator()(boolbvt &boolbv, const symex_target_equationt &equation);
3330

3431
protected:
3532
void get_minimization_list(

‎src/cbmc/fault_localization.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -280,7 +280,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()
280280
{
281281
if(options.get_bool_option("beautify"))
282282
counterexample_beautificationt()(
283-
dynamic_cast<bv_cbmct &>(bmc.prop_conv), bmc.equation);
283+
dynamic_cast<boolbvt &>(bmc.prop_conv), bmc.equation);
284284

285285
bmc.error_trace();
286286
}

‎unit/Makefile

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,6 @@ testing-utils.dir:
6262
BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \
6363
../src/cbmc/bmc$(OBJEXT) \
6464
../src/cbmc/bmc_cover$(OBJEXT) \
65-
../src/cbmc/bv_cbmc$(OBJEXT) \
6665
../src/cbmc/cbmc_dimacs$(OBJEXT) \
6766
../src/cbmc/cbmc_languages$(OBJEXT) \
6867
../src/cbmc/cbmc_parse_options$(OBJEXT) \

0 commit comments

Comments
 (0)