Merge pull request #518 from diffblue/trans-trace-macros

BMC: include macros in trace

Author: kroening

regression/ebmc/traces/verilog1.desc

@@ -0,0 +1,15 @@
+CORE
+verilog1.v
+--bound 9 --numbered-trace
+^\[.*\] .* REFUTED$
+^Counterexample with 10 states:$
+^main\.P@0 = 123$
+^main\.Q@0 = 124$
+^main\.data@0 = 1$
+^main\.P@9 = 123$
+^main\.Q@9 = 124$
+^main\.data@9 = 10$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ebmc/traces/verilog1.v

@@ -0,0 +1,14 @@
+module main(input clk);
+
+  parameter P = 123;
+  parameter Q = P + 1;
+
+  reg [31:0] data;
+  initial data = 1;
+
+  always @(posedge clk)
+    data = data + 1;
+
+  always assert p1: data != 10;
+
+endmodule

src/trans-word-level/trans_trace_word_level.cpp

@@ -58,20 +58,33 @@ trans_tracet compute_trans_trace(
          symbol.type.id()!=ID_module &&
          symbol.type.id()!=ID_module_instance)
       {
-        exprt indexed_symbol_expr(ID_symbol, symbol.type);
-
-        indexed_symbol_expr.set(ID_identifier,
-          timeframe_identifier(t, symbol.name));
-
-        exprt value_expr=decision_procedure.get(indexed_symbol_expr);
-        if(value_expr==indexed_symbol_expr)
-          value_expr=nil_exprt();
-
-        trans_tracet::statet::assignmentt assignment;
-        assignment.rhs.swap(value_expr);
-        assignment.lhs=symbol.symbol_expr();
-      
-        state.assignments.push_back(assignment);
+        if(symbol.is_macro)
+        {
+          if(symbol.value.is_constant())
+          {
+            trans_tracet::statet::assignmentt assignment;
+            assignment.rhs = symbol.value;
+            assignment.lhs = symbol.symbol_expr();
+            state.assignments.push_back(assignment);
+          }
+        }
+        else
+        {
+          exprt indexed_symbol_expr(ID_symbol, symbol.type);
+
+          indexed_symbol_expr.set(
+            ID_identifier, timeframe_identifier(t, symbol.name));
+
+          exprt value_expr = decision_procedure.get(indexed_symbol_expr);
+          if(value_expr == indexed_symbol_expr)
+            value_expr = nil_exprt();
+
+          trans_tracet::statet::assignmentt assignment;
+          assignment.rhs.swap(value_expr);
+          assignment.lhs = symbol.symbol_expr();
+
+          state.assignments.push_back(assignment);
+        }
       }
     }
   }