rewrite_union no longer needs a namespace

Author: Daniel Kroening

src/goto-symex/rewrite_union.cpp

@@ -20,76 +20,68 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/c_types.h>
 
-static bool have_to_rewrite_union(
-  const exprt &expr,
-  const namespacet &ns)
+static bool have_to_rewrite_union(const exprt &expr)
 {
   if(expr.id()==ID_member)
   {
     const exprt &op=to_member_expr(expr).struct_op();
-    const typet &op_type=ns.follow(op.type());
 
-    if(op_type.id()==ID_union)
+    if(op.type().id() == ID_union_tag || op.type().id() == ID_union)
       return true;
   }
   else if(expr.id()==ID_union)
     return true;
 
   forall_operands(it, expr)
-    if(have_to_rewrite_union(*it, ns))
+    if(have_to_rewrite_union(*it))
       return true;
 
   return false;
 }
 
 // inside an address of (&x), unions can simply
 // be type casts and don't have to be re-written!
-void rewrite_union_address_of(
-  exprt &expr,
-  const namespacet &ns)
+void rewrite_union_address_of(exprt &expr)
 {
-  if(!have_to_rewrite_union(expr, ns))
+  if(!have_to_rewrite_union(expr))
     return;
 
   if(expr.id()==ID_index)
   {
-    rewrite_union_address_of(to_index_expr(expr).array(), ns);
-    rewrite_union(to_index_expr(expr).index(), ns);
+    rewrite_union_address_of(to_index_expr(expr).array());
+    rewrite_union(to_index_expr(expr).index());
   }
   else if(expr.id()==ID_member)
-    rewrite_union_address_of(to_member_expr(expr).struct_op(), ns);
+    rewrite_union_address_of(to_member_expr(expr).struct_op());
   else if(expr.id()==ID_symbol)
   {
     // done!
   }
   else if(expr.id()==ID_dereference)
-    rewrite_union(to_dereference_expr(expr).pointer(), ns);
+    rewrite_union(to_dereference_expr(expr).pointer());
 }
 
 /// We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into
 /// byte_update(NIL, 0, v)
-void rewrite_union(
-  exprt &expr,
-  const namespacet &ns)
+void rewrite_union(exprt &expr)
 {
   if(expr.id()==ID_address_of)
   {
-    rewrite_union_address_of(to_address_of_expr(expr).object(), ns);
+    rewrite_union_address_of(to_address_of_expr(expr).object());
     return;
   }
 
-  if(!have_to_rewrite_union(expr, ns))
+  if(!have_to_rewrite_union(expr))
     return;
 
   Forall_operands(it, expr)
-    rewrite_union(*it, ns);
+    rewrite_union(*it);
 
   if(expr.id()==ID_member)
   {
     const exprt &op=to_member_expr(expr).struct_op();
-    const typet &op_type=ns.follow(op.type());
 
-    if(op_type.id()==ID_union)
+    if(op.type().id() == ID_union_tag || op.type().id() == ID_union)
     {
       exprt offset=from_integer(0, index_type());
       byte_extract_exprt tmp(byte_extract_id(), op, offset, expr.type());
@@ -107,27 +99,22 @@ void rewrite_union(
   }
 }
 
-void rewrite_union(
-  goto_functionst::goto_functiont &goto_function,
-  const namespacet &ns)
+void rewrite_union(goto_functionst::goto_functiont &goto_function)
 {
   Forall_goto_program_instructions(it, goto_function.body)
   {
-    rewrite_union(it->code, ns);
-    rewrite_union(it->guard, ns);
+    rewrite_union(it->code);
+    rewrite_union(it->guard);
   }
 }
 
-void rewrite_union(
-  goto_functionst &goto_functions,
-  const namespacet &ns)
+void rewrite_union(goto_functionst &goto_functions)
 {
   Forall_goto_functions(it, goto_functions)
-    rewrite_union(it->second, ns);
+    rewrite_union(it->second);
 }
 
 void rewrite_union(goto_modelt &goto_model)
 {
-  namespacet ns(goto_model.symbol_table);
-  rewrite_union(goto_model.goto_functions, ns);
+  rewrite_union(goto_model.goto_functions);
 }

src/goto-symex/rewrite_union.h

@@ -19,17 +19,9 @@ class namespacet;
 class goto_functionst;
 class goto_modelt;
 
-void rewrite_union(
-  exprt &expr,
-  const namespacet &ns);
-
-void rewrite_union(
-  goto_functionst::goto_functiont &goto_function,
-  const namespacet &ns);
-
-void rewrite_union(
-  goto_functionst &goto_functions,
-  const namespacet &ns);
-void rewrite_union(goto_modelt &goto_model);
+void rewrite_union(exprt &);
+void rewrite_union(goto_functionst::goto_functiont &);
+void rewrite_union(goto_functionst &);
+void rewrite_union(goto_modelt &);
 
 #endif // CPROVER_GOTO_SYMEX_REWRITE_UNION_H