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.

void *lb,
void **ptr,
void *ub,
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
__CPROVER_bool __CPROVER_pointer_in_range_dfcc(void *lb, void *ptr, void *ub)
Runtime representation of a write set.

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