Merge pull request #556 from diffblue/cbmc-6

bump CBMC to version 6

Author: kroening

lib/cbmc

@@ -14,9 +14,9 @@ module main(input clk, x, y);
 
   always @(posedge clk)
     casez (cnt1)
-      {10'b0z, 2'b00}:;
-      {10'b0z, 2'b01}:;
-      {10'b0z, 2'b1z}: out=1;
+      10'b0z00:;
+      10'b0z01:;
+      10'b0z1z: out=1;
     endcase
 
   always assert p1: out==0;

regression/verilog/case/case3.v

@@ -4,7 +4,7 @@ module m(input [7:0] i, output reg [31:0] x);
     casex(i)
       8'b1x: x=1;
       8'bxx: x=2;
-      { 'b11, 'bx, 'bx }: x=3;
+      8'b11xx: x=3;
       default: x=4;
     endcase
 

regression/verilog/case/case4.v

@@ -32,7 +32,7 @@ bool smv_languaget::parse(
   const std::string &path,
   message_handlert &message_handler)
 {
-  smv_parsert smv_parser;
+  smv_parsert smv_parser(message_handler);
 
   const std::string main_name=smv_module_symbol("main");
   smv_parser.module=&smv_parser.parse_tree.modules[main_name];
@@ -41,7 +41,6 @@ bool smv_languaget::parse(
 
   smv_parser.set_file(path);
   smv_parser.in=&instream;
-  smv_parser.log.set_message_handler(message_handler);
 
   bool result=smv_parser.parse();
 

src/smvlang/smv_language.cpp

@@ -20,7 +20,8 @@ extern class smv_parsert *smv_parser_ptr;
 class smv_parsert:public parsert
 {
 public:
-  smv_parsert()
+  explicit smv_parsert(message_handlert &message_handler)
+    : parsert(message_handler)
   {
     PRECONDITION(smv_parser_ptr == nullptr);
     smv_parser_ptr = this;

src/smvlang/smv_parser.h

@@ -69,11 +69,10 @@ bool verilog_languaget::parse(
   else
     standard = verilog_standardt::V2005_SMV;
 
-  verilog_parsert verilog_parser(standard);
+  verilog_parsert verilog_parser(standard, message_handler);
 
   verilog_parser.set_file(path);
   verilog_parser.in=&str;
-  verilog_parser.log.set_message_handler(message_handler);
   verilog_parser.grammar=verilog_parsert::LANGUAGE;
 
   verilog_scanner_init();
@@ -297,11 +296,10 @@ bool verilog_languaget::to_expr(
   verilog_standardt standard = verilog_standardt::V2005;
 
   // parsing
-  verilog_parsert verilog_parser(standard);
+  verilog_parsert verilog_parser(standard, message_handler);
 
   verilog_parser.set_file("");
   verilog_parser.in=&i_preprocessed;
-  verilog_parser.log.set_message_handler(message_handler);
   verilog_parser.grammar=verilog_parsert::EXPRESSION;
   verilog_scanner_init();
 

src/verilog/verilog_language.cpp

@@ -34,10 +34,9 @@ bool parse_verilog_file(const std::string &filename, verilog_standardt standard)
   std::ifstream in(widen_if_needed(filename));
   console_message_handlert console_message_handler;
 
-  verilog_parsert verilog_parser(standard);
+  verilog_parsert verilog_parser(standard, console_message_handler);
 
   verilog_parser.set_file(filename);
-  verilog_parser.log.set_message_handler(console_message_handler);
 
   if(filename=="")
     verilog_parser.in=&std::cin;

src/verilog/verilog_parser.cpp

@@ -38,7 +38,10 @@ class verilog_parsert:public parsert
     return yyverilogparse()!=0;
   }
 
-  explicit verilog_parsert(verilog_standardt standard) : parse_tree(standard)
+  explicit verilog_parsert(
+    verilog_standardt standard,
+    message_handlert &message_handler)
+    : parsert(message_handler), parse_tree(standard)
   {
     PRECONDITION(verilog_parser_ptr == nullptr);
     verilog_parser_ptr = this;

src/verilog/verilog_parser.h

@@ -50,13 +50,7 @@ int yyvhdlerror(const char *error_str)
     tmp+='\'';
   }
 
-  source_locationt source_location;
-  source_location.set_column(yyvhdllval.column);
-  source_location.set_line(yyvhdllval.line);
-  source_location.set_file(yyvhdllval.file);
-
-  PARSER.log.error().source_location=source_location;
-  PARSER.log.error() << tmp << messaget::eom;
+  PARSER.parse_error(error_str, yyvhdltext);
 
   return strlen(error_str)+1;
 }

src/vhdl/parser.y

@@ -33,11 +33,10 @@ bool vhdl_languaget::parse(
   const std::string &path,
   message_handlert &message_handler)
 {
-  vhdl_parsert vhdl_parser;
+  vhdl_parsert vhdl_parser(message_handler);
 
   vhdl_parser.set_file(path);
   vhdl_parser.in=&instream;
-  vhdl_parser.log.set_message_handler(message_handler);
   //vhdl_parser.grammar=vhdl_parsert::LANGUAGE;
 
   vhdl_scanner_init();
@@ -270,10 +269,9 @@ bool vhdl_languaget::to_expr(
   std::istringstream i_preprocessed(code);
 
   // parsing
-  vhdl_parsert vhdl_parser;
+  vhdl_parsert vhdl_parser(message_handler);
   vhdl_parser.set_file("");
   vhdl_parser.in=&i_preprocessed;
-  vhdl_parser.log.set_message_handler(message_handler);
   vhdl_parser.grammar=vhdl_parsert::EXPRESSION;
   vhdl_scanner_init();