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...

#include <util/message.h>
#include <goto-programs/goto_program.h>
#include <map>
#include <set>

Include dependency graph for dfcc_lift_memory_predicates.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	dfcc_lift_memory_predicatest

Detailed Description

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.

Classes

Detailed Description