CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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);
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
__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:85

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 Rewriting Calls to the __CPROVER_pointer_equals Predicate