cprover
ai_history.h File Reference
#include <memory>
#include <goto-programs/goto_model.h>
#include <util/json.h>
#include <util/xml.h>
+ Include dependency graph for ai_history.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  ai_history_baset
 A history object is an abstraction / representation of the control-flow part of a set of traces. More...
 
struct  ai_history_baset::compare_historyt
 In a number of places we need to work with sets of histories so that these (a) make use of the immutability and sharing and (b) ownership can be transfered if necessary, we use shared pointers rather than references. More...
 
class  ahistoricalt
 The common case of history is to only care about where you are now, not how you got there! Invariants are not checkable due to C++... More...
 
class  call_stack_historyt
 Records the call stack Care must be taken when using this on recursive code; it will need the domain to be capable of limiting the recursion. More...
 
class  call_stack_historyt::call_stack_entryt
 
class  ai_history_factory_baset
 As more detailed histories can get complex (for example, nested loops or deep, mutually recursive call stacks) they often need some user controls or limits. More...
 
class  ai_history_factory_default_constructort< traceT >
 An easy factory implementation for histories that don't need parameters. More...
 
class  call_stack_history_factoryt
 

Detailed Description

Abstract Interpretation history

Definition in file ai_history.h.