code_contractst::ptr_field_snapshot_t Struct Reference

Per-field snapshot for pointer-struct-field assigns compliance. More...

#include <contracts.h>

Public Attributes
expr2tc	ptr_sym
	Pointer symbol (e.g. symbol2tc for "ctx").
type2tc	pointee_type
	Resolved struct type pointed to by ptr_sym.
irep_idt	field_name
	Field name not in assigns (e.g. "capacity").
type2tc	field_type
	Type of that field.
expr2tc	snapshot_sym
	Snapshot symbol holding pre-call field value.

Detailed Description

Per-field snapshot for pointer-struct-field assigns compliance.

Captures the pre-call value of a field NOT in the assigns clause so that the post-call assertion can verify it is unchanged.

Member Data Documentation

field_name

irep_idt code_contractst::ptr_field_snapshot_t::field_name

Field name not in assigns (e.g. "capacity").

field_type

type2tc code_contractst::ptr_field_snapshot_t::field_type

Type of that field.

pointee_type

type2tc code_contractst::ptr_field_snapshot_t::pointee_type

Resolved struct type pointed to by ptr_sym.

ptr_sym

expr2tc code_contractst::ptr_field_snapshot_t::ptr_sym

Pointer symbol (e.g. symbol2tc for "ctx").

snapshot_sym

expr2tc code_contractst::ptr_field_snapshot_t::snapshot_sym

Snapshot symbol holding pre-call field value.

---

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

• src/goto-programs/contracts/contracts.h