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.operator |
Elements of the Java syntax tree representing operators and operator-like
expressions.
|
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.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.jml.translation | |
de.uka.ilkd.key.symbolic_execution.po |
Modifier and Type | Interface and Description |
---|---|
interface |
LoopInitializer
Loop initializer.
|
Modifier and Type | Class and Description |
---|---|
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 | Method and Description |
---|---|
static Statement |
KeYJavaASTFactory.breakStatement(Label label,
PositionInfo positionInfo) |
Statement |
Recoder2KeYConverter.convertBody(LoopStatement ls)
helper for convert(x) with x a LoopStatement.
|
Statement |
CcatchReturnValParameterDeclaration.getStatementAt(int index) |
Statement |
StatementContainer.getStatementAt(int index) |
Statement |
StatementBlock.getStatementAt(int index) |
static Statement |
KeYJavaASTFactory.ifElse(Expression guard,
Statement thenStatement,
Statement elseStatement)
Create an if clause.
|
static Statement |
KeYJavaASTFactory.labeledStatement(Label label,
Statement[] statements,
PositionInfo pos)
Create a labeled block of statements.
|
static Statement |
KeYJavaASTFactory.whileLoop(Expression condition,
Statement body)
Create a while loop.
|
Modifier and Type | Method and Description |
---|---|
protected java.util.List<Statement> |
CreateArrayMethodBuilder.createArray(ImmutableList<Field> fields)
creates the statements which take the next object out of the list of
available objects
|
ImmutableArray<? extends Statement> |
StatementBlock.getBody()
Get body.
|
Modifier and Type | Method and Description |
---|---|
static StatementBlock |
KeYJavaASTFactory.block(Statement... statements)
Create a block from an arbitrary number of statements.
|
static Case |
KeYJavaASTFactory.caseBlock(Expression expression,
Statement statement)
Create a case block.
|
static Case |
KeYJavaASTFactory.caseBlock(Expression expression,
Statement[] statements)
Create a case block.
|
static Catch |
KeYJavaASTFactory.catchClause(ParameterDeclaration parameter,
Statement[] statements)
Create a catch clause.
|
static Default |
KeYJavaASTFactory.defaultBlock(Statement statement)
Create a default block.
|
static Default |
KeYJavaASTFactory.defaultBlock(Statement[] statements)
Create a default block.
|
static Do |
KeYJavaASTFactory.doLoop(Expression condition,
Statement statement,
PositionInfo positionInfo)
Create a do loop.
|
static Else |
KeYJavaASTFactory.elseBlock(Statement statement)
Create an else block.
|
static Else |
KeYJavaASTFactory.elseBlock(Statement[] statements)
Create an else block.
|
static Finally |
KeYJavaASTFactory.finallyBlock(Statement statement)
Create a finally block.
|
static Finally |
KeYJavaASTFactory.finallyBlock(Statement[] statements)
Create a finally block.
|
static For |
KeYJavaASTFactory.forLoop(IGuard guard,
IForUpdates updates,
Statement body)
Create a for loop with no initializer.
|
static For |
KeYJavaASTFactory.forLoop(IGuard guard,
IForUpdates updates,
Statement[] body)
Create a for loop with no initializer.
|
static For |
KeYJavaASTFactory.forLoop(ILoopInit init,
IGuard guard,
IForUpdates updates,
Statement... statements)
Create a for loop from the loop definition and an arbitrary number of
body statements.
|
static Statement |
KeYJavaASTFactory.ifElse(Expression guard,
Statement thenStatement,
Statement elseStatement)
Create an if clause.
|
static If |
KeYJavaASTFactory.ifThen(Expression guard,
Statement... statements)
Create an if statement with no else branch.
|
static If |
KeYJavaASTFactory.ifThen(Expression guard,
Statement then)
Create an if statement with no else branch.
|
static StatementBlock |
KeYJavaASTFactory.insertStatementInBlock(Statement[] stmnt,
StatementBlock b)
inserts the given statements at the begin of the block
|
static StatementBlock |
KeYJavaASTFactory.insertStatementInBlock(StatementBlock block,
Statement[] statements)
Create a block where the given statements come after the given block.
|
static StatementBlock |
KeYJavaASTFactory.insertStatementInBlock(Statement statement,
StatementBlock block)
Insert a statement in a block of statements.
|
static Statement |
KeYJavaASTFactory.labeledStatement(Label label,
Statement[] statements,
PositionInfo pos)
Create a labeled block of statements.
|
static LabeledStatement |
KeYJavaASTFactory.labeledStatement(Label label,
Statement statement,
PositionInfo pos)
Create a labeled statement.
|
static Then |
KeYJavaASTFactory.thenBlock(Statement statement)
Create a then block.
|
static Then |
KeYJavaASTFactory.thenBlock(Statement[] statements)
Create a then block.
|
static Try |
KeYJavaASTFactory.tryBlock(Statement statement,
Branch branch)
Create a try block.
|
static Try |
KeYJavaASTFactory.tryBlock(Statement statement,
Branch[] branches)
Create a try block.
|
static Statement |
KeYJavaASTFactory.whileLoop(Expression condition,
Statement body)
Create a while loop.
|
static While |
KeYJavaASTFactory.whileLoop(Expression condition,
Statement body,
PositionInfo position)
Create a while loop at a specific source position.
|
Modifier and Type | Method and Description |
---|---|
static StatementBlock |
KeYJavaASTFactory.block(java.util.List<Statement> statements)
Create a block from an arbitrary number of statements.
|
static ImmutableArray<ProgramPrefix> |
StatementBlock.computePrefixElements(ImmutableArray<? extends Statement> b,
ProgramPrefix current)
computes the prefix elements for the given array of statment block
|
Constructor and Description |
---|
ContextStatementBlock(Statement[] body,
IExecutionContext executionContext) |
ContextStatementBlock(Statement s,
IExecutionContext executionContext) |
StatementBlock(Statement... body) |
StatementBlock(Statement as) |
Constructor and Description |
---|
StatementBlock(ImmutableArray<? extends Statement> as) |
Modifier and Type | Class and Description |
---|---|
class |
ClassDeclaration
There are several types of class declarations:
package-less outer classes
getClassContainer() == null
getStatementContainer() == null
getName() != null
ordinary outer classes
getClassContainer() instanceof Package
getStatementContainer() == null
getName() != null
member classes
getClassContainer() instanceof ClassDeclaration
getStatementContainer() == null
getName() != null
local class
getClassContainer() == null
getStatementContainer() != null
getName() != null
local anonymous class
getClassContainer() == null
getStatementContainer() instanceof expression.New
getName() == null
Anonymous local classes have exactly one supertype and no
subtypes.
|
class |
EnumClassDeclaration
This class is used for wrapping an enum into a standard class type.
|
class |
LocalVariableDeclaration
Local variable declaration.
|
Modifier and Type | Method and Description |
---|---|
Statement |
ClassInitializer.getStatementAt(int index) |
Statement |
MethodDeclaration.getStatementAt(int index) |
Modifier and Type | Interface and Description |
---|---|
interface |
ExpressionStatement
An ExpressionStatement is a statement that may appear as an expression.
|
Modifier and Type | Class and Description |
---|---|
class |
Assignment
An assignment is an operator with side-effects.
|
class |
ParenthesizedExpression
Redundant Parentheses.
|
class |
PassiveExpression
Marks an active statement as inactive.
|
Modifier and Type | Class and Description |
---|---|
class |
BinaryAndAssignment
Binary and assignment.
|
class |
BinaryOrAssignment
Binary or assignment.
|
class |
BinaryXOrAssignment
Binary X or assignment.
|
class |
CopyAssignment
Copy assignment.
|
class |
DivideAssignment
Divide assignment.
|
class |
MinusAssignment
Minus assignment.
|
class |
ModuloAssignment
Modulo assignment.
|
class |
New
The object allocation operator.
|
class |
PlusAssignment
Addition or string concatenation assignment "+=".
|
class |
PostDecrement
Post decrement.
|
class |
PostIncrement
Post increment.
|
class |
PreDecrement
Pre decrement.
|
class |
PreIncrement
Pre increment.
|
class |
ShiftLeftAssignment
Shift left assignment.
|
class |
ShiftRightAssignment
Shift right assignment.
|
class |
TimesAssignment
Times assignment.
|
class |
UnsignedShiftRightAssignment
Unsigned shift right assignment.
|
Modifier and Type | Interface and Description |
---|---|
interface |
ConstructorReference
Constructor reference.
|
interface |
MethodOrConstructorReference |
Modifier and Type | Class and Description |
---|---|
class |
MethodReference
Method reference.
|
class |
SpecialConstructorReference
Occurs in a constructor declaration as the first statement
as this(...) or super(...) reference.
|
class |
SuperConstructorReference
Super constructor reference.
|
class |
ThisConstructorReference
This constructor reference.
|
Modifier and Type | Class and Description |
---|---|
class |
Assert |
class |
BranchStatement
Branch statement.
|
class |
Break
Break.
|
class |
CatchAllStatement |
class |
Continue
Continue.
|
class |
Do
Do.
|
class |
EmptyStatement
Empty statement.
|
class |
EnhancedFor
The new enhanced form of a for-loop.
|
class |
Exec
Exec.
|
class |
ExpressionJumpStatement
Expression jump statement.
|
class |
For
For.
|
class |
If
If.
|
class |
JavaStatement
Default implementation for non-terminal Java statements.
|
class |
JumpStatement
Jump statement.
|
class |
LabeledStatement
Labeled statement.
|
class |
LabelJumpStatement
Label jump statement.
|
class |
LoopScopeBlock
Loop scope block.
|
class |
LoopStatement
Loop statement.
|
class |
MergePointStatement
A statement indicating a merge point.
|
class |
MethodBodyStatement
A shortcut-statement for a method body, i.e.
|
class |
MethodFrame
The statement inserted by KeY if a method call is executed.
|
class |
Return
Return.
|
class |
Switch
Switch.
|
class |
SynchronizedBlock
Synchronized block.
|
class |
Throw
Throw.
|
class |
TransactionStatement |
class |
Try
Try.
|
class |
While
While.
|
Modifier and Type | Field and Description |
---|---|
protected Statement |
LoopStatement.body
Body.
|
protected Statement |
LabeledStatement.body
Body.
|
protected Statement |
Then.body
Body.
|
protected Statement |
Else.body
Body.
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableArray<Statement> |
Default.body
Body.
|
protected ImmutableArray<Statement> |
Case.body
Body.
|
Modifier and Type | Method and Description |
---|---|
Statement |
LoopStatement.getBody()
Get body.
|
Statement |
Catch.getBody()
Get body.
|
Statement |
CatchAllStatement.getBody() |
Statement |
Finally.getBody()
Get body.
|
Statement |
LabeledStatement.getBody()
Get body.
|
Statement |
Then.getBody()
The body may be empty (null), to define a fall-through.
|
Statement |
Else.getBody()
The body may be empty (null), to define a fall-through.
|
Statement |
Ccatch.getBody()
Get body.
|
Statement |
MethodBodyStatement.getBody(Services services)
Get method body.
|
Statement |
LoopStatement.getStatementAt(int index) |
Statement |
Catch.getStatementAt(int index) |
Statement |
Exec.getStatementAt(int index)
Return the statement at the specified index in this node's "virtual"
statement array.
|
Statement |
LoopScopeBlock.getStatementAt(int index)
Return the statement at the specified index in this node's "virtual"
statement array.
|
Statement |
MethodFrame.getStatementAt(int index)
Return the statement at the specified index in this node's
"virtual" statement array.
|
Statement |
CatchAllStatement.getStatementAt(int i) |
Statement |
LoopInit.getStatementAt(int index) |
Statement |
Finally.getStatementAt(int index) |
Statement |
Default.getStatementAt(int index) |
Statement |
Try.getStatementAt(int index) |
Statement |
SynchronizedBlock.getStatementAt(int index) |
Statement |
LabeledStatement.getStatementAt(int index)
Return the statement at the specified index in this node's
"virtual" statement array.
|
Statement |
Then.getStatementAt(int index) |
Statement |
Else.getStatementAt(int index) |
Statement |
Ccatch.getStatementAt(int index) |
Statement |
Case.getStatementAt(int index) |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<Statement> |
Default.getBody()
The body may be empty (null), to define a fall-through.
|
ImmutableArray<Statement> |
Case.getBody()
The body may be empty (null), to define a fall-through.
|
Constructor and Description |
---|
Case(Expression e,
Statement[] body)
Case.
|
Default(Statement[] body)
Default.
|
Do(Expression guard,
Statement body,
ExtList l,
PositionInfo pos)
Do.
|
Do(Expression guard,
Statement body,
PositionInfo pos)
Do.
|
Else(Statement body)
Constructor for the transformation of COMPOST ASTs to KeY.
|
EnhancedFor(LoopInit init,
Guard guard,
Statement statement,
ExtList comments,
PositionInfo info)
Used for the Recoder2KeY transformation.
|
For(ILoopInit inits,
IGuard guard,
IForUpdates updates,
Statement body) |
For(ILoopInit inits,
IGuard guard,
IForUpdates updates,
Statement body,
ExtList comments) |
For(ILoopInit inits,
IGuard guard,
IForUpdates updates,
Statement body,
ExtList comments,
PositionInfo pos) |
For(LoopInitializer[] inits,
Expression guard,
Expression[] updates,
Statement body)
For.
|
LabeledStatement(Label id,
Statement statement,
PositionInfo pos)
Labeled statement.
|
LoopStatement(Expression guard,
Statement body)
Loop statement.
|
LoopStatement(Expression guard,
Statement body,
ExtList comments)
Loop statement.
|
LoopStatement(Expression guard,
Statement body,
ExtList comments,
PositionInfo pos) |
LoopStatement(Expression guard,
Statement body,
PositionInfo pos) |
LoopStatement(ILoopInit inits,
IGuard guard,
IForUpdates updates,
Statement body)
Loop statement.
|
LoopStatement(ILoopInit inits,
IGuard guard,
IForUpdates updates,
Statement body,
ExtList comments)
Loop statement.
|
LoopStatement(ILoopInit inits,
IGuard guard,
IForUpdates updates,
Statement body,
ExtList comments,
PositionInfo pos) |
LoopStatement(ILoopInit inits,
IGuard guard,
IForUpdates updates,
Statement body,
PositionInfo pos)
Loop statement.
|
LoopStatement(LoopInitializer[] inits,
Expression guard,
Expression[] updates,
Statement body)
Loop statement.
|
LoopStatement(Statement body)
Loop statement.
|
Then(Statement stmnt)
Constructor for the transformation of COMPOST ASTs to KeY.
|
While(Expression guard,
Statement body)
create a new While statement with no position info and no comments but guard and body set
|
While(Expression guard,
Statement body,
PositionInfo pos)
While.
|
While(Expression guard,
Statement body,
PositionInfo pos,
ExtList comments)
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 | Method and Description |
---|---|
Statement |
ProgramSV.getStatementAt(int i) |
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 Statement |
InitArray.createAssignment(ReferencePrefix p_array,
int p_index,
Expression p_initializer,
KeYJavaType p_elementType,
TypeReference p_baseType)
Convert one variable initializers to an assignment to the
appropriate array element (the initializer may itself be an
array initializer, in which case a valid creation expression is
created by inserting the new-operator)
|
Statement |
ProgramTransformer.getStatementAt(int index) |
Statement |
ReplaceWhileLoop.getTheLoop() |
protected Statement |
MethodCall.makeIfCascade(ImmutableList<KeYJavaType> imps,
Services services)
TODO
|
Modifier and Type | Method and Description |
---|---|
protected java.util.List<Statement> |
ConstructorCall.constructorCallSequence(New constructorReference,
KeYJavaType classType,
SVInstantiations svInst,
Services services)
returns a sequence of statements modelling the Java constructor call
semantics explicitly
|
Modifier and Type | Method and Description |
---|---|
protected void |
InitArray.createArrayAssignments(int p_start,
Statement[] p_statements,
ProgramVariable[] p_initializers,
ReferencePrefix p_array,
NewArray p_creationExpression)
Convert the variable initializers to assignments to the array
elements (the initializers may itself be array initializers, in
which case valid creation expressions are created by inserting
the new-operator)
|
protected ProgramVariable[] |
InitArray.evaluateInitializers(Statement[] p_stmnts,
NewArray p_creationExpression,
Services services)
The variable initializers have to be evaluated and assigned to
temporary variables (the initializers may itself be array
initializers, in which case valid creation expressions are
created by inserting the new-operator)
|
Constructor and Description |
---|
ExpandMethodBody(Statement mb) |
ForToWhile(SchemaVariable innerLabel,
SchemaVariable outerLabel,
Statement loop)
creates an loop to while - ProgramTransformer
|
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<ProgramVariable> |
JMLSpecFactory.collectLocalVariablesVisibleTo(Statement statement,
IProgramMethod method) |
Modifier and Type | Method and Description |
---|---|
protected boolean |
ProgramMethodSubsetPO.endsWithReturn(Statement[] statements)
Checks if the last statement is a
Return statement. |
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 . |
Copyright © 2003-2019 The KeY-Project.