CBMC
|
Collects all user-defined predicates that call functions is_fresh, pointer_in_range, obeys_contract and lifts them to function taking pointers by reference. More...
Go to the source code of this file.
Classes | |
class | dfcc_lift_memory_predicatest |
Collects all user-defined predicates that call functions is_fresh, pointer_in_range, obeys_contract and lifts them to function taking pointers by reference.
When called in assumption contexts, These user-defined predicates update the pointers using side effect in order to make the assumptions described by the predicate hold. In assertion contexts, they behave like the original user-defined predicate i.e. without side effects.
Definition in file dfcc_lift_memory_predicates.h.