frame_enforcer.h File Reference

Observational frame-rule enforcement for verification. More...

#include <goto-programs/goto_program.h>
#include <util/symtab/context.h>
#include <irep2/irep2_expr.h>
#include <map>
#include <set>
#include <vector>

Include dependency graph for frame_enforcer.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

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

Enumerations
enum class	frame_modet { ASSUME , ASSERT }
	Enforcement mode: ASSUME constrains search space (loops), ASSERT checks compliance (contracts). More...

Detailed Description

Observational frame-rule enforcement for verification.

This module implements the "Snapshot → Havoc → Assume/Assert(Unchanged == Snapshot)" pattern used in two contexts:

1. Loop invariants (ASSUME mode): Bridges the inductive gap in k-induction by assuming unassigned variables retain pre-havoc values.
2. Function contracts (ASSERT mode): Checks assigns clause compliance by asserting that variables NOT in the assigns set are unchanged after the function call.

Key operations:

1. materialize_snapshots: Capture pre-state before havoc/call
2. enforce_frame_rule: Constrain/check post-state for unassigned variables
3. replace_old_with_snapshots: Support old() references in invariants
4. collect_global_variables: Gather all accessible globals from symbol table

Enumeration Type Documentation

frame_modet

enum class frame_modet

strong

Enforcement mode: ASSUME constrains search space (loops), ASSERT checks compliance (contracts).

Enumerator
ASSUME
ASSERT