frame_enforcert::classified_assignst Struct Reference

Classification of assigns targets into direct, pointer, and struct-field categories. More...

#include <frame_enforcer.h>

Public Attributes
std::vector< expr2tc >	direct_targets
	Non-pointer targets matched structurally.
std::vector< expr2tc >	pointer_targets
	Pointer-typed targets from *ptr pattern.
std::map< irep_idt, std::set< irep_idt > >	struct_field_targets
	Direct struct field targets: maps global struct symbol name to the set of field names explicitly assigned.
std::map< irep_idt, std::set< irep_idt > >	ptr_field_targets
	Pointer-struct-field targets: maps pointer symbol name to the set of field names explicitly assigned through that pointer.
std::map< irep_idt, std::vector< expr2tc > >	array_elem_targets
	Array-element targets: maps an array symbol name to the indices the clause names.

Detailed Description

Classification of assigns targets into direct, pointer, and struct-field categories.

Used to separate structurally-matchable targets from pointer-typed targets that require aliasing disjunctions, and from direct struct field targets that require per-field compliance checking.

Member Data Documentation

array_elem_targets

std::map<irep_idt, std::vector<expr2tc> > frame_enforcert::classified_assignst::array_elem_targets

Array-element targets: maps an array symbol name to the indices the clause names.

Used to assert every other element unchanged instead of the whole array, which any write falsifies. Example: __ESBMC_assigns(global[i]) → array_elem_targets["global"] = {i}

direct_targets

std::vector<expr2tc> frame_enforcert::classified_assignst::direct_targets

Non-pointer targets matched structurally.

pointer_targets

std::vector<expr2tc> frame_enforcert::classified_assignst::pointer_targets

Pointer-typed targets from *ptr pattern.

ptr_field_targets

std::map<irep_idt, std::set<irep_idt> > frame_enforcert::classified_assignst::ptr_field_targets

Pointer-struct-field targets: maps pointer symbol name to the set of field names explicitly assigned through that pointer.

Example: __ESBMC_assigns(ctx->count) → ptr_field_targets["ctx"] = {"count"}

struct_field_targets

std::map<irep_idt, std::set<irep_idt> > frame_enforcert::classified_assignst::struct_field_targets

Direct struct field targets: maps global struct symbol name to the set of field names explicitly assigned.

Used to generate per-field compliance assertions instead of a coarse whole-struct assertion. Example: __ESBMC_assigns(global_pt.x) → struct_field_targets["global_pt"] = {"x"}

---

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

• src/goto-programs/frame_enforcer.h