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

#include <util/symbol.h>
#include <goto-programs/goto_program.h>

Include dependency graph for memory_predicates.h:

This graph shows which files directly or indirectly include 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.

Classes