Skip to content

Commit 6d6fa0a

Browse files
committed
Add documentation to goto_trace_constant_pointer_exprt
1 parent 8c7609e commit 6d6fa0a

File tree

1 file changed

+5
-1
lines changed

1 file changed

+5
-1
lines changed

src/goto-programs/goto_trace.h

+5-1
Original file line numberDiff line numberDiff line change
@@ -293,7 +293,11 @@ void show_goto_trace(
293293
options.set_option("stack-trace", true);
294294

295295
/// Variety of constant expression only used in the context of a GOTO trace, to
296-
/// give both the numeric value and the symbolic value of a pointer.
296+
/// give both the numeric value and the symbolic value of a pointer,
297+
/// e.g. numeric value "0xabcd0004" but symbolic value "&some_object + 4". The
298+
/// numeric value is stored in the `constant_exprt`'s usual value slot (see
299+
/// \ref constant_exprt::get_value) and the symbolic value is accessed using the
300+
/// `symbolic_pointer` method introduced by this class.
297301
class goto_trace_constant_pointer_exprt : public constant_exprt
298302
{
299303
public:

0 commit comments

Comments
 (0)