Package org.checkerframework.checker.index

Class IndexRefinementInfo

java.lang.Object

org.checkerframework.checker.index.IndexRefinementInfo

public class IndexRefinementInfo
extends java.lang.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	Description
CFStore	elseStore	The else store.
Node	left	The left operand.
@Nullable javax.lang.model.element.AnnotationMirror	leftAnno	Annotation for left expressions.
ConditionalTransferResult<CFValue,CFStore>	newResult	The new result, after refinement.
Node	right	The right operand.
@Nullable javax.lang.model.element.AnnotationMirror	rightAnno	Annotation for right expressions.
CFStore	thenStore	The then store.

Constructor Summary

Constructors

Constructor	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 javax.lang.model.element.AnnotationMirror leftAnno

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

rightAnno

public final @Nullable javax.lang.model.element.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)