Merge pull request #12 from diffblue/fix/compilation_with_changed_mes…

…saget Adapt print/messaget API, get_error_found
diffblue · Jun 14, 2017 · da525e7 · da525e7
2 parents 3b4b2f2 + 7328b2e
commit da525e7
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 8 deletions.
diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile
@@ -9,7 +9,7 @@ SRC = diameter.cpp main.cpp diatest.cpp show_properties.cpp \
 OBJ+= $(CBMC)/src/util/util$(LIBEXT) \
       $(CBMC)/src/langapi/langapi$(LIBEXT) \
       $(CBMC)/src/ansi-c/string_constant$(OBJEXT) \
-      $(CBMC)/src/ansi-c/c_types$(OBJEXT) \
+      $(CBMC)/src/util/c_types$(OBJEXT) \
       $(CBMC)/src/solvers/solvers$(LIBEXT) \
       $(CBMC)/src/big-int/big-int$(LIBEXT) \
       ../trans-netlist/trans-netlist$(LIBEXT) \

diff --git a/src/vcegar/abstractor.cpp b/src/vcegar/abstractor.cpp
@@ -572,8 +572,9 @@ void abstractort::calc_abstract_trans_rel(
     throw "unexpected result from predabs_sat1.solve()";
   }
 
-  print(9, "Generated "+
-    i2string(trans_cube_set.no_insertions())+" cube(s)");
+  debug() <<"Generated "
+          << i2string(trans_cube_set.no_insertions()) << " cube(s)"
+          << eom;
 
   if(show_cubes)
     std::cout << trans_cube_set;
@@ -693,8 +694,9 @@ void abstractort::calc_abstract_initial_states(
   }
 
   // std::cout<<" The abstract transition relation \n";
-  print(9, "Generated "+
-    i2string(initial.no_insertions())+" cube(s)\n");
+  debug() << "Generated " <<
+          << i2string(initial.no_insertions()) <, " cube(s)\n"
+          << eom;
 
   if(show_cubes)
     std::cout << initial;

diff --git a/src/vcegar/modelchecker_smv.cpp b/src/vcegar/modelchecker_smv.cpp
@@ -164,7 +164,7 @@ bool modelchecker_smvt::read_result_cadence_smv(
           counterexample);
 
 
-        print(9, "Cadence SMV counterexample sucessfully read");
+        debug() << "Cadence SMV counterexample sucessfully read" << eom;
 
         return false;
       }

diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
@@ -2026,6 +2026,9 @@ bool verilog_typecheck(
   message_handlert &message_handler,
   const namespacet &ns)
 {
+  const unsigned errors_before=
+    message_handler.get_message_count(messaget::M_ERROR);
+
   verilog_typecheck_exprt verilog_typecheck_expr(
     ns, module_identifier, message_handler);
 
@@ -2048,6 +2051,6 @@ bool verilog_typecheck(
   {
     verilog_typecheck_expr.error() << e << messaget::eom;
   }
-  
-  return verilog_typecheck_expr.get_error_found();
+
+  return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
 }