cprover
Loading...
Searching...
No Matches
memory_predicates.h File Reference

Predicates to specify memory footprint in function contracts. More...

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

Go to the source code of this file.

Classes

class  is_fresh_baset
class  is_fresh_enforcet
class  is_fresh_replacet
class  find_is_fresh_calls_visitort
 Predicate to be used with the exprt::visit() function. More...
class  functions_in_scope_visitort
 Predicate to be used with the exprt::visit() function. More...
class  function_binding_visitort

Detailed Description

Predicates to specify memory footprint in function contracts.

Definition in file memory_predicates.h.