ai_storage.h File Reference

Abstract Interpretation Storage. More...

#include <util/deprecate.h>
#include <goto-programs/goto_program.h>
#include "ai_domain.h"
#include "ai_history.h"

Include dependency graph for ai_storage.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	ai_storage_baset
	This is the basic interface for storing domains. More...
class	trace_map_storaget
class	location_sensitive_storaget
	The most conventional storage; one domain per location. More...
class	history_sensitive_storaget

Detailed Description

Abstract Interpretation Storage.

An interface for the storage of domains in the abstract interpreter. Conceptually this is a map from history -> domain. However in some cases we may wish to share domains between locations so a simple map interface is not sufficient. Also any domain that has not been previously accessed or stored is automatically bottom. There is a constant interface which returns shared pointers to const domains, allowing these to either be stored domains, or things created on-the-fly. The non-constant interace returns a reference as it can create and initialise the domains as needed.

Definition in file ai_storage.h.