CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Rewriting Calls to the __CPROVER_pointer_equals 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_equals with calls to the library implementation.

__CPROVER_contracts_pointer_equals(
void **ptr1,
void *ptr2,
__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_contracts_pointer_equals
__CPROVER_bool __CPROVER_contracts_pointer_equals(void **ptr1, void *ptr2, __CPROVER_bool may_fail, __CPROVER_contracts_write_set_ptr_t write_set)
Implementation of the pointer_equals front-end predicate.
Definition cprover_contracts.c:1210
__CPROVER_contracts_write_set_t
Runtime representation of a write set.
Definition cprover_contracts.c:85

This function implements the __CPROVER_pointer_equals 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