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