1 files changed, 49 insertions, 0 deletions
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/TransferFunction.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/TransferFunction.java
new file mode 100644
index 0000000000..f4a539398a
--- /dev/null
+++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/TransferFunction.java
@@ -0,0 +1,49 @@
+package org.checkerframework.dataflow.analysis;
+
+/*>>>
+import org.checkerframework.checker.nullness.qual.Nullable;
+*/
+
+import org.checkerframework.dataflow.cfg.UnderlyingAST;
+import org.checkerframework.dataflow.cfg.node.LocalVariableNode;
+import org.checkerframework.dataflow.cfg.node.Node;
+import org.checkerframework.dataflow.cfg.node.NodeVisitor;
+
+import java.util.List;
+
+/**
+ * Interface of a transfer function for the abstract interpretation used for the
+ * flow analysis.
+ *
+ * <p>
+ *
+ * A transfer function consists of the following components:
+ * <ul>
+ * <li>A method {@code initialStore} that determines which initial store should
+ * be used in the org.checkerframework.dataflow analysis.</li>
+ * <li>A function for every {@link Node} type that determines the behavior of
+ * the org.checkerframework.dataflow analysis in that case. This method takes a {@link Node} and an
+ * incoming store, and produces a {@link RegularTransferResult}.</li>
+ * </ul>
+ *
+ * <p>
+ *
+ * <em>Important</em>: The individual transfer functions ( {@code visit*}) are
+ * allowed to use (and modify) the stores contained in the argument passed; the
+ * ownership is transfered from the caller to that function.
+ *
+ * @author Stefan Heule
+ *
+ * @param <S>
+ *            The {@link Store} used to keep track of intermediate results.
+ */
+public interface TransferFunction<A extends AbstractValue<A>, S extends Store<S>>
+        extends NodeVisitor<TransferResult<A, S>, TransferInput<A, S>> {
+
+    /**
+     * @return the initial store to be used by the org.checkerframework.dataflow analysis.
+     *         {@code parameters} is only set if the underlying AST is a method.
+     */
+    S initialStore(UnderlyingAST underlyingAST,
+            /*@Nullable*/ List<LocalVariableNode> parameters);
+}