Back to top Code Contracts Transformation Specification
Let us now consider a function bar
, called directly or indirectly from main
.
Assuming that bar
satisfies a contract d
, we want to replace bar
with an abstraction derived from d
. Checking that bar
actually satisfies d
is the responsibility of the user, and will usually be done using another proof harness.
;
{
}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
We abstract bar
by replacing its instructions with instructions modelling the non-deterministic behavior of the contract d
, following this template:
contract::havoc(contract_write_set);
}
void __CPROVER_contracts_write_set_deallocate_freeable(__CPROVER_contracts_write_set_ptr_t set, __CPROVER_contracts_write_set_ptr_t target)
Non-deterministically call __CPROVER_contracts_free on all elements of set->contract_frees,...
void __CPROVER_contracts_write_set_release(__CPROVER_contracts_write_set_ptr_t set)
Releases resources used by set.
__CPROVER_bool __CPROVER_contracts_write_set_check_assigns_clause_inclusion(__CPROVER_contracts_write_set_ptr_t reference, __CPROVER_contracts_write_set_ptr_t candidate)
Checks the inclusion of the candidate->contract_assigns elements in reference->contract_assigns or re...
void __CPROVER_contracts_write_set_create(__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t contract_assigns_size, __CPROVER_size_t contract_frees_size, __CPROVER_bool assume_requires_ctx, __CPROVER_bool assert_requires_ctx, __CPROVER_bool assume_ensures_ctx, __CPROVER_bool assert_ensures_ctx, __CPROVER_bool allow_allocate, __CPROVER_bool allow_deallocate)
Initialises a __CPROVER_contracts_write_set_t object.
__CPROVER_bool __CPROVER_contracts_write_set_check_frees_clause_inclusion(__CPROVER_contracts_write_set_ptr_t reference, __CPROVER_contracts_write_set_ptr_t candidate)
Checks the inclusion of the candidate->contract_frees elements in reference->contract_frees or refere...
__CPROVER_bool __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty(__CPROVER_contracts_write_set_ptr_t set)
Returns true iff set->deallocated is empty.
Runtime representation of a write set.
After applying this transformation, any function that called the initial bar
now calls the abstraction derived from the contract.