| package org.checkerframework.dataflow.cfg.block; |
| |
| import java.util.List; |
| import org.checkerframework.dataflow.cfg.node.Node; |
| |
| /** |
| * A regular basic block that contains a sequence of {@link Node}s. |
| * |
| * <p>The following invariant holds. |
| * |
| * <pre> |
| * forall n in getContents() :: n.getBlock() == this |
| * </pre> |
| * |
| * @author Stefan Heule |
| */ |
| public interface RegularBlock extends SingleSuccessorBlock { |
| |
| /** @return the unmodifiable sequence of {@link Node}s. */ |
| List<Node> getContents(); |
| |
| /** @return the regular successor block */ |
| Block getRegularSuccessor(); |
| |
| /** Is this block empty (i.e., does it not contain any contents). */ |
| boolean isEmpty(); |
| } |