CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
dfcc_pointer_equals.h File Reference

Instruments occurrences of pointer_equals predicates in programs encoding requires and ensures clauses of contracts. More...

+ Include dependency graph for dfcc_pointer_equals.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  dfcc_pointer_equalst
 Rewrites calls to pointer_equals predicates into calls to the library implementation. More...
 

Functions

void rewrite_equal_exprt_to_pointer_equals (exprt &expr)
 Rewrites equal_exprt over pointers into calls to the front-end function __CPROVER_pointer_equals, at the expression level.
 

Detailed Description

Instruments occurrences of pointer_equals predicates in programs encoding requires and ensures clauses of contracts.

Definition in file dfcc_pointer_equals.h.

Function Documentation

◆ rewrite_equal_exprt_to_pointer_equals()

void rewrite_equal_exprt_to_pointer_equals ( exprt expr)

Rewrites equal_exprt over pointers into calls to the front-end function __CPROVER_pointer_equals, at the expression level.

Meant to be Applied before GOTO conversion of function contract clauses, followed by rewrite_calls.

Definition at line 145 of file dfcc_pointer_equals.cpp.