CBMC
|
Predicates to specify memory footprint in function contracts. More...
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 |
Predicates to specify memory footprint in function contracts.
Definition in file memory_predicates.h.