| package org.checkerframework.dataflow.analysis; |
| |
| /*>>> |
| import org.checkerframework.checker.nullness.qual.Nullable; |
| */ |
| |
| import java.util.List; |
| 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; |
| |
| /** |
| * 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>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}. |
| * </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); |
| } |