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: