Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.declaration |
Elements of the Java syntax tree representing declarations.
|
de.uka.ilkd.key.java.expression |
Elements of the Java syntax tree representing expressions.
|
de.uka.ilkd.key.java.expression.literal |
This package contains representations for the various Java literal types.
|
de.uka.ilkd.key.java.expression.operator |
Elements of the Java syntax tree representing operators and operator-like
expressions.
|
de.uka.ilkd.key.java.expression.operator.adt | |
de.uka.ilkd.key.java.reference |
Elements of the Java syntax tree representing implicit or explicit (named)
references to other program elements.
|
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.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
Modifier and Type | Method and Description |
---|---|
void |
CcatchReturnValParameterDeclaration.visit(Visitor v) |
void |
CcatchReturnParameterDeclaration.visit(Visitor v) |
void |
SourceElement.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
PackageSpecification.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
CcatchContinueWildcardParameterDeclaration.visit(Visitor v) |
void |
ContextStatementBlock.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Label.visit(Visitor v) |
void |
Import.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
CcatchBreakWildcardParameterDeclaration.visit(Visitor v) |
void |
CcatchContinueLabelParameterDeclaration.visit(Visitor v) |
void |
CcatchContinueParameterDeclaration.visit(Visitor v) |
void |
CcatchBreakParameterDeclaration.visit(Visitor v) |
void |
StatementBlock.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
CompilationUnit.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
CcatchBreakLabelParameterDeclaration.visit(Visitor v) |
void |
Comment.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
Modifier and Type | Method and Description |
---|---|
void |
InterfaceDeclaration.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
LocalVariableDeclaration.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ArrayDeclaration.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
VariableDeclaration.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ClassDeclaration.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Throws.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Implements.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
FieldSpecification.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
VariableSpecification.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ConstructorDeclaration.visit(Visitor v) |
void |
Modifier.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ImplicitFieldSpecification.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
FieldDeclaration.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Extends.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ClassInitializer.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ParameterDeclaration.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
MethodDeclaration.visit(Visitor v) |
void |
SuperArrayDeclaration.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
Modifier and Type | Method and Description |
---|---|
void |
PassiveExpression.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ArrayInitializer.visit(Visitor v) |
void |
ParenthesizedExpression.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
Modifier and Type | Method and Description |
---|---|
void |
EmptySeqLiteral.visit(Visitor v) |
void |
StringLiteral.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
DoubleLiteral.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
NullLiteral.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
CharLiteral.visit(Visitor v) |
void |
EmptySetLiteral.visit(Visitor v) |
void |
RealLiteral.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
FloatLiteral.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
BooleanLiteral.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
IntLiteral.visit(Visitor v) |
void |
FreeLiteral.visit(Visitor v) |
void |
LongLiteral.visit(Visitor v) |
void |
EmptyMapLiteral.visit(Visitor v) |
Modifier and Type | Method and Description |
---|---|
void |
PreIncrement.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
PlusAssignment.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Plus.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
TimesAssignment.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
UnsignedShiftRightAssignment.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ShiftLeftAssignment.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
PostDecrement.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
MinusAssignment.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
GreaterOrEquals.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Positive.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ExactInstanceof.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ShiftLeft.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
LessThan.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
TypeCast.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
BinaryOr.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
LogicalOr.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ShiftRightAssignment.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
LessOrEquals.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Intersect.visit(Visitor v) |
void |
Equals.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Instanceof.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Divide.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
GreaterThan.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Negative.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
PostIncrement.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
BinaryXOr.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
CopyAssignment.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Minus.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
BinaryXOrAssignment.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
New.visit(Visitor v) |
void |
NewArray.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
BinaryAndAssignment.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
BinaryAnd.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
NotEquals.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
BinaryOrAssignment.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
UnsignedShiftRight.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
DivideAssignment.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
LogicalNot.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Conditional.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
DLEmbeddedExpression.visit(Visitor v) |
void |
PreDecrement.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Modulo.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
BinaryNot.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Times.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ShiftRight.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ModuloAssignment.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
LogicalAnd.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
Modifier and Type | Method and Description |
---|---|
void |
SeqIndexOf.visit(Visitor v) |
void |
SetUnion.visit(Visitor v) |
void |
SeqSingleton.visit(Visitor v) |
void |
SeqConcat.visit(Visitor v) |
void |
SeqReverse.visit(Visitor v) |
void |
SeqGet.visit(Visitor v) |
void |
AllFields.visit(Visitor v) |
void |
AllObjects.visit(Visitor v) |
void |
SeqLength.visit(Visitor v) |
void |
SeqSub.visit(Visitor v) |
void |
SetMinus.visit(Visitor v) |
void |
Singleton.visit(Visitor v) |
Modifier and Type | Method and Description |
---|---|
void |
ArrayLengthReference.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ThisConstructorReference.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
MetaClassReference.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
SchemaTypeReference.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
MethodReference.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
SuperConstructorReference.visit(Visitor v) |
void |
TypeReferenceImp.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
PackageReference.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ExecutionContext.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ArrayReference.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
SuperReference.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
ThisReference.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
VariableReference.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
SchematicFieldReference.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
FieldReference.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
Modifier and Type | Method and Description |
---|---|
void |
Return.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
EnhancedFor.visit(Visitor v) |
void |
MethodBodyStatement.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Catch.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Switch.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Exec.visit(Visitor v)
calls the corresponding method of a visitor in order to perform some
action/transformation on this element
|
void |
LoopScopeBlock.visit(Visitor v)
Calls the corresponding method of a visitor in order to perform some
action/transformation on this element
|
void |
MethodFrame.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Throw.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
CatchAllStatement.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
LoopInit.visit(Visitor v) |
void |
MergePointStatement.visit(Visitor v)
calls the corresponding method of a visitor in order to perform some
action/transformation on this element
|
void |
ForUpdates.visit(Visitor v) |
void |
While.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Finally.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Default.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
For.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Try.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Break.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
SynchronizedBlock.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Guard.visit(Visitor v) |
void |
LabeledStatement.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Then.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Continue.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Assert.visit(Visitor v) |
void |
Else.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Ccatch.visit(Visitor v)
calls the corresponding method of a visitor in order to perform some
action/transformation on this element
|
void |
TransactionStatement.visit(Visitor v) |
void |
Do.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
EmptyStatement.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
Case.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
void |
If.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
Modifier and Type | Class and Description |
---|---|
class |
ContainsStatementVisitor
Utilits class used by
SymbolicExecutionUtil#containsStatement(MethodFrame, ProgramElement, Services) . |
class |
CreatingASTVisitor
Walks through a java AST in depth-left-fist-order.
|
class |
DeclarationProgramVariableCollector
The DeclarationProgramVariableCollector collects all top level
declared program variables relative to the given block to be
visited, for example starting with
{ int j; { int i; } { int h; } for (int k; ...) {} int h; }
the collector will return a set containg j, h the
h because of the second occurrence of h |
class |
FieldReplaceVisitor
Replaces field references o.a by methodcalls o._a().
|
class |
InnerBreakAndContinueReplacer
This replaces all breaks and continues in a loop with
break l , where l is a
specified label. |
class |
JavaASTVisitor
Extends the JavaASTWalker to use the visitor mechanism.
|
class |
LabelCollector
Collects all labels found in a given program.
|
class |
OuterBreakContinueAndReturnCollector |
class |
OuterBreakContinueAndReturnReplacer |
class |
ProgramElementReplacer |
class |
ProgramReplaceVisitor
Walks through a java AST in depth-left-fist-order.
|
class |
ProgramVariableCollector
Walks through a java AST in depth-left-fist-order.
|
class |
ProgVarReplaceVisitor
Walks through a java AST in depth-left-first-order.
|
class |
UndeclaredProgramVariableCollector
This class is a specialization of
ProgramVariableCollector which
returns as result (UndeclaredProgramVariableCollector.result() ) used LocationVariable which
are undeclared, but used in the given {@link ProgramElement. |
Modifier and Type | Method and Description |
---|---|
void |
ProgramElementName.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
Modifier and Type | Method and Description |
---|---|
void |
ProgramVariable.visit(Visitor v) |
void |
LocationVariable.visit(Visitor v) |
void |
ProgramMethod.visit(Visitor v)
calls the corresponding method of a visitor in order to perform some
action/transformation on this element
|
void |
ProgramConstant.visit(Visitor v) |
void |
ProgramSV.visit(Visitor v) |
Modifier and Type | Class and Description |
---|---|
class |
ForToWhileTransformation
This transformation is used to transform a for-loop into a while-loop.
|
class |
ReplaceWhileLoop
This visitor is used to identify and replace the while loop
in invariant rule.
|
class |
WhileInvariantTransformation
Walks through a java AST in depth-left-fist-order.
|
class |
WhileLoopTransformation
Walks through a java AST in depth-left-fist-order.
|
Modifier and Type | Method and Description |
---|---|
void |
ProgramTransformer.visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
Modifier and Type | Method and Description |
---|---|
void |
LoopSpecification.visit(Visitor v)
Loop invariants can be visited like source elements:
This method calls the corresponding method of a visitor in order to
perform some action/transformation on this element.
|
void |
BlockContractImpl.visit(Visitor visitor) |
void |
LoopContractImpl.visit(Visitor visitor) |
void |
AuxiliaryContract.visit(Visitor visitor)
Accepts a visitor.
|
void |
LoopSpecImpl.visit(Visitor v) |
Copyright © 2003-2019 The KeY-Project.