separate format_rec for codet

Author: Daniel Kroening

src/util/format_expr.cpp

@@ -309,24 +309,27 @@ std::ostream &format_rec(std::ostream &os, const exprt &expr)
               << format(if_expr.true_case()) << " : "
               << format(if_expr.false_case()) << ')';
   }
-  else if(id == ID_code)
-  {
-    const auto &code = to_code(expr);
-    const irep_idt &statement = code.get_statement();
+  else
+    return fallback_format_rec(os, expr);
+}
 
-    if(statement == ID_assign)
-      return os << format(to_code_assign(code).lhs()) << " = "
-                << format(to_code_assign(code).rhs()) << ';';
-    else if(statement == ID_block)
-    {
-      os << '{';
-      for(const auto &s : to_code_block(code).statements())
-        os << ' ' << format(s);
-      return os << " }";
-    }
-    else
-      return fallback_format_rec(os, expr);
+// The below generates a string in a generic syntax
+// that is inspired by C/C++/Java, and is meant for debugging
+// purposes.
+std::ostream &format_rec(std::ostream &os, const codet &code)
+{
+  const irep_idt &statement = code.get_statement();
+
+  if(statement == ID_assign)
+    return os << format(to_code_assign(code).lhs()) << " = "
+              << format(to_code_assign(code).rhs()) << ';';
+  else if(statement == ID_block)
+  {
+    os << '{';
+    for(const auto &s : to_code_block(code).statements())
+      os << ' ' << format(s);
+    return os << " }";
   }
   else
-    return fallback_format_rec(os, expr);
+    return os << statement;
 }

src/util/format_expr.h

@@ -12,8 +12,11 @@ Author: Daniel Kroening, [email protected]
 #include "expr.h"
 #include "format.h"
 
+class codet;
+
 //! Formats an expression in a generic syntax
 //! that is inspired by C/C++/Java, and is meant for debugging
 std::ostream &format_rec(std::ostream &, const exprt &);
+std::ostream &format_rec(std::ostream &, const codet &);
 
 #endif // CPROVER_UTIL_FORMAT_EXPR_H