Merge pull request #3440 from diffblue/smt2_diagnostic_output

smt2_solver: SMT2-specific message output

Author: Daniel Kroening

Diff for: regression/smt2_solver/function-applications/function-application2.desc

@@ -3,5 +3,5 @@ function-application2.smt2
 
 ^EXIT=134$
 ^SIGNAL=0$
-^line 5: type mismatch in function definition: expected `\(_ BitVec 16\)' but got `\(_ BitVec 8\)'$
+^\(error "line 5: type mismatch in function definition: expected `\(_ BitVec 16\)' but got `\(_ BitVec 8\)'"\)$
 --

Diff for: scripts/delete_failing_smt2_solver_tests

@@ -8,10 +8,9 @@ rm Array_operations1/test.desc
 rm BV_Arithmetic6/test.desc
 rm Bitfields1/test.desc
 rm Bitfields3/test.desc
+rm Boolean_Guards1/test.desc
+rm Computed-Goto1/test.desc
 rm Division2/test.desc
-rm Double-to-float-no-simp1/test.desc
-rm Double-to-float-no-simp1-fix1/test.desc
-rm Double-to-float-no-simp1-fix2/test.desc
 rm Empty_struct1/test.desc
 rm Endianness3/test.desc
 rm Endianness4/test.desc
@@ -20,33 +19,24 @@ rm Endianness7/test.desc
 rm Fixedbv3/test.desc
 rm Fixedbv5/test.desc
 rm Fixedbv6/test.desc
-rm Float-Rounding1/test.desc
-rm Float-div1/test.desc
 rm Float-div2/test.desc
 rm Float-div3/test.desc
-rm Float-flags-no-simp1/test.desc
-rm Float-flags-simp1/test.desc
 rm Float-no-simp1/test.desc
 rm Float-no-simp2/test.desc
 rm Float-no-simp3/test.desc
 rm Float-no-simp4/test.desc
 rm Float-no-simp5/test.desc
 rm Float-no-simp6/test.desc
 rm Float-no-simp7/test.desc
-rm Float-no-simp8/test.desc
-rm Float-no-simp9/test.desc
 rm Float-smt2-1/test.desc
-rm Float-to-double1/test.desc
 rm Float-to-double2/test.desc
 rm Float-to-int1/test.desc
 rm Float-to-int2/test.desc
 rm Float-to-int3/test.desc
 rm Float-zero-sum1/test.desc
 rm Float12/test.desc
 rm Float13/test.desc
-rm Float19/test.desc
 rm Float20/test.desc
-rm Float21/test.desc
 rm Float22/test.desc
 rm Float23/test.desc
 rm Float24/test.desc
@@ -61,27 +51,32 @@ rm Function_Pointer3/test.desc
 rm Initialization6/test.desc
 rm Linking4/test.desc
 rm Linking7/test.desc
+rm Local_out_of_scope3/test.desc
 rm Malloc17/test.desc
 rm Malloc18/test.desc
 rm Malloc19/test.desc
-rm Malloc20/test.desc
 rm Malloc21/test.desc
 rm Malloc23/test.desc
 rm Malloc24/test.desc
-rm Memmove1/test.desc
 rm Memory_leak1/test.desc
 rm Memory_leak2/test.desc
+rm Multi_Dimensional_Array1/test.desc
 rm Multi_Dimensional_Array2/test.desc
+rm Multi_Dimensional_Array3/test.desc
 rm Multi_Dimensional_Array4/test.desc
 rm Multi_Dimensional_Array6/test.desc
 rm Multiple_Properties1/test.desc
 rm Overflow_Leftshift1/test.desc
 rm Overflow_Subtraction1/test.desc
+rm Pointer_Arithmetic1/test.desc
 rm Pointer_Arithmetic10/test.desc
 rm Pointer_Arithmetic11/test.desc
 rm Pointer_Arithmetic12/test.desc
 rm Pointer_Arithmetic6/test.desc
+rm Pointer_array3/test.desc
+rm Pointer_array4/test.desc
 rm Pointer_array5/test.desc
+rm Pointer_array6/test.desc
 rm Pointer_byte_extract2/test.desc
 rm Pointer_byte_extract3/test.desc
 rm Pointer_byte_extract4/test.desc
@@ -105,7 +100,7 @@ rm Quantifiers-two-dimension-array/test.desc
 rm Quantifiers-type/test.desc
 rm Quantifiers1/test.desc
 rm Recursion5/test.desc
-rm String6/test.desc
+rm String2/test.desc
 rm Struct_Bytewise1/test.desc
 rm Struct_Bytewise2/test.desc
 rm Struct_Initialization2/test.desc
@@ -140,14 +135,13 @@ rm equality_through_array_of_struct3/test.desc
 rm equality_through_array_of_struct4/test.desc
 rm equality_through_struct_containing_arrays1/test.desc
 rm equality_through_struct_containing_arrays2/test.desc
-rm equality_through_struct_containing_arrays3/test.desc
 rm equality_through_union1/test.desc
 rm equality_through_union2/test.desc
 rm equality_through_union3/test.desc
-rm fgets1/test.desc
 rm full_slice1/test.desc
 rm full_slice2/test.desc
 rm gcc_bswap1/test.desc
+rm gcc_c99-bool-1/test.desc
 rm gcc_statement_expression4/test.desc
 rm gcc_switch_case_range1/test.desc
 rm gcc_switch_case_range2/test.desc
@@ -157,31 +151,27 @@ rm graphml_witness1/test.desc
 rm havoc_object1/test.desc
 rm hex_trace/test.desc
 rm if2/test.desc
-rm inet_endian1/test.desc
-rm int-to-float2/test.desc
 rm integer-assignments1/test.desc
 rm little-endian-array1/test.desc
 rm memory_allocation1/test.desc
+rm memset1/test.desc
 rm memset3/test.desc
 rm mm_io1/test.desc
-rm nested_label1/test.desc
 rm no_nondet_static/test.desc
-rm pipe1/test.desc
+rm null1/test.desc
 rm pointer-function-parameters/test.desc
 rm pointer-function-parameters-2/test.desc
-rm read1/test.desc
-rm realloc1/test.desc
-rm realloc2/test.desc
 rm scanf1/test.desc
 rm simple_assert/test.desc
 rm stack-trace/test.desc
-rm strcat1/test.desc
 rm struct10/test.desc
 rm struct6/test.desc
 rm struct7/test.desc
 rm struct9/test.desc
 rm trace-values/trace-values.desc
 rm trace_address_arithmetic1/test.desc
+rm trace_options_json_extended/extended.desc
+rm trace_options_json_extended/non-extended.desc
 rm trace_show_function_calls/test.desc
 rm uncaught_exceptions_analysis1/test.desc
 rm uniform_array1/test.desc
@@ -192,6 +182,7 @@ rm union7/test.desc
 rm union8/test.desc
 rm union9/test.desc
 rm unsigned___int128/test.desc
+rm variable-access-to-constant-array/test.desc
 rm void_pointer2/test.desc
 rm void_pointer3/test.desc
 rm void_pointer4/test.desc

Diff for: src/solvers/smt2/smt2_solver.cpp

@@ -11,11 +11,11 @@ Author: Daniel Kroening, [email protected]
 
 #include "smt2_parser.h"
 
+#include <util/message.h>
 #include <util/namespace.h>
-#include <util/symbol_table.h>
-#include <util/cout_message.h>
-#include <util/simplify_expr.h>
 #include <util/replace_symbol.h>
+#include <util/simplify_expr.h>
+#include <util/symbol_table.h>
 
 #include <solvers/sat/satcheck.h>
 #include <solvers/flattening/boolbv.h>
@@ -216,12 +216,39 @@ void smt2_solvert::command(const std::string &c)
   }
 }
 
+class smt2_message_handlert : public message_handlert
+{
+public:
+  void print(unsigned level, const std::string &message) override
+  {
+    message_handlert::print(level, message);
+
+    if(level < 4) // errors
+      std::cout << "(error \"" << message << "\")\n";
+    else
+      std::cout << "; " << message << '\n';
+  }
+
+  void print(unsigned level, const xmlt &xml) override
+  {
+  }
+
+  void print(unsigned level, const jsont &json) override
+  {
+  }
+
+  void flush(unsigned) override
+  {
+    std::cout << std::flush;
+  }
+};
+
 int solver(std::istream &in)
 {
   symbol_tablet symbol_table;
   namespacet ns(symbol_table);
 
-  console_message_handlert message_handler;
+  smt2_message_handlert message_handler;
   messaget message(message_handler);
 
   // this is our default verbosity