diff options
Diffstat (limited to 'third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Store.java')
-rw-r--r-- | third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Store.java | 91 |
1 files changed, 0 insertions, 91 deletions
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Store.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Store.java deleted file mode 100644 index 5d714da889..0000000000 --- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Store.java +++ /dev/null @@ -1,91 +0,0 @@ -package org.checkerframework.dataflow.analysis; - -import org.checkerframework.dataflow.cfg.CFGVisualizer; - -/** - * A store is used to keep track of the information that the org.checkerframework.dataflow analysis - * has accumulated at any given point in time. - * - * @author Stefan Heule - * @param <S> the type of the store returned by {@code copy} and that is used in {@code - * leastUpperBound}. Usually it is the implementing class itself, e.g. in {@code T extends - * Store<T>}. - */ -public interface Store<S extends Store<S>> { - - // We maintain a then store and an else store before each basic block. - // When they are identical (by reference equality), they can be treated - // as a regular unconditional store. - // Once we have some information for both the then and else store, we - // create a TransferInput for the block and allow it to be analyzed. - public static enum Kind { - THEN, - ELSE, - BOTH - } - - /** A flow rule describes how stores flow along one edge between basic blocks. */ - public static enum FlowRule { - EACH_TO_EACH, // The normal case, then store flows to the then store - // and else store flows to the else store. - THEN_TO_BOTH, // Then store flows to both then and else of successor. - ELSE_TO_BOTH, // Else store flows to both then and else of successor. - THEN_TO_THEN, // Then store flows to the then of successor. Else store is ignored. - ELSE_TO_ELSE, // Else store flows to the else of successor. Then store is ignored. - } - - /** @return an exact copy of this store. */ - S copy(); - - /** - * Compute the least upper bound of two stores. - * - * <p><em>Important</em>: This method must fulfill the following contract: - * - * <ul> - * <li>Does not change {@code this}. - * <li>Does not change {@code other}. - * <li>Returns a fresh object which is not aliased yet. - * <li>Returns an object of the same (dynamic) type as {@code this}, even if the signature is - * more permissive. - * <li>Is commutative. - * </ul> - */ - S leastUpperBound(S other); - - /** - * Compute an upper bound of two stores that is wider than the least upper bound of the two - * stores. Used to jump to a higher abstraction to allow faster termination of the fixed point - * computations in {@link Analysis}. {@code previous} must be the previous store. - * - * <p>A particular analysis might not require widening and should implement this method by - * calling leastUpperBound. - * - * <p><em>Important</em>: This method must fulfill the following contract: - * - * <ul> - * <li>Does not change {@code this}. - * <li>Does not change {@code previous}. - * <li>Returns a fresh object which is not aliased yet. - * <li>Returns an object of the same (dynamic) type as {@code this}, even if the signature is - * more permissive. - * <li>Is commutative. - * </ul> - * - * @param previous must be the previous store - */ - S widenedUpperBound(S previous); - - /** - * Can the objects {@code a} and {@code b} be aliases? Returns a conservative answer (i.e., - * returns {@code true} if not enough information is available to determine aliasing). - */ - boolean canAlias(FlowExpressions.Receiver a, FlowExpressions.Receiver b); - - /** - * Delegate visualization responsibility to a visualizer. - * - * @param viz the visualizer to visualize this store - */ - void visualize(CFGVisualizer<?, S, ?> viz); -} |