Package 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	Description
final CFStore	elseStore	The else store.
final Node	left	The left operand.
final @Nullable AnnotationMirror	leftAnno	Annotation for left expressions.
final ConditionalTransferResult<CFValue,CFStore>	newResult	The new result, after refinement.
final Node	right	The right operand.
final @Nullable AnnotationMirror	rightAnno	Annotation for right expressions.
final 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 Details

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 Details

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)