Skip to content

Commit da525e7

Browse files
authored
Merge pull request #12 from diffblue/fix/compilation_with_changed_messaget
Adapt print/messaget API, get_error_found
2 parents 3b4b2f2 + 7328b2e commit da525e7

File tree

4 files changed

+13
-8
lines changed

4 files changed

+13
-8
lines changed

src/ebmc/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ SRC = diameter.cpp main.cpp diatest.cpp show_properties.cpp \
99
OBJ+= $(CBMC)/src/util/util$(LIBEXT) \
1010
$(CBMC)/src/langapi/langapi$(LIBEXT) \
1111
$(CBMC)/src/ansi-c/string_constant$(OBJEXT) \
12-
$(CBMC)/src/ansi-c/c_types$(OBJEXT) \
12+
$(CBMC)/src/util/c_types$(OBJEXT) \
1313
$(CBMC)/src/solvers/solvers$(LIBEXT) \
1414
$(CBMC)/src/big-int/big-int$(LIBEXT) \
1515
../trans-netlist/trans-netlist$(LIBEXT) \

src/vcegar/abstractor.cpp

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -572,8 +572,9 @@ void abstractort::calc_abstract_trans_rel(
572572
throw "unexpected result from predabs_sat1.solve()";
573573
}
574574

575-
print(9, "Generated "+
576-
i2string(trans_cube_set.no_insertions())+" cube(s)");
575+
debug() <<"Generated "
576+
<< i2string(trans_cube_set.no_insertions()) << " cube(s)"
577+
<< eom;
577578

578579
if(show_cubes)
579580
std::cout << trans_cube_set;
@@ -693,8 +694,9 @@ void abstractort::calc_abstract_initial_states(
693694
}
694695

695696
// std::cout<<" The abstract transition relation \n";
696-
print(9, "Generated "+
697-
i2string(initial.no_insertions())+" cube(s)\n");
697+
debug() << "Generated " <<
698+
<< i2string(initial.no_insertions()) <, " cube(s)\n"
699+
<< eom;
698700

699701
if(show_cubes)
700702
std::cout << initial;

src/vcegar/modelchecker_smv.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -164,7 +164,7 @@ bool modelchecker_smvt::read_result_cadence_smv(
164164
counterexample);
165165

166166

167-
print(9, "Cadence SMV counterexample sucessfully read");
167+
debug() << "Cadence SMV counterexample sucessfully read" << eom;
168168

169169
return false;
170170
}

src/verilog/verilog_typecheck_expr.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2026,6 +2026,9 @@ bool verilog_typecheck(
20262026
message_handlert &message_handler,
20272027
const namespacet &ns)
20282028
{
2029+
const unsigned errors_before=
2030+
message_handler.get_message_count(messaget::M_ERROR);
2031+
20292032
verilog_typecheck_exprt verilog_typecheck_expr(
20302033
ns, module_identifier, message_handler);
20312034

@@ -2048,6 +2051,6 @@ bool verilog_typecheck(
20482051
{
20492052
verilog_typecheck_expr.error() << e << messaget::eom;
20502053
}
2051-
2052-
return verilog_typecheck_expr.get_error_found();
2054+
2055+
return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
20532056
}

0 commit comments

Comments
 (0)