CBMC
|
Instruments occurrences of pointer_equals predicates in programs encoding requires and ensures clauses of contracts. More...
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. | |
Instruments occurrences of pointer_equals predicates in programs encoding requires and ensures clauses of contracts.
Definition in file dfcc_pointer_equals.h.
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.