formatter for pointer constants

This adds an expression formatter for pointer-typed constants.

Author: kroening

scripts/expected_doxygen_warnings.txt

@@ -7,8 +7,8 @@ warning: Included by graph for 'invariant.h' not generated, too many nodes (172)
 warning: Included by graph for 'irep.h' not generated, too many nodes (80), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'message.h' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'namespace.h' not generated, too many nodes (88), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (120), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'prefix.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (121), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'prefix.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (67), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (71), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_expr.h' not generated, too many nodes (178), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/util/format_expr.cpp

@@ -17,6 +17,8 @@ Author: Daniel Kroening, [email protected]
 #include "ieee_float.h"
 #include "mathematical_expr.h"
 #include "mp_arith.h"
+#include "pointer_expr.h"
+#include "prefix.h"
 #include "std_code.h"
 #include "string_utils.h"
 
@@ -177,8 +179,30 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
     return os << '"' << escape(id2string(src.get_value())) << '"';
   else if(type == ID_floatbv)
     return os << ieee_floatt(src);
-  else if(type == ID_pointer && src.is_zero())
-    return os << src.get_value();
+  else if(type == ID_pointer)
+  {
+    if(src.is_zero())
+      return os << ID_NULL;
+    else if(has_prefix(id2string(src.get_value()), "INVALID-"))
+    {
+      return os << "INVALID-POINTER";
+    }
+    else if(src.operands().size() == 1)
+    {
+      const auto &unary_expr = to_unary_expr(src);
+      const auto &pointer_type = to_pointer_type(src.type());
+      return os << "pointer(" << format(unary_expr.op()) << ", "
+                << format(pointer_type.subtype()) << ')';
+    }
+    else
+    {
+      const auto &pointer_type = to_pointer_type(src.type());
+      const auto width = pointer_type.get_width();
+      auto int_value = bvrep2integer(src.get_value(), width, false);
+      return os << "pointer(0x" << integer2string(int_value, 16) << ", "
+                << format(pointer_type.subtype()) << ')';
+    }
+  }
   else
     return os << src.pretty();
 }