code_contractst::param_extentt Struct Reference

Byte extent of a harness-allocated pointer parameter. More...

#include <contracts.h>

Public Attributes
expr2tc	bytes
	Byte-extent expression of the allocation.
bool	justified
	True when the backing may be dereferenced.
bool	from_is_fresh = false
	True only when bytes is from is_fresh.

Detailed Description

Byte extent of a harness-allocated pointer parameter.

justified says whether the harness backing is real enough to read through: an __ESBMC_is_fresh size, or the one-element stack backing of a C++ this. It is false for a nondet heap extent, which nothing may dereference. An absent map entry is a third state: the harness never allocated, so the pointer is the real caller's.

from_is_fresh is narrower: true only when bytes came from the contract's own __ESBMC_is_fresh(ptr, bytes) clause. The this entry is justified (real stack storage genuinely backs one element) but NOT from_is_fresh (the contract never stated that extent) – consumers that need the extent to match what the contract actually claims, not just "some real memory happens to be there", must check this instead of justified alone (#7057).

Member Data Documentation

bytes

expr2tc code_contractst::param_extentt::bytes

Byte-extent expression of the allocation.

from_is_fresh

bool code_contractst::param_extentt::from_is_fresh = false

True only when bytes is from is_fresh.

justified

bool code_contractst::param_extentt::justified

True when the backing may be dereferenced.

---

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

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