Merge pull request #245 from diffblue/synth-values-expr

Verilog: Synthesis now uses exprt for propagating constants

Author: tautschnig

src/verilog/verilog_synthesis.cpp

@@ -49,7 +49,7 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
 
     if(v_it!=values.end())
     {
-      exprt c=from_integer(v_it->second, integer_typet());
+      exprt c = v_it->second;
       c.add_source_location()=expr.source_location();
       return c;
     }
@@ -1755,10 +1755,9 @@ void verilog_synthesist::synth_assign(
   // elaborate now?
   if(lhs.type().id() == ID_integer)
   {
-    mp_integer i;
     simplify(rhs, ns);
 
-    if(to_integer_non_constant(rhs, i))
+    if(!rhs.is_constant())
     {
       error().source_location=rhs.source_location();
       error() << "synthesis expects constant on rhs" << eom;
@@ -1771,8 +1770,8 @@ void verilog_synthesist::synth_assign(
       error() << "synthesis expects symbol on lhs" << eom;
       throw 0;
     }
-    
-    values[to_symbol_expr(lhs).get_identifier()]=i;
+
+    values[to_symbol_expr(lhs).get_identifier()] = rhs;
   }
   else
     assignment(lhs, rhs, blocking);

src/verilog/verilog_synthesis_class.h

@@ -291,7 +291,7 @@ class verilog_synthesist:
 
   // This map contains the values of all variables
   // fixed to a constant during synthesis.
-  typedef std::map<irep_idt, mp_integer> valuest;
+  typedef std::map<irep_idt, exprt> valuest;
   valuest values;
 
   unsigned temporary_counter;