code_contractst::is_fresh_mapping_t Struct Reference

Structure to store is_fresh mapping information. More...

#include <contracts.h>

Public Attributes
irep_idt	temp_var_name
	Temporary variable name (e.g., return_value$___ESBMC_is_fresh$1).
expr2tc	ptr_expr
	Pointer expression (dereferenced from &ptr).
expr2tc	size_expr
	Extent the contract asked for, in bytes; may be nil.

Detailed Description

Structure to store is_fresh mapping information.

Member Data Documentation

ptr_expr

expr2tc code_contractst::is_fresh_mapping_t::ptr_expr

Pointer expression (dereferenced from &ptr).

size_expr

expr2tc code_contractst::is_fresh_mapping_t::size_expr

Extent the contract asked for, in bytes; may be nil.

temp_var_name

irep_idt code_contractst::is_fresh_mapping_t::temp_var_name

Temporary variable name (e.g., return_value$___ESBMC_is_fresh$1).

---

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

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