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.statement |
Elements of the Java syntax tree representing pure statements.
|
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.symbolic_execution.po | |
de.uka.ilkd.key.symbolic_execution.strategy.breakpoint |
Modifier and Type | Interface and Description |
---|---|
interface |
ParameterContainer
Describes program elements that contain
ParameterDeclaration s. |
Modifier and Type | Class and Description |
---|---|
class |
CcatchReturnValParameterDeclaration
A "\Return int v" parameter declaration of a ccatch clause.
|
class |
ContextStatementBlock
In the DL-formulae description of Taclets the program part can have
the following form < pi alpha;...; omega > Phi where pi is a prefix
consisting of open brackets, try's and so on and omega is the rest
of the program.
|
class |
StatementBlock
Statement block.
|
Modifier and Type | Class and Description |
---|---|
class |
ClassInitializer |
class |
ConstructorDeclaration
The getTypeReference method returns null - constructors do not have
explicite return types.
|
class |
MethodDeclaration
Method declaration.
|
Modifier and Type | Interface and Description |
---|---|
interface |
Branch
Branch.
|
Modifier and Type | Class and Description |
---|---|
class |
BranchImp
Branch.
|
class |
Case
Case.
|
class |
Catch
Catch.
|
class |
CatchAllStatement |
class |
Ccatch
Ccatch.
|
class |
Default
Default.
|
class |
Do
Do.
|
class |
Else
Else.
|
class |
EnhancedFor
The new enhanced form of a for-loop.
|
class |
Exec
Exec.
|
class |
Finally
Finally.
|
class |
For
For.
|
class |
LabeledStatement
Labeled statement.
|
class |
LoopInit |
class |
LoopScopeBlock
Loop scope block.
|
class |
LoopStatement
Loop statement.
|
class |
MethodFrame
The statement inserted by KeY if a method call is executed.
|
class |
SynchronizedBlock
Synchronized block.
|
class |
Then
Then.
|
class |
Try
Try.
|
class |
While
While.
|
Modifier and Type | Interface and Description |
---|---|
interface |
ProgramConstruct
A type that implement this interface can be used in all java
programs instead of an expression or statement.
|
Modifier and Type | Class and Description |
---|---|
class |
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
Modifier and Type | Class and Description |
---|---|
class |
ArrayLength |
class |
ArrayPostDecl
Replaces a local variable declaration
#t #v[]; with
#t[] #v; |
class |
ConstructorCall
The constructor call meta construct is used to handle a allocation expression
like
new Class(...) . |
class |
CreateObject
If an allocation expression
new Class(...) occurs, a new object
has to be created, in KeY this is quite similar to take it out of a list of
objects and setting the implicit flag <created> to
true as well as setting all fields of the object to their
default values. |
class |
DoBreak
This class performs a labeled break.
|
class |
EnhancedForElimination
This class defines a meta operator to resolve an enhanced for loop - by transformation to a
"normal" loop.
|
class |
EvaluateArgs
TODO
|
class |
ExpandMethodBody
Replaces the MethodBodyStatement shortcut with the full body, performs prefix
adjustments in the body (execution context).
|
class |
ForInitUnfoldTransformer
Pulls the initializor out of a for-loop.
|
class |
ForToWhile
converts a for-loop to a while loop.
|
class |
InitArray
Split an array creation expression with explicit array initializer,
creating a creation expression with dimension expression and a list
of assignments (-> Java language specification, 15.10)
|
class |
InitArrayCreation
Split an array creation expression with explicit array initializer, creating
a creation expression with dimension expression and a list of assignments (->
Java language specification, 15.10)
This meta construct delivers the creation expression
|
class |
IsStatic
Creates a true or false literal if the given program element is or is not a
static variable reference.
|
class |
MethodCall
Symbolically executes a method invocation
|
class |
MultipleVarDecl
Replaces a declaration of multiple variables by two variable declarations
where the first one declares a single variable and the second one the
remaining variables.
|
class |
PostWork
creates an assignment instantiationOf(#newObjectsV).
|
class |
ProgramTransformer
ProgramTransformers are used to describe schematic transformations
that cannot be expressed by the taclet language itself.
|
class |
ReattachLoopInvariant
Construct for re-attaching a loop invariant that otherwise would get lost
after a transformation, for instance, the loop scope-based unwinding rule.
|
class |
SpecialConstructorCall
The constructor call meta construct is used to handle a allocation expression
like
new Class(...) . |
class |
StaticInitialisation |
class |
SwitchToIf
This class is used to perform program transformations needed for the symbolic
execution of a switch-case statement.
|
class |
TypeOf |
class |
Unpack |
class |
UnwindLoop
This class is used to perform program transformations needed for the symbolic
execution of a loop.
|
Modifier and Type | Method and Description |
---|---|
protected void |
ProgramMethodSubsetPO.collectStatementsToExecute(java.util.List<Statement> toFill,
StatementContainer container)
Collects recursive the
Statement s which are in the given source range
defined by ProgramMethodSubsetPO.startPosition and ProgramMethodSubsetPO.endPosition . |
Modifier and Type | Method and Description |
---|---|
protected abstract StatementBlock |
AbstractConditionalBreakpoint.getStatementBlock(StatementContainer statementContainer)
For a given
StatementContainer this method computes the StatementBlock that contains all lines before the line the Breakpoint is at, including the line itself. |
protected StatementBlock |
KeYWatchpoint.getStatementBlock(StatementContainer statementContainer) |
protected StatementBlock |
MethodBreakpoint.getStatementBlock(StatementContainer statementContainer) |
protected StatementBlock |
LineBreakpoint.getStatementBlock(StatementContainer statementContainer)
For a given
StatementContainer this method computes the StatementBlock that contains all lines before the line the Breakpoint is at, including the line itself. |
Copyright © 2003-2019 The KeY-Project.