Handle multi-line macros

make more robust, one more test.

Author: petr-bauch

regression/verilog/assert4/main.v

@@ -0,0 +1,15 @@
+module main();
+`define SIZE 31
+`define plus_binary(a,b) \
+   a+b
+   
+   reg [`SIZE:0] x;
+  wire clk;
+  
+  initial x=1;
+  
+  always @(posedge clk) x<=`plus_binary(x,1);
+
+  always assert property1: x!=10;
+
+endmodule

regression/verilog/assert4/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.v
+--module main --bound 20 --trace
+^EXIT=10$
+^SIGNAL=0$
+^Counterexample:$
+\[main.property.property1\] .* FAILURE$
+--
+^warning: ignoring

src/verilog/verilog_language.cpp

@@ -7,6 +7,7 @@ Author: Daniel Kroening, [email protected]
 \*******************************************************************/
 
 #include <sstream>
+#include <iostream>
 
 #include <util/suffix.h>
 
@@ -40,6 +41,10 @@ bool verilog_languaget::parse(
   if(preprocess(instream, path, str))
     return true;
 
+  std::cerr << "--------------------------------------------------\n";
+  std::cerr << str.str();
+  std::cerr << "\n--------------------------------------------------\n";
+
   verilog_parser.set_file(path);
   verilog_parser.in=&str;
   verilog_parser.set_message_handler(get_message_handler());

src/verilog/verilog_preprocessor.cpp

@@ -496,18 +496,35 @@ void verilog_preprocessort::directive()
       tptr++;
     }
 
+    auto old_tptr = tptr;
+    // maybe skip whitespace between name and paramlist
+    while (*tptr == ' ' || *tptr == '\t' || *tptr == '\n')
+      tptr++;
+
     // is there a parameter list?
     if(*tptr=='(')
     {
+      // we don't expect any extra parentheses inside parameter list
       while (*(++tptr) != ')')
         param_string.push_back(*tptr);
       ++tptr; // get past the closing parenthesis
-    }
+    } else
+      tptr = old_tptr;
 
     // skip whitespace
     while(*tptr==' ' || *tptr=='\t') tptr++;
 
     value=tptr;
+    // handle multi-line macros
+    while (value.back() == '\\') {
+      value.pop_back();
+      files.back().getline(line);
+      tptr = line.c_str();
+      // remove indentation
+      while (*tptr == ' ' || *tptr == '\t')
+        tptr++;
+      value += tptr;
+    }
 
     // remove trailing whitespace