Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.recoderext | |
de.uka.ilkd.key.java.recoderext.expression.literal | |
de.uka.ilkd.key.parser |
This package contains the parser for .key and .proof files.
|
de.uka.ilkd.key.parser.proofjava | |
de.uka.ilkd.key.parser.schemajava |
Class and Description |
---|
CatchAllStatement |
CatchSVWrapper |
Ccatch
A ccatch statement (branch of exec statement).
|
CcatchBreakLabelParameterDeclaration
A "\Break label" parameter of a ccatch clause.
|
CcatchBreakParameterDeclaration
A "\Break" parameter of a ccatch clause.
|
CcatchBreakWildcardParameterDeclaration
A "\Break *" parameter of a ccatch clause.
|
CcatchContinueLabelParameterDeclaration
A "\Continue label" parameter of a ccatch clause.
|
CcatchContinueParameterDeclaration
A "\Continue" parameter of a ccatch clause.
|
CcatchContinueWildcardParameterDeclaration
A "\Continue *" parameter of a ccatch clause.
|
CcatchNonstandardParameterDeclaration
A "non-standard" parameter declaration of a Ccatch clause, e.g., "\Return".
|
CcatchReturnParameterDeclaration
A "\Return" parameter of a ccatch clause.
|
CcatchReturnValParameterDeclaration
A "\Return" parameter of a ccatch clause.
|
CcatchSVWrapper |
ClassFileDeclarationBuilder
Make a ClassDeclaration out of a class file.
|
ClassFileDeclarationManager
This class provides an infrastructure to read in multiple class files and to
manufacture ClassDeclarations out of them.
|
ContextStatementBlock
Statement block.
|
EscapeExpression
Handles JML expressions that begin with an escape character '\'.
|
Exec
An exec statement.
|
ExecCtxtSVWrapper |
ExecutionContext |
ExpressionSVWrapper |
ExtendedIdentifier
an extended identifier that accepts hash symbols in its name
but not as first character
|
Ghost |
ImplicitIdentifier
subclasses the recoder Identifier in order to allow fields with special
characters.
|
JumpLabelSVWrapper |
KeYAnnotationUseSpecification |
KeYCrossReferenceServiceConfiguration |
KeYRecoderExtension |
LabelSVWrapper |
LoopScopeBlock
TODO
|
MergePointStatement |
MethodBodyStatement
A shortcut-statement for a method body.
|
MethodCallStatement
The statement inserted by KeY if a method call is executed.
|
MethodSignatureSVWrapper |
Model |
NewArrayWrapper |
NewWrapper |
NoState |
ObjectTypeIdentifier |
PassiveExpression |
ProgramVariableSVWrapper |
RecoderModelTransformer
The Java DL requires some implicit fields, that are available in each
Java class.
|
RecoderModelTransformer.TransformerCache
Cache of important data.
|
RKeYMetaConstruct |
RKeYMetaConstructExpression |
RKeYMetaConstructType |
RMethodBodyStatement |
RMethodCallStatement |
SourceVisitorExtended
Adds visitor methods for recoder extensions.
|
SpecialReferenceWrapper |
StatementSVWrapper |
SVWrapper |
TransactionStatement |
TwoState |
TypeSVWrapper |
Class and Description |
---|
KeYRecoderExtension |
Class and Description |
---|
KeYCrossReferenceServiceConfiguration |
Class and Description |
---|
Exec
An exec statement.
|
ExecutionContext |
ImplicitIdentifier
subclasses the recoder Identifier in order to allow fields with special
characters.
|
LoopScopeBlock
TODO
|
MergePointStatement |
MethodBodyStatement
A shortcut-statement for a method body.
|
MethodCallStatement
The statement inserted by KeY if a method call is executed.
|
TransactionStatement |
Copyright © 2003-2019 The KeY-Project.