#include "contracts.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