ai.h File Reference

Abstract Interpretation. More...

#include <iosfwd>
#include <memory>
#include <util/deprecate.h>
#include <util/json.h>
#include <util/message.h>
#include <util/xml.h>
#include <goto-programs/goto_model.h>
#include "ai_domain.h"
#include "ai_history.h"
#include "ai_storage.h"
#include "is_threaded.h"

Include dependency graph for ai.h:

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

Go to the source code of this file.

Classes
class	ai_baset
	This is the basic interface of the abstract interpreter with default implementations of the core functionality. More...
class	ai_recursive_interproceduralt
class	ait< domainT >
	ait supplies three of the four components needed: an abstract interpreter (in this case handling function calls via recursion), a history factory (using the simplest possible history objects) and storage (one domain per location). More...
class	concurrency_aware_ait< domainT >
	Base class for concurrency-aware abstract interpretation. More...

Detailed Description

Abstract Interpretation.

This is the core of the abstract interpretation framework. To run an analysis you need four components:

1. An abstract interpreter, derived from ai_baset. This performs that actual analysis. There are a number of alternative to choose from, primarily giving different ways of handling function calls / interprocedural analysis. More information is given in this file.
2. A history factory, derived from ai_history_factory_baset. This generates history objects (derived from ai_history_baset) which control the number of steps that the analysis performs. These can be simple, just tracking location, or they can be complex, tracking location, function calls, branches (forwards and backwards), even threading. See ai_history.h for more information.
3. A domain factory, derived from ai_domain_factory_baset. This generates domain objects (derived from ai_domain_baset) which represent the sets of possible valuations that the variables can take at a given point (given history). These can be very simple, just tracking whether a location is reachable or not, or they can be very sophisticated tracking relations between variables, pointers, etc. See ai_domain.h for more information.
4. A storage object, derived from ai_storage_baset. This stores the history and domain objects and manages the link. The simplest case is to store one domain per history (see history_sensitive_storaget). However this can require a large amount of memory being used, so there are options to share / merge domains between different histories, reducing precision in return for better performance.

Definition in file ai.h.