org.checkerframework.checker.lock

Class LockAnalysis

java.lang.Object

org.checkerframework.dataflow.analysis.AbstractAnalysis<V,S,T>

org.checkerframework.dataflow.analysis.ForwardAnalysisImpl<V,S,T>

org.checkerframework.framework.flow.CFAbstractAnalysis<CFValue,LockStore,LockTransfer>

org.checkerframework.checker.lock.LockAnalysis

All Implemented Interfaces:

Analysis<CFValue,LockStore,LockTransfer>, ForwardAnalysis<CFValue,LockStore,LockTransfer>

public class LockAnalysis
extends CFAbstractAnalysis<CFValue,LockStore,LockTransfer>

The analysis class for the lock type system.

This class extends CFAbstractAnalysis so that LockStore is used rather than CFStore.

Nested Class Summary

Nested classes/interfaces inherited from class org.checkerframework.dataflow.analysis.AbstractAnalysis

AbstractAnalysis.Worklist

Nested classes/interfaces inherited from interface org.checkerframework.dataflow.analysis.Analysis

Analysis.BeforeOrAfter, Analysis.Direction

Field Summary

Fields inherited from class org.checkerframework.framework.flow.CFAbstractAnalysis

atypeFactory, checker, dependentTypesHelper, env, fieldValues, qualifierHierarchy, typeHierarchy, types

Fields inherited from class org.checkerframework.dataflow.analysis.ForwardAnalysisImpl

blockCount, elseStores, maxCountBeforeWidening, storesAtReturnStatements, thenStores

Fields inherited from class org.checkerframework.dataflow.analysis.AbstractAnalysis

cfg, currentInput, currentNode, currentTree, direction, finalLocalValues, inputs, isRunning, nodeValues, transferFunction, worklist

Constructor Summary

Constructors

Constructor and Description
LockAnalysis(BaseTypeChecker checker, LockAnnotatedTypeFactory factory, List<Pair<VariableElement,CFValue>> fieldValues)

Method Summary

Modifier and Type	Method and Description
CFValue	createAbstractValue(Set<AnnotationMirror> annotations, TypeMirror underlyingType) Returns an abstract value containing the given annotations and underlyingType.
LockStore	createCopiedStore(LockStore s) Returns an identical copy of the store s.
LockStore	createEmptyStore(boolean sequentialSemantics) Returns an empty store of the appropriate type.
LockTransfer	createTransferFunction() Returns the transfer function to be used by the analysis.

Methods inherited from class org.checkerframework.framework.flow.CFAbstractAnalysis

createAbstractValue, createSingleAnnotationValue, defaultCreateAbstractValue, getEnv, getFieldValues, getTypeFactory, getTypeHierarchy, getTypes, performAnalysis

Methods inherited from class org.checkerframework.dataflow.analysis.ForwardAnalysisImpl

addStoreBefore, callTransferFunction, getInput, getInputBefore, getReturnStatementStores, getStoreBefore, initFields, initInitialInputs, performAnalysis, performAnalysisBlock, propagateStoresTo, runAnalysisFor

Methods inherited from class org.checkerframework.dataflow.analysis.AbstractAnalysis

addToWorklist, getContainingClass, getContainingMethod, getCurrentTree, getDirection, getExceptionalExitStore, getNodesForTree, getNodeValues, getRegularExitStore, getResult, getTransferFunction, getValue, getValue, init, isRunning, readFromStore, setCurrentNode, setCurrentTree, updateNodeValues

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface org.checkerframework.dataflow.analysis.Analysis

getDirection, getExceptionalExitStore, getRegularExitStore, getResult, getTransferFunction, getValue, getValue, isRunning

Constructor Detail

LockAnalysis

public LockAnalysis(BaseTypeChecker checker,
                    LockAnnotatedTypeFactory factory,
                    List<Pair<VariableElement,CFValue>> fieldValues)

Method Detail

createTransferFunction

public LockTransfer createTransferFunction()

Description copied from class: CFAbstractAnalysis

Returns the transfer function to be used by the analysis.

Overrides:

createTransferFunction in class CFAbstractAnalysis<CFValue,LockStore,LockTransfer>

Returns:

the transfer function to be used by the analysis

createEmptyStore

public LockStore createEmptyStore(boolean sequentialSemantics)

Description copied from class: CFAbstractAnalysis

Returns an empty store of the appropriate type.

Specified by:

createEmptyStore in class CFAbstractAnalysis<CFValue,LockStore,LockTransfer>

Returns:

an empty store of the appropriate type

createCopiedStore

public LockStore createCopiedStore(LockStore s)

Description copied from class: CFAbstractAnalysis

Returns an identical copy of the store s.

Specified by:

createCopiedStore in class CFAbstractAnalysis<CFValue,LockStore,LockTransfer>

Returns:

an identical copy of the store s

createAbstractValue

public CFValue createAbstractValue(Set<AnnotationMirror> annotations,
                                   TypeMirror underlyingType)

Description copied from class: CFAbstractAnalysis

Returns an abstract value containing the given annotations and underlyingType. Returns null if the annotation set has missing annotations.

Specified by:

createAbstractValue in class CFAbstractAnalysis<CFValue,LockStore,LockTransfer>

Returns:

an abstract value containing the given annotations and underlyingType