package org.checkerframework.dataflow.cfg.block;

import org.checkerframework.dataflow.analysis.Store.FlowRule;

// Werner believes that a ConditionalBlock has to have exactly one RegularBlock (?) predecessor and
// the last node of that predecessor has to be a node of boolean type. He's not totally sure,
// though.  We should check whether that property holds.

/** Represents a conditional basic block. */
public interface ConditionalBlock extends Block {

  /**
   * Returns the entry block of the then branch.
   *
   * @return the entry block of the then branch
   */
  Block getThenSuccessor();

  /**
   * Returns the entry block of the else branch.
   *
   * @return the entry block of the else branch
   */
  Block getElseSuccessor();

  /**
   * Returns the flow rule for information flowing from this block to its then successor.
   *
   * @return the flow rule for information flowing from this block to its then successor
   */
  FlowRule getThenFlowRule();

  /**
   * Returns the flow rule for information flowing from this block to its else successor.
   *
   * @return the flow rule for information flowing from this block to its else successor
   */
  FlowRule getElseFlowRule();

  /**
   * Set the flow rule for information flowing from this block to its then successor.
   *
   * @param rule the new flow rule for information flowing from this block to its then successor
   */
  void setThenFlowRule(FlowRule rule);

  /**
   * Set the flow rule for information flowing from this block to its else successor.
   *
   * @param rule the new flow rule for information flowing from this block to its else successor
   */
  void setElseFlowRule(FlowRule rule);
}