de.uka.ilkd.key.symbolic_execution

Class SymbolicExecutionTreeBuilder.MethodFrameCounterJavaASTVisitor

java.lang.Object

de.uka.ilkd.key.java.visitor.JavaASTWalker

de.uka.ilkd.key.java.visitor.JavaASTVisitor

de.uka.ilkd.key.symbolic_execution.SymbolicExecutionTreeBuilder.MethodFrameCounterJavaASTVisitor

All Implemented Interfaces:

Visitor

Enclosing class:

SymbolicExecutionTreeBuilder

private static final class SymbolicExecutionTreeBuilder.MethodFrameCounterJavaASTVisitor
extends JavaASTVisitor

Utility class used in SymbolicExecutionTreeBuilder.initNewLoopBodyMethodCallStack(Node) to compute the number of available MethodFrames.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private int	count The number of MethodFrames.

Fields inherited from class de.uka.ilkd.key.java.visitor.JavaASTVisitor

services

Constructor Summary

Constructors

Constructor and Description
MethodFrameCounterJavaASTVisitor(ProgramElement root, Services services) Constructor.

Method Summary

Modifier and Type	Method and Description
protected void	doDefaultAction(SourceElement node) the action that is performed just before leaving the node the last time
void	performActionOnMethodFrame(MethodFrame x)
int	run() Performs the counting of MethodFrames.

Methods inherited from class de.uka.ilkd.key.java.visitor.JavaASTVisitor

doAction, performActionOnAbstractProgramElement, performActionOnAllFields, performActionOnAllObjects, performActionOnArrayDeclaration, performActionOnArrayInitializer, performActionOnArrayLengthReference, performActionOnArrayReference, performActionOnAssert, performActionOnBinaryAnd, performActionOnBinaryAndAssignment, performActionOnBinaryNot, performActionOnBinaryOr, performActionOnBinaryOrAssignment, performActionOnBinaryXOr, performActionOnBinaryXOrAssignment, performActionOnBlockContract, performActionOnBlockContract, performActionOnBooleanLiteral, performActionOnBreak, performActionOnCase, performActionOnCatch, performActionOnCatchAllStatement, performActionOnCharLiteral, performActionOnClassDeclaration, performActionOnClassInitializer, performActionOnComment, performActionOnCompilationUnit, performActionOnConditional, performActionOnConstructorDeclaration, performActionOnContextStatementBlock, performActionOnContinue, performActionOnCopyAssignment, performActionOnDefault, performActionOnDivide, performActionOnDivideAssignment, performActionOnDLEmbeddedExpression, performActionOnDo, performActionOnDoubleLiteral, performActionOnElse, performActionOnEmptyMapLiteral, performActionOnEmptySeqLiteral, performActionOnEmptySetLiteral, performActionOnEmptyStatement, performActionOnEnhancedFor, performActionOnEquals, performActionOnExactInstanceof, performActionOnExecutionContext, performActionOnExtends, performActionOnFieldDeclaration, performActionOnFieldReference, performActionOnFieldSpecification, performActionOnFinally, performActionOnFloatLiteral, performActionOnFor, performActionOnForUpdates, performActionOnGreaterOrEquals, performActionOnGreaterThan, performActionOnGuard, performActionOnIf, performActionOnImplements, performActionOnImplicitFieldSpecification, performActionOnImport, performActionOnInstanceof, performActionOnInterfaceDeclaration, performActionOnIntersect, performActionOnIntLiteral, performActionOnIProgramVariable, performActionOnLabeledStatement, performActionOnLessOrEquals, performActionOnLessThan, performActionOnLocalVariableDeclaration, performActionOnLocationVariable, performActionOnLogicalAnd, performActionOnLogicalNot, performActionOnLogicalOr, performActionOnLongLiteral, performActionOnLoopContract, performActionOnLoopContract, performActionOnLoopContract, performActionOnLoopInit, performActionOnLoopInvariant, performActionOnLoopScopeBlock, performActionOnMergeContract, performActionOnMergePointStatement, performActionOnMetaClassReference, performActionOnMethod, performActionOnMethodBodyStatement, performActionOnMethodDeclaration, performActionOnMethodReference, performActionOnMinus, performActionOnMinusAssignment, performActionOnModifier, performActionOnModulo, performActionOnModuloAssignment, performActionOnNegative, performActionOnNew, performActionOnNewArray, performActionOnNotEquals, performActionOnNullLiteral, performActionOnPackageReference, performActionOnPackageSpecification, performActionOnParameterDeclaration, performActionOnParenthesizedExpression, performActionOnPassiveExpression, performActionOnPlus, performActionOnPlusAssignment, performActionOnPositive, performActionOnPostDecrement, performActionOnPostIncrement, performActionOnPreDecrement, performActionOnPreIncrement, performActionOnProgramConstant, performActionOnProgramElementName, performActionOnProgramMetaConstruct, performActionOnProgramMethod, performActionOnProgramVariable, performActionOnReturn, performActionOnSchematicFieldReference, performActionOnSchemaVariable, performActionOnSeqConcat, performActionOnSeqGet, performActionOnSeqIndexOf, performActionOnSeqLength, performActionOnSeqReverse, performActionOnSeqSingleton, performActionOnSeqSub, performActionOnSetMinus, performActionOnSetUnion, performActionOnShiftLeft, performActionOnShiftLeftAssignment, performActionOnShiftRight, performActionOnShiftRightAssignment, performActionOnSingleton, performActionOnStatementBlock, performActionOnStringLiteral, performActionOnSuperArrayDeclaration, performActionOnSuperConstructorReference, performActionOnSuperReference, performActionOnSwitch, performActionOnSynchronizedBlock, performActionOnThen, performActionOnThisConstructorReference, performActionOnThisReference, performActionOnThrow, performActionOnThrows, performActionOnTimes, performActionOnTimesAssignment, performActionOnTransactionStatement, performActionOnTry, performActionOnTypeCast, performActionOnTypeReference, performActionOnUnsignedShiftRight, performActionOnUnsignedShiftRightAssignment, performActionOnVariableDeclaration, performActionOnVariableReference, performActionOnVariableSpecification, performActionOnWhile, walk

Methods inherited from class de.uka.ilkd.key.java.visitor.JavaASTWalker

depth, root, start

Methods inherited from class java.lang.Object

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

Field Detail

count

private int count

The number of MethodFrames.

Constructor Detail

MethodFrameCounterJavaASTVisitor

public MethodFrameCounterJavaASTVisitor(ProgramElement root,
                                        Services services)

Constructor.

Parameters:

root - The ProgramElement to count the contained MethodFrames.

services - The Services to use.

Method Detail

doDefaultAction

protected void doDefaultAction(SourceElement node)

the action that is performed just before leaving the node the last time

Specified by:

doDefaultAction in class JavaASTVisitor

Parameters:

node - the node described above

performActionOnMethodFrame

public void performActionOnMethodFrame(MethodFrame x)

Specified by:

performActionOnMethodFrame in interface Visitor

Overrides:

performActionOnMethodFrame in class JavaASTVisitor

run

public int run()

Performs the counting of MethodFrames.

Returns:

The number of found MethodFrames.