public abstract class KeYJavaASTFactory
extends java.lang.Object
Constructor and Description |
---|
KeYJavaASTFactory() |
Modifier and Type | Method and Description |
---|---|
static ArrayReference |
arrayFieldAccess(ReferencePrefix array,
Expression index)
Create an array field access with a single index.
|
static ArrayInitializer |
arrayInitializer(Expression[] expressions,
KeYJavaType type)
Create an array initializer.
|
static FieldReference |
arrayLength(JavaInfo model,
ReferencePrefix array)
Create an array length access.
|
static CopyAssignment |
assign(Expression lhs,
Expression rhs)
creates an assignment
lhs:=rhs |
static CopyAssignment |
assign(Expression lhs,
Expression rhs,
PositionInfo posInfo)
creates an assignment
lhs:=rhs |
static CopyAssignment |
assign(ExtList parameters)
Create an assignment.
|
static CopyAssignment |
assignArrayField(ProgramVariable variable,
ReferencePrefix array,
Expression index)
Create a statement that assigns an array element to a variable.
|
static Expression |
attribute(ReferencePrefix prefix,
ProgramVariable field)
creates an attribute access
prefix.field |
static StatementBlock |
block(ExtList statements)
Create a block from an arbitrary number of statements.
|
static StatementBlock |
block(java.util.List<Statement> statements)
Create a block from an arbitrary number of statements.
|
static StatementBlock |
block(Statement... statements)
Create a block from an arbitrary number of statements.
|
static Break |
breakStatement(Label l)
Create a break statement.
|
static Statement |
breakStatement(Label label,
PositionInfo positionInfo) |
static Case |
caseBlock(Expression expression,
Statement statement)
Create a case block.
|
static Case |
caseBlock(Expression expression,
Statement[] statements)
Create a case block.
|
static Case |
caseBlock(ExtList parameters,
Expression expression,
PositionInfo position)
Create a case block.
|
static TypeCast |
cast(Expression expression,
KeYJavaType targetType) |
static Catch |
catchClause(ExtList parameters)
Create a catch clause.
|
static Catch |
catchClause(JavaInfo javaInfo,
java.lang.String param,
KeYJavaType kjt,
StatementBlock body)
Create a catch clause.
|
static Catch |
catchClause(JavaInfo javaInfo,
java.lang.String param,
java.lang.String type,
StatementBlock body)
Create a catch clause.
|
static Catch |
catchClause(ParameterDeclaration parameter,
Statement[] statements)
Create a catch clause.
|
static Catch |
catchClause(ParameterDeclaration param,
StatementBlock body)
create a catch clause
|
static Continue |
continueStatement(Label label) |
static LocalVariableDeclaration |
declare(ExtList parameters)
Create a local variable declaration without initialization.
|
static LocalVariableDeclaration |
declare(ImmutableArray<Modifier> modifiers,
IProgramVariable variable,
Expression init,
KeYJavaType type)
Create a local variable declaration with an arbitrary number of
modifiers.
|
static ProgramElement |
declare(ImmutableArray<Modifier> modifiers,
IProgramVariable variable,
Expression init,
ProgramElementName typeName,
int dimensions,
ReferencePrefix typePrefix,
KeYJavaType baseType)
Create a local array variable declaration with an arbitrary number of
modifiers.
|
static LocalVariableDeclaration |
declare(ImmutableArray<Modifier> modifiers,
IProgramVariable variable,
Expression init,
TypeReference typeRef)
Create a local variable declaration with an arbitrary number of
modifiers.
|
static LocalVariableDeclaration |
declare(ImmutableArray<Modifier> modifiers,
TypeReference typeRef,
VariableSpecification specification)
Create a local variable declaration.
|
static LocalVariableDeclaration |
declare(ImmutableArray<Modifier> modifiers,
TypeReference typeRef,
VariableSpecification[] specifications)
Create local variable declarations.
|
static LocalVariableDeclaration |
declare(IProgramVariable variable)
Create a local variable declaration without initialization.
|
static LocalVariableDeclaration |
declare(IProgramVariable variable,
Expression init)
Create a local variable declaration.
|
static LocalVariableDeclaration |
declare(IProgramVariable var,
Expression init,
KeYJavaType type)
Create a local variable declaration.
|
static LocalVariableDeclaration |
declare(IProgramVariable var,
KeYJavaType type)
Create a local variable declaration without initialization.
|
static LocalVariableDeclaration |
declare(Modifier[] modifiers,
IProgramVariable variable,
Expression init,
KeYJavaType type)
Create a local variable declaration with an arbitrary number of
modifiers.
|
static LocalVariableDeclaration |
declare(Modifier modifier,
IProgramVariable variable,
Expression init,
KeYJavaType type)
Create a local variable declaration with a single modifier.
|
static LocalVariableDeclaration |
declare(ProgramElementName name,
Expression init,
KeYJavaType type)
create a local variable declaration
type name = init; |
static LocalVariableDeclaration |
declare(ProgramElementName name,
KeYJavaType type)
Create a local variable declaration without initialization.
|
static LocalVariableDeclaration |
declare(ProgramElementName name,
TypeReference typeRef)
creates a local variable declaration
typeRef name; |
static LocalVariableDeclaration |
declare(Services services,
java.lang.String name,
Expression initializer,
KeYJavaType type)
Create a local variable declaration with a unique name.
|
static LocalVariableDeclaration |
declare(java.lang.String name,
KeYJavaType type)
create a local variable declaration
|
static LocalVariableDeclaration |
declareMethodCall(IProgramVariable variable,
ReferencePrefix reference,
java.lang.String method)
Create a local variable declaration that assigns a method's return value
initially.
|
static LocalVariableDeclaration |
declareMethodCall(KeYJavaType type,
IProgramVariable variable,
ReferencePrefix reference,
java.lang.String method)
Create a local variable declaration that assigns a method's return value
initially.
|
static LocalVariableDeclaration |
declareZero(KeYJavaType type,
IProgramVariable variable)
Create a local variable declaration that assigns zero initially.
|
static Default |
defaultBlock(ExtList parameters)
Create a default block.
|
static Default |
defaultBlock(Statement statement)
Create a default block.
|
static Default |
defaultBlock(Statement[] statements)
Create a default block.
|
static Do |
doLoop(Expression condition,
Statement statement,
PositionInfo positionInfo)
Create a do loop.
|
static Else |
elseBlock(ExtList parameters)
Create an else block.
|
static Else |
elseBlock(Statement statement)
Create an else block.
|
static Else |
elseBlock(Statement[] statements)
Create an else block.
|
static EmptyStatement |
emptyStatement()
Create an empty statement.
|
static EnhancedFor |
enhancedForLoop(ExtList parameters)
Create an enhanced for loop.
|
static Equals |
equalsNullOperator(Expression expression)
Create an equality comparison with
null . |
static Equals |
equalsOperator(Expression left,
Expression right)
Create an equals operator.
|
static Equals |
equalsOperator(ExtList operands)
Create an equals operator.
|
static ExecutionContext |
executionContext(KeYJavaType classType,
IProgramMethod method,
ReferencePrefix reference)
Create an execution context.
|
static BooleanLiteral |
falseLiteral()
Create a literal for the truth value
false . |
static FieldReference |
fieldReference(ReferencePrefix prefix,
ProgramVariable field)
Create a field access.
|
static FieldReference |
fieldReference(Services services,
java.lang.String name,
Expression expression,
ExecutionContext context)
Create a field access.
|
static Finally |
finallyBlock(ExtList parameters)
Create a finally block.
|
static Finally |
finallyBlock(Statement statement)
Create a finally block.
|
static Finally |
finallyBlock(Statement[] statements)
Create a finally block.
|
static Finally |
finallyBlock(StatementBlock body)
Create a finally block.
|
static For |
forLoop(ExtList parameters)
Create a for loop.
|
static For |
forLoop(IGuard guard,
IForUpdates updates,
Statement body)
Create a for loop with no initializer.
|
static For |
forLoop(IGuard guard,
IForUpdates updates,
Statement[] body)
Create a for loop with no initializer.
|
static For |
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 IForUpdates |
forUpdates(Expression update)
Create a list of loop updates that consists of a single expression.
|
static Statement |
ifElse(Expression guard,
Statement thenStatement,
Statement elseStatement)
Create an if clause.
|
static If |
ifElse(Expression guard,
Then then,
Else els)
Create an if statement including an else branch.
|
static If |
ifStatement(ExtList parameters)
Create an if statement.
|
static If |
ifThen(Expression guard,
Statement... statements)
Create an if statement with no else branch.
|
static If |
ifThen(Expression guard,
Statement then)
Create an if statement with no else branch.
|
static If |
ifThen(Expression guard,
Then then)
Create an if statement with no else branch.
|
static StatementBlock |
insertStatementInBlock(Statement[] stmnt,
StatementBlock b)
inserts the given statements at the begin of the block
|
static StatementBlock |
insertStatementInBlock(StatementBlock block,
Statement[] statements)
Create a block where the given statements come after the given block.
|
static StatementBlock |
insertStatementInBlock(StatementBlock stmnt,
StatementBlock b)
inserts the given statements at the begin of the block
|
static StatementBlock |
insertStatementInBlock(Statement statement,
StatementBlock block)
Insert a statement in a block of statements.
|
static Instanceof |
instanceOf(Expression expression,
KeYJavaType type)
Create an instance of operator.
|
static IntLiteral |
intLiteral(java.lang.Integer value)
Create an integer literal.
|
static LabeledStatement |
labeledStatement(ExtList parameters,
Label label,
PositionInfo position)
Create a labeled statement.
|
static Statement |
labeledStatement(Label label,
Statement[] statements,
PositionInfo pos)
Create a labeled block of statements.
|
static LabeledStatement |
labeledStatement(Label label,
Statement statement,
PositionInfo pos)
Create a labeled statement.
|
static IGuard |
lessThanArrayLengthGuard(JavaInfo model,
ProgramVariable variable,
ReferencePrefix array)
Create a condition that compares a variable and an array length using the
less than operator.
|
static IGuard |
lessThanGuard(Expression left,
Expression right)
Create a condition that compares two expressions using the less than
operator.
|
static LessThan |
lessThanOperator(Expression left,
Expression right)
Create a less than operator.
|
static LessThan |
lessThanZeroOperator(Expression expression)
Create a less than zero operator.
|
static ProgramVariable |
localVariable(ProgramElementName name,
KeYJavaType kjt)
create a local variable
|
static ProgramVariable |
localVariable(Services services,
java.lang.String name,
KeYJavaType type)
Create a local variable with a unique name.
|
static ProgramVariable |
localVariable(java.lang.String name,
KeYJavaType kjt)
create a local variable
|
static LogicalAnd |
logicalAndOperator(Expression left,
Expression right)
Create a logical and operator.
|
static LogicalOr |
logicalOrOperator(Expression left,
Expression right)
Create a logical or operator.
|
static ILoopInit |
loopInit(LoopInitializer init)
Create a loop initialization that consists of a single statement.
|
static ILoopInit |
loopInitZero(KeYJavaType type,
IProgramVariable variable)
Create a loop initialization that declares and assigns zero to a local
variable.
|
static MethodBodyStatement |
methodBody(JavaInfo model,
ProgramVariable result,
ReferencePrefix reference,
KeYJavaType classType,
java.lang.String methodName,
ProgramVariable[] arguments)
Create a method body shortcut.
|
static MethodBodyStatement |
methodBody(ProgramVariable result,
ReferencePrefix reference,
IProgramMethod method,
Expression[] arguments)
Create a method body shortcut.
|
static MethodBodyStatement |
methodBody(ProgramVariable result,
ReferencePrefix reference,
IProgramMethod method,
ImmutableArray<Expression> arguments)
Create a method body shortcut.
|
static MethodReference |
methodCall(KeYJavaType type,
java.lang.String name)
Create a method call on a type with no arguments.
|
static MethodReference |
methodCall(KeYJavaType type,
java.lang.String name,
Expression... args)
Create a method call on a type.
|
static MethodReference |
methodCall(KeYJavaType type,
java.lang.String name,
ImmutableArray<? extends Expression> args)
Create a method call on a type.
|
static MethodReference |
methodCall(ReferencePrefix reference,
MethodName name,
Expression... args)
Create a method call.
|
static MethodReference |
methodCall(ReferencePrefix reference,
MethodName name,
ImmutableArray<? extends Expression> args)
Create a method call.
|
static MethodReference |
methodCall(ReferencePrefix reference,
java.lang.String name)
Create a method call with no arguments.
|
static MethodReference |
methodCall(ReferencePrefix reference,
java.lang.String name,
Expression... args)
Create a method call.
|
static MethodReference |
methodCall(ReferencePrefix reference,
java.lang.String name,
ImmutableArray<? extends Expression> args)
Create a method call.
|
static MethodFrame |
methodFrame(IExecutionContext executionContext,
StatementBlock block)
Create a method call substitution.
|
static MethodFrame |
methodFrame(IExecutionContext executionContext,
StatementBlock block,
PositionInfo position)
Create a method call substitution at a specific source position.
|
static MethodFrame |
methodFrame(IProgramVariable result,
IExecutionContext executionContext,
StatementBlock block)
Create a method call substitution with a return value assignment.
|
static MethodFrame |
methodFrame(IProgramVariable result,
IExecutionContext executionContext,
StatementBlock block,
PositionInfo position)
Create a method call substitution with a return value assignment at a
specific source position.
|
static NewArray |
newArray(TypeReference typeRef,
int dimensions,
ArrayInitializer initializer,
KeYJavaType keyJavaType)
Create an array instantiation.
|
static NewArray |
newArray(TypeReference typeRef,
int dimensions,
Expression[] sizes,
ArrayInitializer initializer,
KeYJavaType keyJavaType)
Create an array instantiation.
|
static NewArray |
newArray(TypeReference typeRef,
int dimensions,
Expression[] sizes,
KeYJavaType keyJavaType)
Create an array instantiation.
|
static NewArray |
newArray(TypeReference typeRef,
int dimensions,
Expression size,
KeYJavaType keyJavaType)
Create an array instantiation.
|
static New |
newOperator(KeYJavaType type)
Create an object allocation without arguments.
|
static New |
newOperator(ReferencePrefix referencePrefix,
KeYJavaType type)
Create an object allocation without arguments.
|
static New |
newOperator(ReferencePrefix referencePrefix,
KeYJavaType type,
Expression[] args)
Create an object allocation.
|
static New |
newOperator(ReferencePrefix referencePrefix,
TypeReference typeReference,
Expression[] args)
Create an object allocation.
|
static NotEquals |
notEqualsOperator(ExtList operands)
Create an unequal operator.
|
static ParameterDeclaration |
parameterDeclaration(JavaInfo javaInfo,
KeYJavaType kjt,
IProgramVariable var)
Create a parameter declaration.
|
static ParameterDeclaration |
parameterDeclaration(JavaInfo javaInfo,
KeYJavaType kjt,
java.lang.String name)
create a parameter declaration
|
static ParameterDeclaration |
parameterDeclaration(JavaInfo javaInfo,
java.lang.String type,
java.lang.String name) |
static ParenthesizedExpression |
parenthesizedExpression(Expression expression)
Create a parenthesized expression.
|
static PassiveExpression |
passiveExpression(Expression expression)
Create an inactive expression.
|
static IForUpdates |
postIncrementForUpdates(ProgramVariable variable)
Create a loop update expression that post increments a given variable.
|
static Return |
returnClause(Expression e)
Create a return clause.
|
static SuperConstructorReference |
superConstructor(ReferencePrefix referencePrefix,
Expression[] args)
Create a call to the super constructor.
|
static SuperReference |
superReference()
Create a reference to
super . |
static Switch |
switchBlock(Expression expression,
Branch[] branches)
Create a switch block.
|
static Switch |
switchBlock(ExtList parameters)
Create a switch block.
|
static SynchronizedBlock |
synchronizedBlock(ExtList parameters)
Create a synchronized block.
|
static Then |
thenBlock(ExtList parameters)
Create a then block.
|
static Then |
thenBlock(Statement statement)
Create a then block.
|
static Then |
thenBlock(Statement[] statements)
Create a then block.
|
static ThisConstructorReference |
thisConstructor(Expression[] args)
Create a call to a constructor of the current class.
|
static ThisReference |
thisReference()
Create a reference to
this . |
static Throw |
throwClause(Expression e)
Create a throw clause.
|
static TransactionStatement |
transactionStatement(int type)
Create a transaction statement.
|
static Guard |
trueGuard()
Create a
true condition. |
static BooleanLiteral |
trueLiteral()
Create a literal for the truth value
true . |
static Try |
tryBlock(ExtList parameters)
Create a try block.
|
static Try |
tryBlock(StatementBlock body,
Branch[] branches)
Create a try block.
|
static Try |
tryBlock(Statement statement,
Branch branch)
Create a try block.
|
static Try |
tryBlock(Statement statement,
Branch[] branches)
Create a try block.
|
static TypeRef |
typeRef(KeYJavaType type)
Create a type reference.
|
static TypeRef |
typeRef(KeYJavaType type,
int dimensions)
Create a type reference.
|
static VariableSpecification |
variableSpecification(IProgramVariable variable,
Expression initializer,
KeYJavaType keyJavaType)
Create a variable specification.
|
static VariableSpecification |
variableSpecification(IProgramVariable variable,
int dimensions,
Expression initializer,
Type type)
Create a variable specification.
|
static Statement |
whileLoop(Expression condition,
Statement body)
Create a while loop.
|
static While |
whileLoop(Expression condition,
Statement body,
PositionInfo position)
Create a while loop at a specific source position.
|
static IntLiteral |
zeroLiteral()
Create a literal for the integer zero.
|
public static CopyAssignment assign(Expression lhs, Expression rhs)
lhs:=rhs
public static CopyAssignment assign(Expression lhs, Expression rhs, PositionInfo posInfo)
lhs:=rhs
public static CopyAssignment assign(ExtList parameters)
parameters
- the assignment parameters (variable, expression) as
ExtList
CopyAssignment
as defined by
parameters
public static Expression attribute(ReferencePrefix prefix, ProgramVariable field)
prefix.field
public static LocalVariableDeclaration declare(ProgramElementName name, TypeReference typeRef)
typeRef name;
public static LocalVariableDeclaration declare(ProgramElementName name, KeYJavaType type)
type name;
name
- the ProgramElementName
of the variable to be declaredtype
- the static KeYJavaType
of the variable to be declaredLocalVariableDeclaration
of a variable with static
type type
and name name
public static LocalVariableDeclaration declare(ProgramElementName name, Expression init, KeYJavaType type)
type name = init;
public static LocalVariableDeclaration declare(IProgramVariable var, Expression init, KeYJavaType type)
type var = init;
var
- the named and typed IProgramVariable
to be declaredinit
- the Expression
var
is initialized withtype
- the static KeYJavaType
of var
LocalVariableDeclaration
of var
with
static type type
and initial value init
public static LocalVariableDeclaration declare(Services services, java.lang.String name, Expression initializer, KeYJavaType type)
type name{unique} = initializer;
services
- the Services
whose VariableNamer
is used to
determine a unique variable namename
- the String
on which the variable's unique name is
basedinitializer
- the Expression
the declared variable is initialized
withtype
- the static KeYJavaType
of the to be declared variableLocalVariableDeclaration
of variable named uniquely
after name
with static type type
and
initial value initializer
public static LocalVariableDeclaration declare(IProgramVariable var, KeYJavaType type)
type var;
var
- the named and typed IProgramVariable
to be declaredtype
- the static KeYJavaType
of var
LocalVariableDeclaration
of var
with
static type type
public static LocalVariableDeclaration declare(java.lang.String name, KeYJavaType type)
public static ParameterDeclaration parameterDeclaration(JavaInfo javaInfo, KeYJavaType kjt, java.lang.String name)
public static ParameterDeclaration parameterDeclaration(JavaInfo javaInfo, KeYJavaType kjt, IProgramVariable var)
kjt var
javaInfo
- the Java model containing kjt
kjt
- the static KeYJavaType
of var
var
- the named and typed IProgramVariable
to be declared as
parameterParameterDeclaration
of var
with static
type kjt
public static ParameterDeclaration parameterDeclaration(JavaInfo javaInfo, java.lang.String type, java.lang.String name)
public static ParenthesizedExpression parenthesizedExpression(Expression expression)
(expression)
expression
- the Expression
to be parenthesizedParenthesizedExpression
of expression
public static PassiveExpression passiveExpression(Expression expression)
expression
- the Expression
to be marked inactivePassiveExpression
version of
expression
public static ProgramVariable localVariable(java.lang.String name, KeYJavaType kjt)
public static ProgramVariable localVariable(ProgramElementName name, KeYJavaType kjt)
public static ProgramVariable localVariable(Services services, java.lang.String name, KeYJavaType type)
services
- the Services
whose VariableNamer
is usedname
- the String
on which the variable's unique name is
basedtype
- the variable's static KeYJavaType
ProgramVariable
of static type type
and with a unique name based on name
public static LogicalAnd logicalAndOperator(Expression left, Expression right)
left & right
left
- the left operand Expression
right
- the right operand Expression
LogicalAnd
of left
and
right
public static LogicalOr logicalOrOperator(Expression left, Expression right)
left | right
left
- the left operand Expression
right
- the right operand Expression
LogicalOr
of left
and
right
public static Catch catchClause(ParameterDeclaration param, StatementBlock body)
public static Catch catchClause(ParameterDeclaration parameter, Statement[] statements)
catch (parameter) { statements }
parameter
- the to be caught ParameterDeclaration
statements
- the body Statement
sCatch
clause for execution of
statements
in case of parameter
public static Catch catchClause(JavaInfo javaInfo, java.lang.String param, KeYJavaType kjt, StatementBlock body)
catch (kjt param) body
javaInfo
- the JavaInfo
containing kjt
param
- the String
name of the exception object variablekjt
- the KeYJavaType
of the exception object variablebody
- the StatementBlock
catch clause bodyCatch
with parameter param
of static
type kjt
and body body
public static Catch catchClause(JavaInfo javaInfo, java.lang.String param, java.lang.String type, StatementBlock body)
catch (type param) body
javaInfo
- the JavaInfo
containing a KeYJavaType
named
type
param
- the String
name of the exception object variabletype
- the String
name of the exception object
variable's KeYJavaType
body
- the StatementBlock
catch clause bodyCatch
with parameter param
of static
type type
and body body
public static Throw throwClause(Expression e)
throw e
e
- the throw Expression
Throw
statement with expression e
public static TransactionStatement transactionStatement(int type)
type
- the transaction statement typeTransactionStatement
of type type
public static Guard trueGuard()
true
condition.Guard
with expression true
public static Statement whileLoop(Expression condition, Statement body)
while (condition) body
condition
- the loop condition Expression
body
- the loop body Statement
While
loop defined by condition
and
body
public static While whileLoop(Expression condition, Statement body, PositionInfo position)
while (condition) body
condition
- the loop condition Expression
body
- the loop body Statement
position
- the new source element's PositionInfo
While
loop defined by condition
and
body
, and positioned at position
public static Return returnClause(Expression e)
return e
e
- the return Expression
Return
statement with expression e
public static If ifThen(Expression guard, Statement then)
if (guard) then
guard
- the if statement condition Expression
then
- the if statement then branch Statement
If
with expression guard
and then branch
then
public static If ifThen(Expression guard, Statement... statements)
if (guard) { statements }
guard
- the if statement condition Expression
statements
- the if statement then branch Statement
sIf
with condition guard
and then branch
statements
public static If ifThen(Expression guard, Then then)
if (guard) then
guard
- the if statement condition Expression
then
- the if statement then branch Then
If
with expression guard
and then branch
then
public static If ifElse(Expression guard, Then then, Else els)
if (guard) then else els
guard
- the if statement condition Expression
then
- the if statement then branch Statement
els
- the if statement else branch Statement
If
with expression guard
, then branch
then
and else branch els
public static Statement ifElse(Expression guard, Statement thenStatement, Statement elseStatement)
if (guard) thenStatement else elseStatement
guard
- the if clause condition Expression
thenStatement
- the if clause then branch Statement
elseStatement
- the if clause else branch Statement
If
with condition guard
, then branch
thenStatement
and else branch
elseStatement
public static Statement breakStatement(Label label, PositionInfo positionInfo)
public static Case caseBlock(ExtList parameters, Expression expression, PositionInfo position)
parameters
- the case block parameters (body) as ExtList
expression
- the case block Expression
position
- the new source element's PositionInfo
Case
as defined by parameters
and
expression
public static Case caseBlock(Expression expression, Statement statement)
case (expression) statement
expression
- the case Expression
statement
- the to be executed Statement
Case
for execution of statement
in
case of expression
public static Case caseBlock(Expression expression, Statement[] statements)
case (expression) { statements }
expression
- the case Expression
statements
- the to be executed Statement
sCase
for execution of statements
in
case of expression
public static EmptyStatement emptyStatement()
EmptyStatement
public static EnhancedFor enhancedForLoop(ExtList parameters)
public static Equals equalsNullOperator(Expression expression)
null
.
expression == null
expression
- the Expression
to be compared against
null
Equals
that compares expression
against null
public static Equals equalsOperator(Expression left, Expression right)
left == right
left
- the left operand Expression
right
- the right operand Expression
Equals
of left
and right
public static Equals equalsOperator(ExtList operands)
operand{1} == operand{2}
public static ExecutionContext executionContext(KeYJavaType classType, IProgramMethod method, ReferencePrefix reference)
classType
- the enclosing class KeYJavaType
method
- the enclosing IProgramMethod
defined in
classType
reference
- the ReferencePrefix
method
is called onExecutionContext
for calls on
reference
to method
from
classType
public static StatementBlock insertStatementInBlock(Statement statement, StatementBlock block)
statement
- the Statement
to be inserted into block
block
- the StatementBlock
statement
is inserted
intoStatementBlock
that contains both the
Statement
s from block
and
statement
public static StatementBlock insertStatementInBlock(Statement[] stmnt, StatementBlock b)
stmnt
- array of Statement those have to be insertedb
- the Statementblock where to insertpublic static StatementBlock insertStatementInBlock(StatementBlock stmnt, StatementBlock b)
stmnt
- array of Statement those have to be insertedb
- the Statementblock where to insertpublic static StatementBlock insertStatementInBlock(StatementBlock block, Statement[] statements)
block statements
block
- the original StatementBlock
statements
- the inserted Statement
sStatementBlock
that contains
block
first and statements
secondpublic static Instanceof instanceOf(Expression expression, KeYJavaType type)
expression instance of type
expression
- the Expression
operand, whose runtime type is to be
checkedtype
- the KeYJavaType
operand expression
's type
is checked againstInstanceof
for checking expression
's
type against type
public static LocalVariableDeclaration declareZero(KeYJavaType type, IProgramVariable variable)
type variable = 0;
type
- the static KeYJavaType
of variable
variable
- the named and typed IProgramVariable
to be declaredLocalVariableDeclaration
of variable
with static type type
and initial value zeropublic static LocalVariableDeclaration declareMethodCall(KeYJavaType type, IProgramVariable variable, ReferencePrefix reference, java.lang.String method)
type variable = reference.method();
type
- the static KeYJavaType
of variable
variable
- the named and typed IProgramVariable
to be declaredreference
- the ReferencePrefix
the method is called onmethod
- the method's name String
LocalVariableDeclaration
of variable
with static type type
and initial value
reference.method()
public static LocalVariableDeclaration declareMethodCall(IProgramVariable variable, ReferencePrefix reference, java.lang.String method)
type variable = reference.method();where
type
is variable's KeYJavaType
as it is
returned by IProgramVariable.getKeYJavaType()
.variable
- the named and typed IProgramVariable
to be declaredreference
- the ReferencePrefix
the method is called onmethod
- the method's name String
LocalVariableDeclaration
of variable
with static type type
and initial value
reference.method()
public static Default defaultBlock(Statement statement)
default statement
public static Default defaultBlock(Statement[] statements)
default { statements }
public static Do doLoop(Expression condition, Statement statement, PositionInfo positionInfo)
do statement while (condition);
condition
- the do-loop condition Expression
statement
- the do-loop body Statement
positionInfo
- the new source element's PositionInfo
Do
that executes statement
while
condition
holdspublic static Else elseBlock(Statement[] statements)
else { statements }
public static ILoopInit loopInit(LoopInitializer init)
init
init
- the single LoopInitializer
ILoopInit
that consists of init
onlypublic static ILoopInit loopInitZero(KeYJavaType type, IProgramVariable variable)
type variable = 0
type
- the static KeYJavaType
of variable
variable
- the named and typed IProgramVariable
to be declaredILoopInit
that declares variable
variable
with static type type
and
initial value zeropublic static ArrayInitializer arrayInitializer(Expression[] expressions, KeYJavaType type)
expressions
- the initial value Expression
stype
- the array type KeYJavaType
ArrayInitializer
which contains
expressions
and is of type type
public static FieldReference arrayLength(JavaInfo model, ReferencePrefix array)
array.length
model
- the JavaInfo
to retrieve the array super class type,
which holds the length attribute, fromarray
- the ReferencePrefix
whose length attribute is accessedFieldReference
for array
's length
attributepublic static IGuard lessThanGuard(Expression left, Expression right)
left < right
left
- the Expression
to be compared less than
right
right
- the Expression
to be compared greater than
left
Guard
that compares left
less than
right
public static LessThan lessThanOperator(Expression left, Expression right)
left < right
left
- the left operand Expression
right
- the right operand Expression
LessThan
that compares left
less than
right
public static LessThan lessThanZeroOperator(Expression expression)
expression < 0
expression
- the left operand Expression
LessThan
that compares expression
less
than 0
public static IGuard lessThanArrayLengthGuard(JavaInfo model, ProgramVariable variable, ReferencePrefix array)
variable < array.length
model
- the JavaInfo
to retrieve the array super class type,
which holds the length attribute, fromvariable
- the ProgramVariable
to be compared less than
array
's lengtharray
- the ReferencePrefix
whose length attribute is accessedGuard
that compares variable
less than
array
's lengthpublic static IForUpdates forUpdates(Expression update)
update
update
- the single update Expression
ForUpdates
that consists of update
onlypublic static IForUpdates postIncrementForUpdates(ProgramVariable variable)
variable++
variable
- the ProgramVariable
to be post incremented during the
loop updatesForUpdates
that consists of the post increment of
variable
public static ArrayReference arrayFieldAccess(ReferencePrefix array, Expression index)
array[index]
array
- the ReferencePrefix
to be accessedindex
- the array access index Expression
ArrayReference
for access of array
at
index
public static StatementBlock block(ExtList statements)
statements
- the block statements as ExtList
StatementBlock
consisting of
statements
public static StatementBlock block(Statement... statements)
{ statements; }
statements
- the Statement
s to appear in the blockStatementBlock
that consists of the given
statements
in the very same orderpublic static StatementBlock block(java.util.List<Statement> statements)
{ statements; }
statements
- the Statement
s to appear in the blockStatementBlock
that consists of the given
statements
in the very same orderpublic static For forLoop(ILoopInit init, IGuard guard, IForUpdates updates, Statement... statements)
for (init; guard; updates) { statements; }
init
- the ILoopInit
loop initializationsguard
- the IGuard
loop conditionupdates
- the IForUpdates
loop updatesstatements
- the body Statement
sFor
with initializers init
, condition
guard
, updates updates
and body
statements
public static For forLoop(IGuard guard, IForUpdates updates, Statement body)
for (; guard; updates) body
guard
- the IGuard
loop conditionupdates
- the IForUpdates
loop updatesbody
- the body Statement
For
with condition guard
, updates
updates
and body body
public static For forLoop(IGuard guard, IForUpdates updates, Statement[] body)
for (; guard; updates) body
guard
- the IGuard
loop conditionupdates
- the IForUpdates
loop updatesbody
- the body Statement
sFor
with condition guard
, updates
updates
and body body
public static CopyAssignment assignArrayField(ProgramVariable variable, ReferencePrefix array, Expression index)
variable = array[index];
variable
- the ProgramVariable
to be assigned toarray
- the array ReferencePrefix
to be accessedindex
- the array access index Expression
CopyAssignment
of array
element at
index
to variable
public static LocalVariableDeclaration declare(ExtList parameters)
parameters
- the declaration parameters (modifiers, type reference,
variable specifications) as ExtList
LocalVariableDeclaration
as defined by
parameters
public static LocalVariableDeclaration declare(IProgramVariable variable)
type variable;where
type
is variable
's KeYJavaType
as
it is returned by IProgramVariable.getKeYJavaType()
.variable
- the named and typed IProgramVariable
to be declaredLocalVariableDeclaration
of variable
public static LocalVariableDeclaration declare(IProgramVariable variable, Expression init)
type variable = init;where
type
is variable
's KeYJavaType
as
it is returned by IProgramVariable.getKeYJavaType()
.variable
- the named and typed IProgramVariable
to be declaredinit
- the Expression
variable
is initialized
withLocalVariableDeclaration
of variable
public static LocalVariableDeclaration declare(Modifier modifier, IProgramVariable variable, Expression init, KeYJavaType type)
modifier type variable = init;
modifier
- the Modifier
variable
- the named and typed IProgramVariable
to be declaredinit
- the Expression
variable
is initialized
withtype
- the static KeYJavaType
of variable
LocalVariableDeclaration
of variable
with static type type
and initial value
init
public static LocalVariableDeclaration declare(Modifier[] modifiers, IProgramVariable variable, Expression init, KeYJavaType type)
modifiers type variable = init;
modifiers
- the Modifier
svariable
- the named and typed IProgramVariable
to be declaredinit
- the Expression
variable
is initialized
withtype
- the static KeYJavaType
of variable
LocalVariableDeclaration
of variable
with static type type
and initial value
init
public static LocalVariableDeclaration declare(ImmutableArray<Modifier> modifiers, IProgramVariable variable, Expression init, KeYJavaType type)
modifiers type variable = init;
modifiers
- the Modifier
svariable
- the named and typed IProgramVariable
to be declaredinit
- the Expression
variable
is initialized
withtype
- the static KeYJavaType
of variable
LocalVariableDeclaration
of variable
with static type type
and initial value
init
public static LocalVariableDeclaration declare(ImmutableArray<Modifier> modifiers, IProgramVariable variable, Expression init, TypeReference typeRef)
modifiers typeRef variable = init;
modifiers
- the Modifier
svariable
- the named and typed IProgramVariable
to be declaredinit
- the Expression
variable
is initialized
withtypeRef
- the static TypeRef
of variable
LocalVariableDeclaration
of variable
with static type typeRef
and initial value
init
public static LocalVariableDeclaration declare(ImmutableArray<Modifier> modifiers, TypeReference typeRef, VariableSpecification specification)
modifiers typeRef specification
modifiers
- the Modifier
stypeRef
- the static TypeRef
of the variable to be declaredspecification
- the VariableSpecification
of the variable to be
declaredLocalVariableDeclaration
of the variable specified
by specification
with static type
typeRef
public static LocalVariableDeclaration declare(ImmutableArray<Modifier> modifiers, TypeReference typeRef, VariableSpecification[] specifications)
modifiers typeRef specification{1}, ...
modifiers
- the Modifier
stypeRef
- the static TypeRef
of the variable to be declaredspecifications
- the VariableSpecification
s of the variables to be
declaredLocalVariableDeclaration
of the variables specified
by specifications
with static type
typeRef
public static MethodReference methodCall(ReferencePrefix reference, java.lang.String name, ImmutableArray<? extends Expression> args)
reference.name(args);
reference
- the ReferencePrefix
the method is called onname
- the method's name String
args
- the argument Expression
s to be passed to the methodMethodReference
for call of method
name
on reference
with arguments
args
public static MethodReference methodCall(KeYJavaType type, java.lang.String name, ImmutableArray<? extends Expression> args)
type.name(args);
type
- the KeYJavaType
the method is called onname
- the method's name String
args
- the argument Expression
s to be passed to the methodMethodReference
for call of method
name
on type
with arguments
args
public static MethodReference methodCall(KeYJavaType type, java.lang.String name, Expression... args)
type.name(args);
type
- the KeYJavaType
the method is called onname
- the method's name String
args
- the argument Expression
s to be passed to the methodMethodReference
for call of method
name
on type
with arguments
args
public static MethodReference methodCall(KeYJavaType type, java.lang.String name)
type.name();
type
- the KeYJavaType
the method is called onname
- the method's name String
MethodReference
for call of method
name
on type
with arguments
args
public static MethodReference methodCall(ReferencePrefix reference, java.lang.String name)
reference.name();
reference
- the ReferencePrefix
the method is called onname
- the method's name String
MethodReference
for call of method
name
on reference
with no argumentspublic static MethodReference methodCall(ReferencePrefix reference, java.lang.String name, Expression... args)
reference.name(args);
reference
- the ReferencePrefix
the method is called onname
- the method's name String
args
- the argument Expression
s to be passed to the methodMethodReference
for call of method
name
on reference
with arguments
args
public static MethodReference methodCall(ReferencePrefix reference, MethodName name, Expression... args)
reference.name(args);
reference
- the ReferencePrefix
the method is called onname
- the MethodName
args
- the argument Expression
s to be passed to the methodMethodReference
for call of method
name
on reference
with arguments
args
public static MethodReference methodCall(ReferencePrefix reference, MethodName name, ImmutableArray<? extends Expression> args)
reference.name(args);
reference
- the ReferencePrefix
the method is called onname
- the MethodName
args
- the argument Expression
s to be passed to the methodMethodReference
for call of method
name
on reference
with arguments
args
public static FieldReference fieldReference(Services services, java.lang.String name, Expression expression, ExecutionContext context)
(expression).name
services
- the Services
to determine both expression
's KeYJavaType
and the ProgramVariable
corresponding to the field name
name
- the to be accessed field's name String
expression
- the Expression
on which the field is accessedcontext
- the ExecutionContext
, which is needed to determine
expression
's KeYJavaType
FieldReference
of field name
on
expression
public static FieldReference fieldReference(ReferencePrefix prefix, ProgramVariable field)
prefix.field
prefix
- the ReferencePrefix
on which field
is
accessedfield
- the ProgramVariable
to be accessedFieldReference
of field
on
prefix
public static Finally finallyBlock(Statement statement)
finally statement
public static Finally finallyBlock(Statement[] statements)
finally { statements }
public static Finally finallyBlock(StatementBlock body)
finally body
body
- the StatementBlock
to be executedFinally
block consisting of body
solelypublic static ProgramElement declare(ImmutableArray<Modifier> modifiers, IProgramVariable variable, Expression init, ProgramElementName typeName, int dimensions, ReferencePrefix typePrefix, KeYJavaType baseType)
modifiers typePrefix.baseType[] variable = init;
modifiers
- the Modifiers
variable
- the named and typed IProgramVariable
to be declaredinit
- the Expression
variable
is initialized
withtypeName
- the type's ProgramElementName
dimensions
- the type's dimensionstypePrefix
- the type's ReferencePrefix
baseType
- the base KeYJavaType
LocalVariableDeclaration
of variable
with static type baseType[dimensions]
and initial
value init
public static MethodBodyStatement methodBody(JavaInfo model, ProgramVariable result, ReferencePrefix reference, KeYJavaType classType, java.lang.String methodName, ProgramVariable[] arguments)
classType
is also used as visibility context when
looking for methodName
in its definition.model
- the JavaInfo
that contains
classType.methodName
result
- the ProgramVariable
the return value is assigned to or
null
reference
- the ReferencePrefix
invocation targetclassType
- the KeYJavaType
in which the method is declaredmethodName
- the method's String
namearguments
- the ProgramVariable
and their static types the
method is called withMethodBodyStatement
for
classType.methodName
when called with
arguments
or null
when the former is
not definedpublic static MethodBodyStatement methodBody(ProgramVariable result, ReferencePrefix reference, IProgramMethod method, Expression[] arguments)
result
- the ProgramVariable
the return value is assigned to or
null
reference
- the ReferencePrefix
invocation targetmethod
- the IProgramMethod
referencearguments
- the Expression
s and their static types the method
is called withMethodBodyStatement
for method
when
called with arguments
public static MethodBodyStatement methodBody(ProgramVariable result, ReferencePrefix reference, IProgramMethod method, ImmutableArray<Expression> arguments)
result
- the ProgramVariable
the return value is assigned to or
null
reference
- the ReferencePrefix
invocation targetmethod
- the IProgramMethod
referencearguments
- the Expression
s and their static types the method
is called withMethodBodyStatement
for method
when
called with arguments
public static MethodFrame methodFrame(IExecutionContext executionContext, StatementBlock block)
executionContext
- the block
's IExecutionContext
block
- the StatementBlock
to be put in executionContext
MethodFrame
that associates block
with
executionContext
public static MethodFrame methodFrame(IExecutionContext executionContext, StatementBlock block, PositionInfo position)
executionContext
- the block
's IExecutionContext
block
- the StatementBlock
to be put in
executionContext
position
- the new source element's PositionInfo
MethodFrame
that associates block
with
executionContext
and positions it at
position
public static MethodFrame methodFrame(IProgramVariable result, IExecutionContext executionContext, StatementBlock block)
result
- the IProgramVariable
block
's return value
is assigned toexecutionContext
- the block
's IExecutionContext
block
- the StatementBlock
to be put in
executionContext
MethodFrame
that associates block
with
executionContext
public static MethodFrame methodFrame(IProgramVariable result, IExecutionContext executionContext, StatementBlock block, PositionInfo position)
result
- the IProgramVariable
block
's return value
is assigned toexecutionContext
- the block
's IExecutionContext
block
- the StatementBlock
to be put in
executionContext
position
- the new source element's PositionInfo
MethodFrame
that associates block
with
executionContext
and positions it at
position
public static IntLiteral intLiteral(java.lang.Integer value)
value
- the Integer
to be turned into an literalIntLiteral
representing value
public static LabeledStatement labeledStatement(ExtList parameters, Label label, PositionInfo position)
parameters
- the parameters (statement) as ExtList
label
- the Label
position
- the new source element's PositionInfo
LabeledStatement
as defined by
parameters
and label
public static LabeledStatement labeledStatement(Label label, Statement statement, PositionInfo pos)
label: statement
label
- the Label
statement
- the Statement
to be labeledLabeledStatement
that adds label
to
statement
public static Statement labeledStatement(Label label, Statement[] statements, PositionInfo pos)
label: { statements }
label
- the Label
statements
- the Statement
s to be labeledLabeledStatement
that adds label
to
statements
public static NewArray newArray(TypeReference typeRef, int dimensions, Expression[] sizes, ArrayInitializer initializer, KeYJavaType keyJavaType)
new typeRef[sizes{1}]...[sizes{dimensions}] initializer
sizes
- the size Expression
s for each dimensiontypeRef
- the static array base typekeyJavaType
- the array element typeinitializer
- the ArrayInitializer
dimensions
- the number of dimensionsNewArray
for the instantiation of an array of base
type typeRef
with dimensions
dimensionspublic static NewArray newArray(TypeReference typeRef, int dimensions, Expression[] sizes, KeYJavaType keyJavaType)
new typeRef[sizes{1}]...[sizes{dimensions}]
typeRef
- the static array base typedimensions
- the number of dimensionssizes
- the size Expression
s for each dimensionkeyJavaType
- the array element typeNewArray
for the instantiation of an array of base
type typeRef
with dimensions
dimensionspublic static NewArray newArray(TypeReference typeRef, int dimensions, Expression size, KeYJavaType keyJavaType)
new typeRef[size]
typeRef
- the static array base typedimensions
- the number of dimensionssize
- the size Expression
for the first dimensionkeyJavaType
- the array element typeNewArray
for the instantiation of an array of base
type typeRef
with dimensions
dimensionspublic static NewArray newArray(TypeReference typeRef, int dimensions, ArrayInitializer initializer, KeYJavaType keyJavaType)
new typeRef[]...[] initializer
typeRef
- the static array base typekeyJavaType
- the array element typeinitializer
- the ArrayInitializer
dimensions
- the number of dimensionsNewArray
for the instantiation of an array of base
type typeRef
with dimensions
dimensionspublic static New newOperator(ReferencePrefix referencePrefix, TypeReference typeReference, Expression[] args)
new referencePrefix.typeReference(args)
referencePrefix
- the typeReference
's ReferencePrefix
typeReference
- a TypeReference
to the class type that is instantiatedargs
- the Expression
arguments to be passed to the
constructorNew
operator that allocates a new instance of
typeReference
parameterized with args
public static New newOperator(ReferencePrefix referencePrefix, KeYJavaType type, Expression[] args)
new referencePrefix.type(args)
referencePrefix
- the type
's ReferencePrefix
type
- the KeYJavaType
to be instantiatedargs
- the Expression
arguments to be passed to the
constructorNew
operator that allocates a new instance of
type
parameterized with args
public static New newOperator(ReferencePrefix referencePrefix, KeYJavaType type)
new referencePrefix.type()
referencePrefix
- the type
's ReferencePrefix
type
- the KeYJavaType
to be instantiatedNew
operator that allocates a new instance of
type
public static New newOperator(KeYJavaType type)
new type()
type
- the KeYJavaType
to be instantiatedNew
operator that allocates a new instance of
type
public static NotEquals notEqualsOperator(ExtList operands)
operands{1} != operands{2}
public static SuperConstructorReference superConstructor(ReferencePrefix referencePrefix, Expression[] args)
super(args)
referencePrefix
- the enclosing class typeargs
- the Expression
arguments to be passed to constructorSuperConstructorReference
parameterized with
args
public static SuperReference superReference()
super
.SuperReference
public static Switch switchBlock(Expression expression, Branch[] branches)
switch (expression) { branches }
expression
- the to be evaluated Expression
branches
- the switch-case Branch
esSwitch
block that executes branches
depending on the value of expression
public static SynchronizedBlock synchronizedBlock(ExtList parameters)
parameters
- the synchronized block parameters (monitor, body) as
ExtList
SynchronizedBlock
as defined by
parameters
public static Then thenBlock(Statement[] statements)
then { statements }
public static ThisConstructorReference thisConstructor(Expression[] args)
this(args)
args
- the Expression
arguments to be passed to constructorThisConstructorReference
parameterized with
args
public static ThisReference thisReference()
this
.ThisReference
public static BooleanLiteral trueLiteral()
true
.BooleanLiteral
that represents the value
true
public static Try tryBlock(StatementBlock body, Branch[] branches)
try body branches
body
- the StatementBlock
to be executedbranches
- the try-catch Branch
esTry
block for the execution of
branches
depending on the events during the
execution of body
public static Try tryBlock(Statement statement, Branch[] branches)
try statement branches
public static Try tryBlock(Statement statement, Branch branch)
try statement branch
public static TypeRef typeRef(KeYJavaType type)
type
type
- the KeYJavaType
to be referencedTypeRef
that references type
public static TypeRef typeRef(KeYJavaType type, int dimensions)
type[]...[]
type
- the base KeYJavaType
dimensions
- the number of dimensionsTypeRef
for dimensions
dimensions of
type
public static BooleanLiteral falseLiteral()
false
.BooleanLiteral
that represents the value
true
public static VariableSpecification variableSpecification(IProgramVariable variable, int dimensions, Expression initializer, Type type)
variable
- the IProgramVariable
to be specifieddimensions
- the number of dimensionsinitializer
- the initializer Expression
type
- the Type
VariableSpecification
for variable
of
type type[dimensions]
, initialized to
initializer
public static VariableSpecification variableSpecification(IProgramVariable variable, Expression initializer, KeYJavaType keyJavaType)
variable
- the IProgramVariable
to be specifiedinitializer
- the initializer Expression
keyJavaType
- the KeYJavaType
VariableSpecification
for variable
of
type type
, initialized to initializer
public static IntLiteral zeroLiteral()
0
IntLiteral
that represents the integer value
0
public static TypeCast cast(Expression expression, KeYJavaType targetType)