Stores context information supporting the evaluation of pointer predicates in both assume and assert contexts for all predicates: pointer equals, pointer_in_range_dfcc, pointer_is_fresh, obeys_contract. More...

Collaboration diagram for __CPROVER_contracts_ptr_pred_ctx_t:

Public Attributes
__CPROVER_contracts_car_t	fresh_car

void **	ptr_pred

Detailed Description

Stores context information supporting the evaluation of pointer predicates in both assume and assert contexts for all predicates: pointer equals, pointer_in_range_dfcc, pointer_is_fresh, obeys_contract.

Definition at line 73 of file cprover_contracts.c.

Member Data Documentation

◆ fresh_car

__CPROVER_contracts_car_t __CPROVER_contracts_ptr_pred_ctx_t::fresh_car

Definition at line 75 of file cprover_contracts.c.

◆ ptr_pred

void** __CPROVER_contracts_ptr_pred_ctx_t::ptr_pred

Definition at line 76 of file cprover_contracts.c.

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

/home/runner/work/cbmc/cbmc/src/ansi-c/library/cprover_contracts.c

Public Attributes

Detailed Description

Member Data Documentation

◆ fresh_car

◆ ptr_pred