Merge pull request #5034 from smowton/smowton/cleanup/constant-pointer-expr

Add goto_trace_constant_pointer_exprt

Author: smowton

Diff for: src/goto-programs/goto_trace.h

@@ -292,4 +292,28 @@ void show_goto_trace(
   if(cmdline.isset("stack-trace"))                                             \
     options.set_option("stack-trace", true);
 
+/// Variety of constant expression only used in the context of a GOTO trace, to
+/// give both the numeric value and the symbolic value of a pointer.
+class goto_trace_constant_pointer_exprt : public constant_exprt
+{
+public:
+  const exprt &symbolic_pointer() const
+  {
+    return static_cast<const exprt &>(operands()[0]);
+  }
+};
+
+template <>
+inline bool can_cast_expr<goto_trace_constant_pointer_exprt>(const exprt &base)
+{
+  return can_cast_expr<constant_exprt>(base) && base.operands().size() == 1;
+}
+
+inline const goto_trace_constant_pointer_exprt &
+to_goto_trace_constant_pointer_expr(const exprt &expr)
+{
+  PRECONDITION(can_cast_expr<goto_trace_constant_pointer_exprt>(expr));
+  return static_cast<const goto_trace_constant_pointer_exprt &>(expr);
+}
+
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H