Initial Data Flow State

This modules supports the specification of the initial state of the data flow. Its classes, properties and feature are able to provide initial values for registers and memories. More...

Classes
class	otawa::dfa::MemCell
class	otawa::dfa::State
class	otawa::dfa::Value

Functions
p::id< State * >	otawa::dfa::INITIAL_STATE ("otawa::dfa::INITIAL_STATE", 0)
	This attribute provides the initial state of the task. More...
p::interfaced_feature< State >	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. More...
p::id< MemCell >	otawa::dfa::MEM_INIT ("otawa::dfa::MEM_INIT")
	This configuration attribute allows to specify an initial value for a memory cell. More...
p::id< 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. More...

Variables
p::id< State * >	otawa::dfa::INITIAL_STATE
	This attribute provides the initial state of the task. More...
p::interfaced_feature< State >	otawa::dfa::INITIAL_STATE_FEATURE
	This feature ensures that the executable and user information have been parsed to make the initial state of the task. More...
p::id< MemCell >	otawa::dfa::MEM_INIT
	This configuration attribute allows to specify an initial value for a memory cell. More...
p::id< Pair< const hard::Register *, Value > >	otawa::dfa::REG_INIT
	This configuration attribute allows to specify an initial value for a register. More...

Detailed Description

This modules supports the specification of the initial state of the data flow. Its classes, properties and feature are able to provide initial values for registers and memories.

For instance, this is useful to specify stack or any other OS-dependant initial value.

Function Documentation

INITIAL_STATE()

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

This attribute provides the initial state of the task.

Hook

• WorkSpace

Feature

• INITIAL_STATE_FEATURE

INITIAL_STATE_FEATURE()

p::interfaced_feature<State> 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

• CONST_MEM
• CONST_SECTION
• MEM_INIT
• REG_INIT

Properties

• INITIAL_STATE

MEM_INIT()

p::id<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

• INITIAL_STATE_FEATURE

REG_INIT()

p::id<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

• INITIAL_STATE_FEATURE

Variable Documentation

INITIAL_STATE

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

This attribute provides the initial state of the task.

Hook

• WorkSpace

Feature

• INITIAL_STATE_FEATURE

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

INITIAL_STATE_FEATURE

p::interfaced_feature<State> 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

• CONST_MEM
• CONST_SECTION
• MEM_INIT
• REG_INIT

Properties

• INITIAL_STATE

MEM_INIT

p::id<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

• INITIAL_STATE_FEATURE

REG_INIT

p::id<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

• INITIAL_STATE_FEATURE