gcc style error messages for goto-cc

regression/cbmc/Fixedbv8/main.c

@@ -0,0 +1,13 @@
+typedef __CPROVER_fixedbv[64][32] __plant_typet;
+extern __plant_typet A0, A1;
+
+int main(void) {
+  __CPROVER_assume(A0 == (__plant_typet)0.125);
+  __CPROVER_assume(A1 == (__plant_typet)0.015625);
+
+  const __plant_typet XXX1a=A0 * A1;
+  const __plant_typet XXX2a=(__plant_typet)-1 * XXX1a;
+  const __plant_typet XXX2b=-0.001953125;
+  __CPROVER_assert(XXX2a==XXX2b, "");
+  return 0;
+}

regression/cbmc/Fixedbv8/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/goto-cc/armcc_mode.cpp

@@ -59,8 +59,8 @@ int armcc_modet::doit()
   if(cmdline.isset("verbosity"))
     verbosity=unsafe_string2int(cmdline.get_value("verbosity"));
 
-  compiler.ui_message_handler.set_verbosity(verbosity);
-  ui_message_handler.set_verbosity(verbosity);
+  compiler.set_message_handler(get_message_handler());
+  message_handler.set_verbosity(verbosity);
 
   debug() << "ARM mode" << eom;
 

src/goto-cc/armcc_mode.h

@@ -11,25 +11,28 @@ Date: June 2006
 #ifndef CPROVER_GOTO_CC_ARMCC_MODE_H
 #define CPROVER_GOTO_CC_ARMCC_MODE_H
 
+#include <util/cout_message.h>
+
 #include "goto_cc_mode.h"
 #include "armcc_cmdline.h"
 
 class armcc_modet:public goto_cc_modet
 {
 public:
-  virtual int doit();
-  virtual void help_mode();
+  int doit() final;
+  void help_mode() final;
 
   armcc_modet(
     armcc_cmdlinet &_armcc_cmdline,
     const std::string &_base_name):
-    goto_cc_modet(_armcc_cmdline, _base_name),
+    goto_cc_modet(_armcc_cmdline, _base_name, message_handler),
     cmdline(_armcc_cmdline)
   {
   }
 
 protected:
   armcc_cmdlinet &cmdline;
+  gcc_message_handlert message_handler;
 };
 
 #endif // CPROVER_GOTO_CC_ARMCC_MODE_H

src/goto-cc/as_mode.cpp

@@ -79,7 +79,7 @@ as_modet::as_modet(
   goto_cc_cmdlinet &_cmdline,
   const std::string &_base_name,
   bool _produce_hybrid_binary):
-  goto_cc_modet(_cmdline, _base_name),
+  goto_cc_modet(_cmdline, _base_name, message_handler),
   produce_hybrid_binary(_produce_hybrid_binary),
   native_tool_name(assembler_name(cmdline, base_name))
 {
@@ -137,7 +137,7 @@ int as_modet::doit()
   if(cmdline.isset("verbosity"))
     verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
 
-  ui_message_handler.set_verbosity(verbosity);
+  message_handler.set_verbosity(verbosity);
 
   if(act_as_as86)
   {

src/goto-cc/as_mode.h

@@ -11,6 +11,8 @@ Date: July 2016
 #ifndef CPROVER_GOTO_CC_AS_MODE_H
 #define CPROVER_GOTO_CC_AS_MODE_H
 
+#include <util/cout_message.h>
+
 #include "goto_cc_mode.h"
 
 class as_modet:public goto_cc_modet
@@ -25,7 +27,8 @@ class as_modet:public goto_cc_modet
     bool _produce_hybrid_binar);
 
 protected:
-  bool produce_hybrid_binary;
+  gcc_message_handlert message_handler;
+  const bool produce_hybrid_binary;
   const std::string native_tool_name;
 
   int run_as(); // call as with original command line

src/goto-cc/cw_mode.cpp

@@ -59,8 +59,8 @@ int cw_modet::doit()
   if(cmdline.isset("verbosity"))
     verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
 
-  compiler.ui_message_handler.set_verbosity(verbosity);
-  ui_message_handler.set_verbosity(verbosity);
+  compiler.set_message_handler(get_message_handler());
+  message_handler.set_verbosity(verbosity);
 
   debug() << "CodeWarrior mode" << eom;
 

src/goto-cc/cw_mode.h

@@ -11,6 +11,8 @@ Date: June 2006
 #ifndef CPROVER_GOTO_CC_CW_MODE_H
 #define CPROVER_GOTO_CC_CW_MODE_H
 
+#include <util/cout_message.h>
+
 #include "goto_cc_mode.h"
 #include "gcc_cmdline.h"
 
@@ -21,13 +23,14 @@ class cw_modet:public goto_cc_modet
   virtual void help_mode();
 
   cw_modet(gcc_cmdlinet &_gcc_cmdline, const std::string &_base_name):
-    goto_cc_modet(_gcc_cmdline, _base_name),
+    goto_cc_modet(_gcc_cmdline, _base_name, message_handler),
     cmdline(_gcc_cmdline)
   {
   }
 
 protected:
   gcc_cmdlinet &cmdline;
+  console_message_handlert message_handler;
 };
 
 #endif // CPROVER_GOTO_CC_CW_MODE_H

src/goto-cc/gcc_mode.cpp

@@ -121,7 +121,7 @@ gcc_modet::gcc_modet(
   goto_cc_cmdlinet &_cmdline,
   const std::string &_base_name,
   bool _produce_hybrid_binary):
-  goto_cc_modet(_cmdline, _base_name),
+  goto_cc_modet(_cmdline, _base_name, gcc_message_handler),
   produce_hybrid_binary(_produce_hybrid_binary),
   act_as_ld(base_name=="ld" ||
             base_name.find("goto-ld")!=std::string::npos)
@@ -223,7 +223,7 @@ int gcc_modet::doit()
   if(cmdline.isset("verbosity"))
     verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
 
-  ui_message_handler.set_verbosity(verbosity);
+  gcc_message_handler.set_verbosity(verbosity);
 
   if(act_as_ld)
   {
@@ -303,7 +303,7 @@ int gcc_modet::doit()
 
   // determine actions to be undertaken
   compilet compiler(cmdline);
-  compiler.ui_message_handler.set_verbosity(verbosity);
+  compiler.set_message_handler(get_message_handler());
 
   if(act_as_ld)
     compiler.mode=compilet::LINK_LIBRARY;

src/goto-cc/gcc_mode.h

@@ -11,20 +11,24 @@ Date: June 2006
 #ifndef CPROVER_GOTO_CC_GCC_MODE_H
 #define CPROVER_GOTO_CC_GCC_MODE_H
 
+#include <util/cout_message.h>
+
 #include "goto_cc_mode.h"
 
 class gcc_modet:public goto_cc_modet
 {
 public:
-  virtual int doit();
-  virtual void help_mode();
+  int doit() final;
+  void help_mode() final;
 
   gcc_modet(
     goto_cc_cmdlinet &_cmdline,
     const std::string &_base_name,
     bool _produce_hybrid_binary);
 
 protected:
+  gcc_message_handlert gcc_message_handler;
+
   const bool produce_hybrid_binary;
 
   const bool act_as_ld;

src/goto-cc/goto_cc_mode.cpp

@@ -35,11 +35,11 @@ Function: goto_cc_modet::goto_cc_modet
 
 goto_cc_modet::goto_cc_modet(
   goto_cc_cmdlinet &_cmdline,
-  const std::string &_base_name):
-  language_uit(_cmdline, ui_message_handler),
-  ui_message_handler(_cmdline, "goto-cc " CBMC_VERSION),
-  base_name(_base_name),
-  cmdline(_cmdline)
+  const std::string &_base_name,
+  message_handlert &_message_handler):
+  messaget(_message_handler),
+  cmdline(_cmdline),
+  base_name(_base_name)
 {
   register_languages();
 }

src/goto-cc/goto_cc_mode.h

@@ -15,7 +15,7 @@ Date: June 2006
 
 #include "goto_cc_cmdline.h"
 
-class goto_cc_modet:public language_uit
+class goto_cc_modet:public messaget
 {
 public:
   virtual int main(int argc, const char **argv);
@@ -25,15 +25,16 @@ class goto_cc_modet:public language_uit
   virtual void usage_error();
 
   goto_cc_modet(
-    goto_cc_cmdlinet &_cmdline,
-    const std::string &_base_name);
+    goto_cc_cmdlinet &,
+    const std::string &_base_name,
+    message_handlert &);
   ~goto_cc_modet();
 
 protected:
-  ui_message_handlert ui_message_handler;
+  goto_cc_cmdlinet &cmdline;
   const std::string base_name;
+
   void register_languages();
-  goto_cc_cmdlinet &cmdline;
 };
 
 #endif // CPROVER_GOTO_CC_GOTO_CC_MODE_H

src/goto-cc/ms_cl_mode.cpp

@@ -69,8 +69,8 @@ int ms_cl_modet::doit()
   if(cmdline.isset("verbosity"))
     verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
 
-  compiler.ui_message_handler.set_verbosity(verbosity);
-  ui_message_handler.set_verbosity(verbosity);
+  compiler.set_message_handler(get_message_handler());
+  message_handler.set_verbosity(verbosity);
 
   debug() << "Visual Studio mode" << eom;
 

src/goto-cc/ms_cl_mode.h

@@ -11,6 +11,8 @@ Date: June 2006
 #ifndef CPROVER_GOTO_CC_MS_CL_MODE_H
 #define CPROVER_GOTO_CC_MS_CL_MODE_H
 
+#include <util/cout_message.h>
+
 #include "goto_cc_mode.h"
 #include "ms_cl_cmdline.h"
 
@@ -23,13 +25,14 @@ class ms_cl_modet:public goto_cc_modet
   ms_cl_modet(
     ms_cl_cmdlinet &_ms_cl_cmdline,
     const std::string &_base_name):
-    goto_cc_modet(_ms_cl_cmdline, _base_name),
+    goto_cc_modet(_ms_cl_cmdline, _base_name, message_handler),
     cmdline(_ms_cl_cmdline)
   {
   }
 
 protected:
   ms_cl_cmdlinet &cmdline;
+  console_message_handlert message_handler;
 };
 
 #endif // CPROVER_GOTO_CC_MS_CL_MODE_H

src/solvers/flattening/boolbv_mult.cpp

@@ -53,15 +53,15 @@ bvt boolbvt::convert_mult(const exprt &expr)
     std::size_t fraction_bits=
       to_fixedbv_type(expr.type()).get_fraction_bits();
 
-    // do a sign extension by fraction_bits bits
-    bv=bv_utils.sign_extension(bv, bv.size()+fraction_bits);
-
     for(exprt::operandst::const_iterator it=operands.begin()+1;
         it!=operands.end(); it++)
     {
       if(it->type()!=expr.type())
         throw "multiplication with mixed types";
 
+      // do a sign extension by fraction_bits bits
+      bv=bv_utils.sign_extension(bv, bv.size()+fraction_bits);
+
       bvt op=convert_bv(*it);
 
       if(op.size()!=width)
@@ -70,10 +70,10 @@ bvt boolbvt::convert_mult(const exprt &expr)
       op=bv_utils.sign_extension(op, bv.size());
 
       bv=bv_utils.signed_multiplier(bv, op);
-    }
 
-    // cut it down again
-    bv.erase(bv.begin(), bv.begin()+fraction_bits);
+      // cut it down again
+      bv.erase(bv.begin(), bv.begin()+fraction_bits);
+    }
 
     return bv;
   }

src/util/cout_message.cpp

@@ -135,3 +135,68 @@ void console_message_handlert::print(
     std::cerr << message << '\n' << std::flush;
   #endif
 }
+
+/*******************************************************************\
+
+Function: gcc_message_handlert::print
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void gcc_message_handlert::print(
+  unsigned level,
+  const std::string &message,
+  int sequence_number,
+  const source_locationt &location)
+{
+  std::string dest;
+
+  const irep_idt &file=location.get_file();
+  const irep_idt &line=location.get_line();
+  const irep_idt &function=location.get_function();
+
+  if(!function.empty())
+  {
+    if(!file.empty())
+      dest+=id2string(file)+":";
+    if(dest!="") dest+=' ';
+    dest+="In function '"+id2string(function)+"':\n";
+  }
+
+  if(!line.empty())
+  {
+    if(!file.empty())
+      dest+=id2string(file)+":";
+
+    dest+=id2string(line)+":"+id2string(line)+":";
+  }
+
+  dest+=message;
+
+  print(level, dest);
+}
+
+/*******************************************************************\
+
+Function: gcc_message_handlert::print
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void gcc_message_handlert::print(
+  unsigned level,
+  const std::string &message)
+{
+  // gcc appears to send everything to cerr
+  std::cerr << message << '\n' << std::flush;
+}