Merge pull request #6834 from diffblue/pointer-trace

show bit-pattern of pointers in trace

Author: kroening

regression/cbmc/hex_trace/main.c

@@ -3,13 +3,15 @@ int main()
   int a;
   unsigned int b;
   float f;
+  char *p;
 
   a = 0;
   a = -100;
   a = 2147483647;
   b = a * 2;
   a = -2147483647;
   f = 0.1f;
+  p = (char *)123;
 
   __CPROVER_assert(0, "");
 }

regression/cbmc/hex_trace/test.desc

@@ -10,6 +10,7 @@ a=2147483647 \s*\(0x7FFFFFFF\)
 b=4294967294ul? \s*\(0xFFFFFFFE\)
 a=-2147483647 \s*\(0x80000001\)
 f=0\.1f \s*\(0x3DCCCCCD\)
+p=.* \(0x7B\)
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

src/goto-programs/goto_trace.cpp

@@ -242,6 +242,15 @@ std::string trace_numeric_value(
       }
     }
   }
+  else if(expr.id() == ID_annotated_pointer_constant)
+  {
+    const auto &annotated_pointer_constant =
+      to_annotated_pointer_constant_expr(expr);
+    auto width = to_pointer_type(expr.type()).get_width();
+    auto &value = annotated_pointer_constant.get_value();
+    auto c = constant_exprt(value, unsignedbv_typet(width));
+    return numeric_representation(c, ns, options);
+  }
   else if(expr.id()==ID_array)
   {
     std::string result;

src/solvers/smt2/smt2_conv.cpp

@@ -662,7 +662,9 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &type)
     pointer_logict::pointert ptr;
     ptr.object = numeric_cast_v<std::size_t>(v / pow);
     ptr.offset=v%pow;
-    return pointer_logic.pointer_expr(ptr, to_pointer_type(type));
+    return annotated_pointer_constant_exprt(
+      bv_expr.get_value(),
+      pointer_logic.pointer_expr(ptr, to_pointer_type(type)));
   }
   else if(type.id()==ID_struct)
   {