From 6d6fa0a3954f97f21c5d99a6050fccc2381e4253 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 20 Aug 2019 10:02:51 +0100 Subject: [PATCH] Add documentation to `goto_trace_constant_pointer_exprt` --- src/goto-programs/goto_trace.h | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index 09587ffbe48..1d6e63904a5 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -293,7 +293,11 @@ void show_goto_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. +/// give both the numeric value and the symbolic value of a pointer, +/// e.g. numeric value "0xabcd0004" but symbolic value "&some_object + 4". The +/// numeric value is stored in the `constant_exprt`'s usual value slot (see +/// \ref constant_exprt::get_value) and the symbolic value is accessed using the +/// `symbolic_pointer` method introduced by this class. class goto_trace_constant_pointer_exprt : public constant_exprt { public: