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.

  • Field Details

    • 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 Details

    • ConditionalBlockImpl

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

  • Method Details

    • 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 List<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 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