org.checkerframework.dataflow.cfg.block

Class ConditionalBlockImpl

java.lang.Object

org.checkerframework.dataflow.cfg.block.BlockImpl

org.checkerframework.dataflow.cfg.block.ConditionalBlockImpl

All Implemented Interfaces:

Block, ConditionalBlock

public class ConditionalBlockImpl
extends BlockImpl
implements ConditionalBlock

Implementation of a conditional basic block.

Nested Class Summary

Nested classes/interfaces inherited from interface org.checkerframework.dataflow.cfg.block.Block

Block.BlockType

Field Summary

Fields

Modifier and Type	Field and Description
protected Store.FlowRule	elseFlowRule
protected @Nullable BlockImpl	elseSuccessor Successor of the else branch.
protected Store.FlowRule	thenFlowRule The initial values for the rules below say that the THEN store before a conditional block flows to BOTH of the stores of the then successor, while the ELSE store before a conditional block flows to BOTH of the stores of the else successor.
protected @Nullable BlockImpl	thenSuccessor Successor of the then branch.

Fields inherited from class org.checkerframework.dataflow.cfg.block.BlockImpl

id, lastId, predecessors, type

Constructor Summary

Constructors

Constructor and Description
ConditionalBlockImpl() Initialize an empty conditional basic block to be filled with contents and linked to other basic blocks later.

Method Summary

Modifier and Type	Method and Description
Store.FlowRule	getElseFlowRule() Returns the flow rule for information flowing from this block to its else successor.
Block	getElseSuccessor() Returns the entry block of the else branch.
@Nullable Node	getLastNode() Returns the last node of this block, or null if none.
List<Node>	getNodes() Returns the nodes contained within this basic block.
Set<Block>	getSuccessors() Returns the successors of this basic block.
Store.FlowRule	getThenFlowRule() Returns the flow rule for information flowing from this block to its then successor.
Block	getThenSuccessor() Returns the entry block of the then branch.
void	setElseFlowRule(Store.FlowRule rule) Set the flow rule for information flowing from this block to its else successor.
void	setElseSuccessor(BlockImpl b) Set the else branch successor.
void	setThenFlowRule(Store.FlowRule rule) Set the flow rule for information flowing from this block to its then successor.
void	setThenSuccessor(BlockImpl b) Set the then branch successor.
String	toString()

Methods inherited from class org.checkerframework.dataflow.cfg.block.BlockImpl

addPredecessor, getId, getPredecessors, getType, removePredecessor

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface org.checkerframework.dataflow.cfg.block.Block

getId, getPredecessors, getType

Field Detail

thenSuccessor

protected @Nullable BlockImpl thenSuccessor

Successor of the then branch.

elseSuccessor

protected @Nullable BlockImpl elseSuccessor

Successor of the else branch.

thenFlowRule

protected Store.FlowRule thenFlowRule

The initial values for the rules below say that the THEN store before a conditional block flows to BOTH of the stores of the then successor, while the ELSE store before a conditional block flows to BOTH of the stores of the else successor.

elseFlowRule

protected Store.FlowRule elseFlowRule

Constructor Detail

ConditionalBlockImpl

public ConditionalBlockImpl()

Initialize an empty conditional basic block to be filled with contents and linked to other basic blocks later.

Method Detail

setThenSuccessor

public void setThenSuccessor(BlockImpl b)

Set the then branch successor.

setElseSuccessor

public void setElseSuccessor(BlockImpl b)

Set the else branch successor.

getThenSuccessor

public Block getThenSuccessor()

Description copied from interface: ConditionalBlock

Returns the entry block of the then branch.

Specified by:

getThenSuccessor in interface ConditionalBlock

Returns:

the entry block of the then branch

getElseSuccessor

public Block getElseSuccessor()

Description copied from interface: ConditionalBlock

Returns the entry block of the else branch.

Specified by:

getElseSuccessor in interface ConditionalBlock

Returns:

the entry block of the else branch

getSuccessors

public Set<Block> getSuccessors()

Description copied from interface: Block

Returns the successors of this basic block.

Specified by:

getSuccessors in interface Block

Returns:

the successors of this basic block

getThenFlowRule

public Store.FlowRule getThenFlowRule()

Description copied from interface: ConditionalBlock

Returns the flow rule for information flowing from this block to its then successor.

Specified by:

getThenFlowRule in interface ConditionalBlock

Returns:

the flow rule for information flowing from this block to its then successor

getElseFlowRule

public Store.FlowRule getElseFlowRule()

Description copied from interface: ConditionalBlock

Returns the flow rule for information flowing from this block to its else successor.

Specified by:

getElseFlowRule in interface ConditionalBlock

Returns:

the flow rule for information flowing from this block to its else successor

setThenFlowRule

public void setThenFlowRule(Store.FlowRule rule)

Description copied from interface: ConditionalBlock

Set the flow rule for information flowing from this block to its then successor.

Specified by:

setThenFlowRule in interface ConditionalBlock

setElseFlowRule

public void setElseFlowRule(Store.FlowRule rule)

Description copied from interface: ConditionalBlock

Set the flow rule for information flowing from this block to its else successor.

Specified by:

setElseFlowRule in interface ConditionalBlock

getNodes

public List<Node> getNodes()

Returns the nodes contained within this basic block. The list may be empty.

The following invariant holds.

 forall n in getNodes() :: n.getBlock() == this
 

This implementation returns an empty list.

Specified by:

getNodes in interface Block

Returns:

the nodes contained within this basic block

getLastNode

public @Nullable Node getLastNode()

Description copied from interface: Block

Returns the last node of this block, or null if none.

Specified by:

getLastNode in interface Block

Returns:

the last node of this block or null

toString

public String toString()

Overrides:

toString in class Object