CBMC
ai_history.h File Reference

Abstract Interpretation history. More...

#include <memory>
#include <util/json.h>
#include <util/xml.h>
#include <goto-programs/goto_program.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  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...
 

Detailed Description

Abstract Interpretation history.

Definition in file ai_history.h.