org.checkerframework.checker.index

Class IndexRefinementInfo

java.lang.Object

org.checkerframework.checker.index.IndexRefinementInfo

public class IndexRefinementInfo
extends Object

This struct contains all of the information that the refinement functions need. It's called by each node function (i.e. greater than node, less than node, etc.) and then the results are passed to the refinement function in whatever order is appropriate for that node. Its constructor contains all of its logic.

Field Summary

Fields

Modifier and Type	Field and Description
CFStore	elseStore The else store.
Node	left The left operand.
@Nullable AnnotationMirror	leftAnno Annotation for left expressions.
ConditionalTransferResult<CFValue,CFStore>	newResult The new result, after refinement.
Node	right The right operand.
@Nullable AnnotationMirror	rightAnno Annotation for right expressions.
CFStore	thenStore The then store.

Constructor Summary

Constructors

Constructor and Description
IndexRefinementInfo(TransferResult<CFValue,CFStore> result, CFAbstractAnalysis<?,?,?> analysis, BinaryOperationNode node)
IndexRefinementInfo(TransferResult<CFValue,CFStore> result, CFAbstractAnalysis<?,?,?> analysis, Node right, Node left) Creates a new IndexRefinementInfo.

Method Summary

Methods inherited from class java.lang.Object

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

Field Detail

left

public final Node left

The left operand.

right

public final Node right

The right operand.

leftAnno

public final @Nullable AnnotationMirror leftAnno

Annotation for left expressions. Might be null if dataflow doesn't have a value for the expression.

rightAnno

public final @Nullable AnnotationMirror rightAnno

Annotation for right expressions. Might be null if dataflow doesn't have a value for the expression.

thenStore

public final CFStore thenStore

The then store.

elseStore

public final CFStore elseStore

The else store.

newResult

public final ConditionalTransferResult<CFValue,CFStore> newResult

The new result, after refinement.

Constructor Detail

IndexRefinementInfo

public IndexRefinementInfo(TransferResult<CFValue,CFStore> result,
                           CFAbstractAnalysis<?,?,?> analysis,
                           Node right,
                           Node left)

Creates a new IndexRefinementInfo.

Parameters:

left - the left operand

right - the right operand

result - the new result, after refinement

analysis - the CFAbstractAnalysis

IndexRefinementInfo

public IndexRefinementInfo(TransferResult<CFValue,CFStore> result,
                           CFAbstractAnalysis<?,?,?> analysis,
                           BinaryOperationNode node)