beautification of ssa_exprt

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4652 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/goto-symex/ssa_expr.cpp

@@ -7,6 +7,7 @@ Author: Daniel Kroening, [email protected]
 \*******************************************************************/
 
 #include <sstream>
+#include <cassert>
 
 #include <util/arith_tools.h>
 
@@ -28,21 +29,22 @@ static void build_ssa_identifier_rec(
   const exprt &expr,
   const irep_idt &l0,
   const irep_idt &l1,
+  const irep_idt &l2,
   std::ostream &os)
 {
   if(expr.id()==ID_member)
   {
     const member_exprt &member=to_member_expr(expr);
 
-    build_ssa_identifier_rec(member.struct_op(), l0, l1, os);
+    build_ssa_identifier_rec(member.struct_op(), l0, l1, l2, os);
 
     os << '.' << member.get_component_name();
   }
   else if(expr.id()==ID_index)
   {
     const index_exprt &index=to_index_expr(expr);
 
-    build_ssa_identifier_rec(index.array(), l0, l1, os);
+    build_ssa_identifier_rec(index.array(), l0, l1, l2, os);
 
     mp_integer idx;
     if(to_integer(to_constant_expr(index.index()), idx))
@@ -59,14 +61,17 @@ static void build_ssa_identifier_rec(
 
     if(!l1.empty())
       os << '@' << l1;
+
+    if(!l2.empty())
+      os << '#' << l2;
   }
   else
     assert(false);
 }
 
 /*******************************************************************\
 
-Function: ssa_exprt::update_identifier
+Function: ssa_exprt::build_identifier
 
   Inputs:
 
@@ -76,18 +81,16 @@ Function: ssa_exprt::update_identifier
 
 \*******************************************************************/
 
-void ssa_exprt::update_identifier()
+irep_idt ssa_exprt::build_identifier(
+  const exprt &expr,
+  const irep_idt &l0,
+  const irep_idt &l1,
+  const irep_idt &l2)
 {
   std::ostringstream oss;
 
-  const irep_idt &l0=get_level_0();
-  const irep_idt &l1=get_level_1();
-  const irep_idt &l2=get_level_2();
+  build_ssa_identifier_rec(expr, l0, l1, l2, oss);
 
-  build_ssa_identifier_rec(get_original_expr(), l0, l1, oss);
-
-  if(!l2.empty())
-    oss << '#' << l2;
-
-  set_identifier(oss.str());
+  return oss.str();
 }
+

src/goto-symex/ssa_expr.h

@@ -102,7 +102,20 @@ class ssa_exprt:public symbol_exprt
     return get(ID_L2);
   }
 
-  void update_identifier();
+  void update_identifier()
+  {
+    const irep_idt &l0=get_level_0();
+    const irep_idt &l1=get_level_1();
+    const irep_idt &l2=get_level_2();
+
+    set_identifier(build_identifier(get_original_expr(), l0, l1, l2));
+  }
+  
+  static irep_idt build_identifier(
+    const exprt &src,
+    const irep_idt &l0,
+    const irep_idt &l1,
+    const irep_idt &l2);
 };
 
 /*! \brief Cast a generic exprt to an \ref ssa_exprt