frame_enforcert Class Reference

#include <frame_enforcer.h>

Classes
struct	snapshot_entryt
	Snapshot entry: maps an original expression to its snapshot symbol. More...
struct	classified_assignst
	Classification of assigns targets into direct, pointer, and struct-field categories. More...

Public Member Functions
	frame_enforcert (contextt &_context)
void	materialize_snapshots (const std::vector< expr2tc > &vars_to_snapshot, goto_programt &dest, const locationt &loc, const std::string &scope_prefix)
	Materialize snapshots for a set of variables.
void	enforce_frame_rule (const std::vector< expr2tc > &explicit_assigns, goto_programt &dest, const locationt &loc, frame_modet mode=frame_modet::ASSUME)
	Enforce frame rule with configurable mode.
expr2tc	replace_old_with_snapshots (const expr2tc &expr) const
	Replace old() references in an expression with snapshot variables.
expr2tc	in_pre_state (const expr2tc &expr) const
	Rewrite expr to denote what it denoted before the havoc or call, by substituting each snapshotted symbol for its snapshot.
void	patch_old_snapshot_assigns (goto_programt &prog) const
	Patch old_snapshot side effects in a GOTO program to use frame snapshots.
const std::vector< snapshot_entryt > &	get_active_snapshots () const
	Get the active snapshots (for debugging/inspection).

Static Public Member Functions
static std::vector< expr2tc >	collect_global_variables (const contextt &context)
	Collect all accessible global variables from the symbol table.
static classified_assignst	classify_assigns_targets (const std::vector< expr2tc > &explicit_assigns)
	Classify assigns targets into direct and pointer categories.

Constructor & Destructor Documentation

frame_enforcert()

frame_enforcert::frame_enforcert

(

contextt &

_context

)

Member Function Documentation

classify_assigns_targets()

frame_enforcert::classified_assignst frame_enforcert::classify_assigns_targets ( const std::vector< expr2tc > & explicit_assigns )

static

Classify assigns targets into direct and pointer categories.

• Pointer-typed symbols (from Clang simplifying &(*ptr) to ptr) → pointer_targets
• Dereference expressions → extract pointer operand → pointer_targets
• Everything else → direct_targets

collect_global_variables()

std::vector< expr2tc > frame_enforcert::collect_global_variables ( const contextt & context )

static

Collect all accessible global variables from the symbol table.

Returns symbol2tc expressions for all static-lifetime lvalue symbols, excluding __ESBMC_* internal symbols, functions, and types.

Parameters

context

Symbol table to scan

Returns

Vector of symbol2tc expressions for global variables

enforce_frame_rule()

void frame_enforcert::enforce_frame_rule	(	const std::vector< expr2tc > &	explicit_assigns,
		goto_programt &	dest,
		const locationt &	loc,
		frame_modet	mode = frame_modet::ASSUME )

Enforce frame rule with configurable mode.

For each snapshotted variable NOT in explicit_assigns, generates either ASSUME(var == snapshot_var) or ASSERT(var == snapshot_var).

ASSUME mode (loops): constrains search space for k-induction ASSERT mode (contracts): checks assigns clause compliance

Parameters

explicit_assigns	Variables explicitly allowed to change
dest	GOTO program to append instructions to
loc	Source location for generated instructions
mode	ASSUME for loops (default), ASSERT for contracts

get_active_snapshots()

const std::vector< snapshot_entryt > & frame_enforcert::get_active_snapshots ( ) const

inline

Get the active snapshots (for debugging/inspection).

in_pre_state()

expr2tc frame_enforcert::in_pre_state

(

const expr2tc &

expr

)

const

Rewrite expr to denote what it denoted before the havoc or call, by substituting each snapshotted symbol for its snapshot.

Unlike replace_old_with_snapshots this does not look for an old() marker: it is for expressions that are implicitly pre-state, such as the index of an assigns target.

materialize_snapshots()

void frame_enforcert::materialize_snapshots	(	const std::vector< expr2tc > &	vars_to_snapshot,
		goto_programt &	dest,
		const locationt &	loc,
		const std::string &	scope_prefix )

Materialize snapshots for a set of variables.

Generates DECL + ASSIGN instructions that capture the current value of each variable into a fresh snapshot symbol. Call this BEFORE havoc/call.

Parameters

vars_to_snapshot	Variables to create snapshots for
dest	GOTO program to append snapshot instructions to
loc	Source location for generated instructions
scope_prefix	Unique prefix for snapshot symbol names (e.g., "loop_0")

patch_old_snapshot_assigns()

void frame_enforcert::patch_old_snapshot_assigns

(

goto_programt &

prog

)

const

Patch old_snapshot side effects in a GOTO program to use frame snapshots.

Scans all ASSIGN instructions in prog for the pattern: return_value$___ESBMC_old_raw$N = old_snapshot(var) where var matches an active snapshot entry. The RHS is replaced with (void*)&snapshot_of_var so that (T)return_value$... naturally dereferences the snapshot value.

Must be called after materialize_snapshots() has populated active_snapshots.

replace_old_with_snapshots()

expr2tc frame_enforcert::replace_old_with_snapshots

(

const expr2tc &

expr

)

const

Replace old() references in an expression with snapshot variables.

Walks the expression tree and replaces any symbol matching a snapshotted variable's original with the corresponding snapshot symbol.

Parameters

expr	Expression potentially containing old() references

Returns

Expression with old() replaced by snapshot symbols

---

The documentation for this class was generated from the following files:

• src/goto-programs/frame_enforcer.h
• src/goto-programs/frame_enforcer.cpp