code_contractst::arr_elem_snapshot_t Struct Reference

Snapshot for array element assigns compliance (Phase 2B). More...

#include <contracts.h>

Public Attributes
expr2tc	arr_ptr
	Array pointer symbol (e.g. symbol2tc for "arr").
type2tc	arr_add_type
	Result type of (arr + j) pointer-arithmetic.
type2tc	elem_type
	Element type (pointee of arr_ptr).
std::vector< expr2tc >	declared_indices
	Every index the clause names on this array: the witness assertion must excuse all of them, not just one (#7184).
expr2tc	witness_idx
	Nondet witness index symbol j.
expr2tc	snapshot_sym
	Snapshot symbol holding arr[j] pre-call value.

Detailed Description

Snapshot for array element assigns compliance (Phase 2B).

For __ESBMC_assigns(arr[i], arr[k]), use one nondet witness index j to check that no element arr[j] outside the declared indices was modified.

Member Data Documentation

arr_add_type

type2tc code_contractst::arr_elem_snapshot_t::arr_add_type

Result type of (arr + j) pointer-arithmetic.

arr_ptr

expr2tc code_contractst::arr_elem_snapshot_t::arr_ptr

Array pointer symbol (e.g. symbol2tc for "arr").

declared_indices

std::vector<expr2tc> code_contractst::arr_elem_snapshot_t::declared_indices

Every index the clause names on this array: the witness assertion must excuse all of them, not just one (#7184).

elem_type

type2tc code_contractst::arr_elem_snapshot_t::elem_type

Element type (pointee of arr_ptr).

snapshot_sym

expr2tc code_contractst::arr_elem_snapshot_t::snapshot_sym

Snapshot symbol holding arr[j] pre-call value.

witness_idx

expr2tc code_contractst::arr_elem_snapshot_t::witness_idx

Nondet witness index symbol j.

---

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

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