Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.statement |
Elements of the Java syntax tree representing pure statements.
|
de.uka.ilkd.key.java.visitor |
contains classes representing visitors traversing the tree
structure of Java programs.
|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
MethodFrame |
Recoder2KeYConverter.convert(MethodCallStatement rmcs)
convert a recoderext MethodFrameStatement to a KeY MethodFrameStatement
|
MethodFrame |
SchemaRecoder2KeYConverter.convert(RMethodCallStatement l)
method-call-statements are expanded to method-frames
|
MethodFrame |
ProgramPrefixUtil.ProgramPrefixInfo.getInnerMostMethodFrame() |
MethodFrame |
StatementBlock.getInnerMostMethodFrame() |
static MethodFrame |
JavaTools.getInnermostMethodFrame(JavaBlock jb,
Services services)
Returns the innermost method frame of the passed java block
|
static MethodFrame |
JavaTools.getInnermostMethodFrame(ProgramElement pe,
Services services)
Returns the innermost method frame of the passed java block
|
static MethodFrame |
KeYJavaASTFactory.methodFrame(IExecutionContext executionContext,
StatementBlock block)
Create a method call substitution.
|
static MethodFrame |
KeYJavaASTFactory.methodFrame(IExecutionContext executionContext,
StatementBlock block,
PositionInfo position)
Create a method call substitution at a specific source position.
|
static MethodFrame |
KeYJavaASTFactory.methodFrame(IProgramVariable result,
IExecutionContext executionContext,
StatementBlock block)
Create a method call substitution with a return value assignment.
|
static MethodFrame |
KeYJavaASTFactory.methodFrame(IProgramVariable result,
IExecutionContext executionContext,
StatementBlock block,
PositionInfo position)
Create a method call substitution with a return value assignment at a
specific source position.
|
Modifier and Type | Method and Description |
---|---|
void |
PrettyPrinter.printMethodFrame(MethodFrame x) |
Constructor and Description |
---|
ProgramPrefixInfo(int length,
MethodFrame mf) |
Modifier and Type | Method and Description |
---|---|
MethodFrame |
Exec.getInnerMostMethodFrame() |
MethodFrame |
LoopScopeBlock.getInnerMostMethodFrame() |
MethodFrame |
MethodFrame.getInnerMostMethodFrame() |
MethodFrame |
Try.getInnerMostMethodFrame() |
MethodFrame |
SynchronizedBlock.getInnerMostMethodFrame() |
MethodFrame |
LabeledStatement.getInnerMostMethodFrame() |
Modifier and Type | Method and Description |
---|---|
protected MethodFrame |
ProgramContextAdder.createMethodFrameWrapper(MethodFrame old,
StatementBlock body) |
Modifier and Type | Method and Description |
---|---|
protected MethodFrame |
ProgramContextAdder.createMethodFrameWrapper(MethodFrame old,
StatementBlock body) |
void |
Visitor.performActionOnMethodFrame(MethodFrame x) |
void |
OuterBreakContinueAndReturnReplacer.performActionOnMethodFrame(MethodFrame x) |
void |
InnerBreakAndContinueReplacer.performActionOnMethodFrame(MethodFrame x) |
void |
CreatingASTVisitor.performActionOnMethodFrame(MethodFrame x) |
void |
JavaASTVisitor.performActionOnMethodFrame(MethodFrame x) |
void |
UndeclaredProgramVariableCollector.performActionOnMethodFrame(MethodFrame x) |
Modifier and Type | Method and Description |
---|---|
MethodFrame |
ProgramPrefix.getInnerMostMethodFrame()
returns the inner most
MethodFrame |
Modifier and Type | Field and Description |
---|---|
protected java.util.Stack<MethodFrame> |
WhileLoopTransformation.methodStack |
Modifier and Type | Method and Description |
---|---|
void |
WhileLoopTransformation.performActionOnMethodFrame(MethodFrame x) |
void |
ReplaceWhileLoop.performActionOnMethodFrame(MethodFrame x) |
Modifier and Type | Method and Description |
---|---|
protected boolean |
SymbolicExecutionTreeBuilder.isAfterBlockReached(int currentStackSize,
MethodFrame currentInnerMostMethodFrame,
SourceElement currentActiveStatement,
int expectedStackSize,
java.util.Iterator<SourceElement> expectedStatementsIterator)
Checks if the after block condition is fulfilled.
|
protected boolean |
SymbolicExecutionTreeBuilder.isAfterBlockReached(int currentStackSize,
MethodFrame currentInnerMostMethodFrame,
SourceElement currentActiveStatement,
SymbolicExecutionTreeBuilder.JavaPair expectedPair)
Checks if the after block condition is fulfilled.
|
Modifier and Type | Method and Description |
---|---|
static ProgramVariable |
MiscTools.getSelf(MethodFrame mf) |
static Term |
MiscTools.getSelfTerm(MethodFrame mf,
Services services)
Returns the receiver term of the passed method frame, or null if the frame belongs to a
static method.
|
Copyright © 2003-2019 The KeY-Project.