Package 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, org.plumelib.util.UniqueId

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	Description
protected Store.FlowRule	elseFlowRule	The initial value says that the ELSE store before a conditional block flows to BOTH of the stores of the else successor.
protected @Nullable BlockImpl	elseSuccessor	Successor of the else branch.
protected Store.FlowRule	thenFlowRule	The initial value says that the THEN store before a conditional block flows to BOTH of the stores of the then successor.
protected @Nullable BlockImpl	thenSuccessor	Successor of the then branch.

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

predecessors, type

Constructor Summary

Constructors

Constructor	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	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.
java.util.List<Node>	getNodes()	Returns the nodes contained within this basic block.
java.util.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.
java.lang.String	toString()

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

addPredecessor, getPredecessors, getType, getUid, 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

getPredecessors, getType

Methods inherited from interface org.plumelib.util.UniqueId

getClassAndUid, getUid

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 value says that the THEN store before a conditional block flows to BOTH of the stores of the then successor.

elseFlowRule

protected Store.FlowRule elseFlowRule

The initial value says that the ELSE store before a conditional block flows to BOTH of the stores of the else successor.

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 java.util.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

Parameters:

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

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

Parameters:

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

getNodes

public java.util.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 java.lang.String toString()

Overrides:

toString in class java.lang.Object