CBMC
Rewriting Calls to the __CPROVER_pointer_in_range_dfcc Predicate

Back to top Code Contracts Transformation Specification

In goto programs encoding pre or post conditions (generated from the contract clauses) and in all user-defined functions, we simply replace calls to __CPROVER_pointer_in_range_dfcc with calls to the library implementation.

__CPROVER_pointer_in_range_dfcc(
void *lb,
void **ptr,
void *ub,
__CPROVER_contracts_write_set_ptr_t write_set);
__CPROVER_pointer_in_range_dfcc
__CPROVER_bool __CPROVER_pointer_in_range_dfcc(void *lb, void *ptr, void *ub)
__CPROVER_contracts_write_set_t
Runtime representation of a write set.
Definition: cprover_contracts.c:72

This function implements the __CPROVER_pointer_in_range_dfcc behaviour in all possible contexts (contract checking vs replacement, requires vs ensures clause context, as described by the flags carried by the write set parameter).

Prev Next
Code Contracts Developer Documentation Function Contracts Reminder