frame_enforcert::snapshot_entryt Struct Reference

Snapshot entry: maps an original expression to its snapshot symbol. More...

#include <frame_enforcer.h>

Public Attributes
expr2tc	original_expr
	The variable being snapshotted (e.g., "i").
expr2tc	snapshot_sym
	The snapshot symbol (e.g., "__ESBMC_frame_snap_loop_0_i").

Detailed Description

Snapshot entry: maps an original expression to its snapshot symbol.

Member Data Documentation

original_expr

expr2tc frame_enforcert::snapshot_entryt::original_expr

The variable being snapshotted (e.g., "i").

snapshot_sym

expr2tc frame_enforcert::snapshot_entryt::snapshot_sym

The snapshot symbol (e.g., "__ESBMC_frame_snap_loop_0_i").

---

The documentation for this struct was generated from the following file:

• src/goto-programs/frame_enforcer.h