Otawa  0.10
otawa::dfa Namespace Reference

Namespaces

 hai
 

Classes

class  AbsIntLite
 This class provides a light implementation for abstract interpretation. More...
 
class  AbsIntLiteEx
 
class  AbsIntLiteExtender
 
class  BitSet
 This class implements a set as a bit vector. More...
 
class  FastState
 Fast implementation of abstract domain on the functional state of a microprocessor including the registers and the memory content. More...
 
class  IterativeDFA
 This class provides a generic facility to implement iterative Data Flow Analysis (DFA) as presented in "Aho, Sethi, Ullman, Compilers: Principles, Techniques, and Tools, Addison Wesley 1986". More...
 
class  MemCell
 
class  Predecessor
 This iterator is used to traverse forward a CFG in an iterative DFA analysis. More...
 
class  State
 Represents a value of the data state. More...
 
class  Successor
 This iterator is used to traverse backward a CFG in an iterative DFA analysis. More...
 
class  Value
 
class  XCFGVisitor
 This class implements the visitor concept of XIterativeDFA class and allows applying an analysis on a collection of CFG in a flow-insensitive way. More...
 
class  XIterativeDFA
 The DFAEngine implements an extended Iterative Data Flow Algorithm, that is, it work on graphs with any forms. More...
 

Functions

elm::io::Outputoperator<< (elm::io::Output &output, const BitSet &bits)
 
p::feature INITIAL_STATE_FEATURE ("otawa::dfa::INITIAL_STATE_FEATURE", new Maker< InitialStateBuilder >())
 This feature ensures that the executable and user information have been parsed to make the initial state of the task. More...
 
Identifier< Pair< const
hard::Register *, Value > > 
REG_INIT ("otawa::dfa::REG_INIT")
 This configuration attribute allows to specify an initial value for a register. More...
 
Identifier< MemCellMEM_INIT ("otawa::dfa::MEM_INIT")
 This configuration attribute allows to specify an initial value for a memory cell. More...
 
Identifier< State * > INITIAL_STATE ("otawa::dfa::INITIAL_STATE", 0)
 This attribute provides the initial state of the task. More...
 
Identifier< int > INDEX ("otawa::dfa::I",-1)
 Identifier used for internal use. More...
 

Variables

Identifier< Pair< const
hard::Register *, Value > > 
REG_INIT
 This configuration attribute allows to specify an initial value for a register. More...
 
Identifier< MemCellMEM_INIT
 This configuration attribute allows to specify an initial value for a memory cell. More...
 
p::feature INITIAL_STATE_FEATURE
 This feature ensures that the executable and user information have been parsed to make the initial state of the task. More...
 
Identifier< State * > INITIAL_STATE
 This attribute provides the initial state of the task. More...
 
Identifier< int > INDEX
 Identifier used for internal use. More...
 

Function Documentation

Identifier<int> otawa::dfa::INDEX ( "otawa::dfa::I"  ,
1 
)

Identifier used for internal use.

Identifier<State *> otawa::dfa::INITIAL_STATE ( "otawa::dfa::INITIAL_STATE"  ,
 
)

This attribute provides the initial state of the task.

Hook

Feature

p::feature otawa::dfa::INITIAL_STATE_FEATURE ( "otawa::dfa::INITIAL_STATE_FEATURE"  ,
new Maker< InitialStateBuilder >  () 
)

This feature ensures that the executable and user information have been parsed to make the initial state of the task.

Configuration

Attributes

Identifier<MemCell> otawa::dfa::MEM_INIT ( "otawa::dfa::MEM_INIT"  )

This configuration attribute allows to specify an initial value for a memory cell.

Implictely, it allows also to assign a type to the memory cell.

Feature

elm::io::Output& otawa::dfa::operator<< ( elm::io::Output output,
const BitSet &  bits 
)
inline
Identifier<Pair<const hard::Register *, Value> > otawa::dfa::REG_INIT ( "otawa::dfa::REG_INIT"  )

This configuration attribute allows to specify an initial value for a register.

Feature

Variable Documentation

Identifier<State *> otawa::dfa::INITIAL_STATE("otawa::dfa::INITIAL_STATE", 0)

This attribute provides the initial state of the task.

Hook

Feature

Referenced by otawa::clp::Analysis::processWorkSpace(), and otawa::FlowFactLoader::setup().

p::feature otawa::dfa::INITIAL_STATE_FEATURE("otawa::dfa::INITIAL_STATE_FEATURE", new Maker< InitialStateBuilder >())

This feature ensures that the executable and user information have been parsed to make the initial state of the task.

Configuration

Attributes

Identifier<MemCell> otawa::dfa::MEM_INIT("otawa::dfa::MEM_INIT")

This configuration attribute allows to specify an initial value for a memory cell.

Implictely, it allows also to assign a type to the memory cell.

Feature

Identifier<Pair<const hard::Register *, Value> > otawa::dfa::REG_INIT("otawa::dfa::REG_INIT")

This configuration attribute allows to specify an initial value for a register.

Feature