Snapshot for pointer-parameter dereference assigns compliance (Phase 2C). More...

#include <contracts.h>

Public Attributes
expr2tc	ptr_sym
	Pointer parameter symbol.
type2tc	pointee_type
	Resolved type pointed to by ptr_sym.
irep_idt	field_name
	Empty for scalars; field name for struct members.
type2tc	value_type
	Type of the snapshotted value.
expr2tc	snapshot_sym
	Snapshot symbol holding the pre-call value.
expr2tc	array_index
	Nil for scalars; nondet witness index for array fields.
type2tc	member_type
	Array-field member type (for indexing); nil otherwise.
expr2tc	alias_exemption
	Nil, or a guard under which this location is an assigns target reached by another name.

Detailed Description

Snapshot for pointer-parameter dereference assigns compliance (Phase 2C).

When a pointer param p is NOT declared in the assigns clause at all, its pointed-to value (*p or p->field for structs) must remain unchanged.

Member Data Documentation

expr2tc code_contractst::ptr_deref_snapshot_t::alias_exemption

Nil, or a guard under which this location is an assigns target reached by another name.

expr2tc code_contractst::ptr_deref_snapshot_t::array_index

Nil for scalars; nondet witness index for array fields.

irep_idt code_contractst::ptr_deref_snapshot_t::field_name

Empty for scalars; field name for struct members.

type2tc code_contractst::ptr_deref_snapshot_t::member_type

Array-field member type (for indexing); nil otherwise.

type2tc code_contractst::ptr_deref_snapshot_t::pointee_type

Resolved type pointed to by ptr_sym.

expr2tc code_contractst::ptr_deref_snapshot_t::ptr_sym

Pointer parameter symbol.

expr2tc code_contractst::ptr_deref_snapshot_t::snapshot_sym

Snapshot symbol holding the pre-call value.

type2tc code_contractst::ptr_deref_snapshot_t::value_type

Type of the snapshotted value.

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