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.ldt |
This package contains the "language data types" (LDTs) of KeY.
|
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 |
This package contains classes for implementing rules.
|
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.
|
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.model | |
de.uka.ilkd.key.symbolic_execution.model.impl | |
de.uka.ilkd.key.symbolic_execution.slicing |
Modifier and Type | Method and Description |
---|---|
static Expression |
KeYJavaASTFactory.attribute(ReferencePrefix prefix,
ProgramVariable field)
creates an attribute access
prefix.field |
Expression |
Recoder2KeYConverter.convert(FieldReference fr)
converts a recoder field reference.
|
Expression |
SchemaRecoder2KeYConverter.convert(FieldReference fr) |
Expression |
TypeConverter.convertToProgramElement(Term term)
converts a logical term to an AST node if possible.
|
protected Expression |
CreateArrayMethodBuilder.getDefaultValue(Type type)
returns the default value of the given type according to JLS \S 4.5.5
|
Expression |
ExpressionContainer.getExpressionAt(int index) |
Modifier and Type | Method and Description |
---|---|
static ArrayReference |
KeYJavaASTFactory.arrayFieldAccess(ReferencePrefix array,
Expression index)
Create an array field access with a single index.
|
static ArrayInitializer |
KeYJavaASTFactory.arrayInitializer(Expression[] expressions,
KeYJavaType type)
Create an array initializer.
|
static CopyAssignment |
KeYJavaASTFactory.assign(Expression lhs,
Expression rhs)
creates an assignment
lhs:=rhs |
static CopyAssignment |
KeYJavaASTFactory.assign(Expression lhs,
Expression rhs,
PositionInfo posInfo)
creates an assignment
lhs:=rhs |
static CopyAssignment |
KeYJavaASTFactory.assignArrayField(ProgramVariable variable,
ReferencePrefix array,
Expression index)
Create a statement that assigns an array element to a variable.
|
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 Case |
KeYJavaASTFactory.caseBlock(ExtList parameters,
Expression expression,
PositionInfo position)
Create a case block.
|
static TypeCast |
KeYJavaASTFactory.cast(Expression expression,
KeYJavaType targetType) |
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ImmutableArray<Modifier> modifiers,
IProgramVariable variable,
Expression init,
KeYJavaType type)
Create a local variable declaration with an arbitrary number of
modifiers.
|
static ProgramElement |
KeYJavaASTFactory.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 |
KeYJavaASTFactory.declare(ImmutableArray<Modifier> modifiers,
IProgramVariable variable,
Expression init,
TypeReference typeRef)
Create a local variable declaration with an arbitrary number of
modifiers.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(IProgramVariable variable,
Expression init)
Create a local variable declaration.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(IProgramVariable var,
Expression init,
KeYJavaType type)
Create a local variable declaration.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(Modifier[] modifiers,
IProgramVariable variable,
Expression init,
KeYJavaType type)
Create a local variable declaration with an arbitrary number of
modifiers.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(Modifier modifier,
IProgramVariable variable,
Expression init,
KeYJavaType type)
Create a local variable declaration with a single modifier.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ProgramElementName name,
Expression init,
KeYJavaType type)
create a local variable declaration
type name = init; |
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(Services services,
java.lang.String name,
Expression initializer,
KeYJavaType type)
Create a local variable declaration with a unique name.
|
static Do |
KeYJavaASTFactory.doLoop(Expression condition,
Statement statement,
PositionInfo positionInfo)
Create a do loop.
|
static Equals |
KeYJavaASTFactory.equalsNullOperator(Expression expression)
Create an equality comparison with
null . |
static Equals |
KeYJavaASTFactory.equalsOperator(Expression left,
Expression right)
Create an equals operator.
|
static FieldReference |
KeYJavaASTFactory.fieldReference(Services services,
java.lang.String name,
Expression expression,
ExecutionContext context)
Create a field access.
|
static IForUpdates |
KeYJavaASTFactory.forUpdates(Expression update)
Create a list of loop updates that consists of a single expression.
|
KeYJavaType |
ConstantExpressionEvaluator.getCompileTimeConstantType(Expression expr) |
KeYJavaType |
TypeConverter.getKeYJavaType(Expression e)
Retrieves the static type of the expression.
|
KeYJavaType |
TypeConverter.getKeYJavaType(Expression e,
ExecutionContext ec)
retrieves the type of the expression e with respect to
the context in which it is evaluated
|
IProgramMethod |
CreateArrayMethodBuilder.getPrepareArrayMethod(TypeRef arrayRef,
ProgramVariable length,
Expression defaultValue,
ImmutableList<Field> fields)
returns the prepare method for arrays initialising all array fields with
their default value
|
static Statement |
KeYJavaASTFactory.ifElse(Expression guard,
Statement thenStatement,
Statement elseStatement)
Create an if clause.
|
static If |
KeYJavaASTFactory.ifElse(Expression guard,
Then then,
Else els)
Create an if statement including an else branch.
|
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 If |
KeYJavaASTFactory.ifThen(Expression guard,
Then then)
Create an if statement with no else branch.
|
static Instanceof |
KeYJavaASTFactory.instanceOf(Expression expression,
KeYJavaType type)
Create an instance of operator.
|
boolean |
TypeConverter.isAssignableTo(Expression expr,
Type to,
ExecutionContext ec) |
boolean |
ConstantExpressionEvaluator.isCompileTimeConstant(Expression expr) |
boolean |
ConstantExpressionEvaluator.isCompileTimeConstant(Expression expr,
ConstantEvaluator.EvaluationResult result) |
boolean |
TypeConverter.isImplicitNarrowing(Expression expr,
PrimitiveType to) |
static IGuard |
KeYJavaASTFactory.lessThanGuard(Expression left,
Expression right)
Create a condition that compares two expressions using the less than
operator.
|
static LessThan |
KeYJavaASTFactory.lessThanOperator(Expression left,
Expression right)
Create a less than operator.
|
static LessThan |
KeYJavaASTFactory.lessThanZeroOperator(Expression expression)
Create a less than zero operator.
|
static LogicalAnd |
KeYJavaASTFactory.logicalAndOperator(Expression left,
Expression right)
Create a logical and operator.
|
static LogicalOr |
KeYJavaASTFactory.logicalOrOperator(Expression left,
Expression right)
Create a logical or operator.
|
static MethodBodyStatement |
KeYJavaASTFactory.methodBody(ProgramVariable result,
ReferencePrefix reference,
IProgramMethod method,
Expression[] arguments)
Create a method body shortcut.
|
static MethodReference |
KeYJavaASTFactory.methodCall(KeYJavaType type,
java.lang.String name,
Expression... args)
Create a method call on a type.
|
static MethodReference |
KeYJavaASTFactory.methodCall(ReferencePrefix reference,
MethodName name,
Expression... args)
Create a method call.
|
static MethodReference |
KeYJavaASTFactory.methodCall(ReferencePrefix reference,
java.lang.String name,
Expression... args)
Create a method call.
|
static NewArray |
KeYJavaASTFactory.newArray(TypeReference typeRef,
int dimensions,
Expression[] sizes,
ArrayInitializer initializer,
KeYJavaType keyJavaType)
Create an array instantiation.
|
static NewArray |
KeYJavaASTFactory.newArray(TypeReference typeRef,
int dimensions,
Expression[] sizes,
KeYJavaType keyJavaType)
Create an array instantiation.
|
static NewArray |
KeYJavaASTFactory.newArray(TypeReference typeRef,
int dimensions,
Expression size,
KeYJavaType keyJavaType)
Create an array instantiation.
|
static New |
KeYJavaASTFactory.newOperator(ReferencePrefix referencePrefix,
KeYJavaType type,
Expression[] args)
Create an object allocation.
|
static New |
KeYJavaASTFactory.newOperator(ReferencePrefix referencePrefix,
TypeReference typeReference,
Expression[] args)
Create an object allocation.
|
static ParenthesizedExpression |
KeYJavaASTFactory.parenthesizedExpression(Expression expression)
Create a parenthesized expression.
|
static PassiveExpression |
KeYJavaASTFactory.passiveExpression(Expression expression)
Create an inactive expression.
|
static Return |
KeYJavaASTFactory.returnClause(Expression e)
Create a return clause.
|
static SuperConstructorReference |
KeYJavaASTFactory.superConstructor(ReferencePrefix referencePrefix,
Expression[] args)
Create a call to the super constructor.
|
static Switch |
KeYJavaASTFactory.switchBlock(Expression expression,
Branch[] branches)
Create a switch block.
|
static ThisConstructorReference |
KeYJavaASTFactory.thisConstructor(Expression[] args)
Create a call to a constructor of the current class.
|
static Throw |
KeYJavaASTFactory.throwClause(Expression e)
Create a throw clause.
|
static VariableSpecification |
KeYJavaASTFactory.variableSpecification(IProgramVariable variable,
Expression initializer,
KeYJavaType keyJavaType)
Create a variable specification.
|
static VariableSpecification |
KeYJavaASTFactory.variableSpecification(IProgramVariable variable,
int dimensions,
Expression initializer,
Type type)
Create a variable specification.
|
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 |
---|---|
ImmutableList<KeYJavaType> |
JavaInfo.createSignature(ImmutableArray<? extends Expression> arguments)
retrieves the signature according to the given expressions
|
static MethodBodyStatement |
KeYJavaASTFactory.methodBody(ProgramVariable result,
ReferencePrefix reference,
IProgramMethod method,
ImmutableArray<Expression> arguments)
Create a method body shortcut.
|
static MethodReference |
KeYJavaASTFactory.methodCall(KeYJavaType type,
java.lang.String name,
ImmutableArray<? extends Expression> args)
Create a method call on a type.
|
static MethodReference |
KeYJavaASTFactory.methodCall(ReferencePrefix reference,
MethodName name,
ImmutableArray<? extends Expression> args)
Create a method call.
|
static MethodReference |
KeYJavaASTFactory.methodCall(ReferencePrefix reference,
java.lang.String name,
ImmutableArray<? extends Expression> args)
Create a method call.
|
Modifier and Type | Field and Description |
---|---|
protected Expression |
VariableSpecification.initializer
Initializer.
|
Modifier and Type | Method and Description |
---|---|
Expression |
VariableSpecification.getExpressionAt(int index) |
Expression |
VariableSpecification.getInitializer()
Get initializer.
|
Constructor and Description |
---|
FieldSpecification(ProgramVariable var,
Expression init,
Type type)
Field specification.
|
FieldSpecification(ProgramVariable var,
int dimensions,
Expression init,
Type type)
Field specification.
|
VariableSpecification(IProgramVariable var,
Expression init,
Type type) |
VariableSpecification(IProgramVariable var,
int dim,
Expression init,
Type type) |
VariableSpecification(IProgramVariable var,
int dim,
Expression init,
Type type,
PositionInfo pi) |
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 |
ArrayInitializer
An ArrayInitializer is a valid expression exclusively for initializing
ArrayTypes.
|
class |
Assignment
An assignment is an operator with side-effects.
|
class |
Literal
Literal.
|
class |
Operator
Operator base class.
|
class |
ParenthesizedExpression
Redundant Parentheses.
|
class |
PassiveExpression
Marks an active statement as inactive.
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableArray<Expression> |
ArrayInitializer.children |
protected ImmutableArray<Expression> |
Operator.children
Children.
|
Modifier and Type | Method and Description |
---|---|
Expression |
ArrayInitializer.getExpressionAt(int index) |
Expression |
Operator.getExpressionAt(int index) |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<Expression> |
ArrayInitializer.getArguments()
Get arguments.
|
ImmutableArray<Expression> |
Operator.getArguments()
return arguments
|
Constructor and Description |
---|
ArrayInitializer(Expression[] expressions,
KeYJavaType kjt)
create a new array initializer with the given expressions as elements.
|
Assignment(Expression lhs)
Unary Assignment (e.g.
|
Assignment(Expression lhs,
Expression rhs)
Assignment.
|
Operator(Expression unaryChild)
Operator.
|
Operator(Expression[] arguments)
Operator.
|
Operator(Expression lhs,
Expression rhs)
Operator.
|
ParenthesizedExpression(Expression child) |
PassiveExpression(Expression child) |
Modifier and Type | Class and Description |
---|---|
class |
AbstractIntegerLiteral
This class is a superclass for integer literals (Int, Long, Char).
|
class |
BooleanLiteral
Boolean literal.
|
class |
CharLiteral
Char literal.
|
class |
DoubleLiteral
Double literal.
|
class |
EmptyMapLiteral |
class |
EmptySeqLiteral |
class |
EmptySetLiteral |
class |
FloatLiteral
Float literal.
|
class |
FreeLiteral |
class |
IntLiteral
Int literal.
|
class |
LongLiteral
Long literal.
|
class |
NullLiteral
Null literal.
|
class |
RealLiteral
JML \real literal.
|
class |
StringLiteral |
Modifier and Type | Class and Description |
---|---|
class |
BinaryAnd
Binary and.
|
class |
BinaryAndAssignment
Binary and assignment.
|
class |
BinaryNot
Binary not.
|
class |
BinaryOperator
Operator of arity 2
|
class |
BinaryOr
Binary or.
|
class |
BinaryOrAssignment
Binary or assignment.
|
class |
BinaryXOr
Binary X or.
|
class |
BinaryXOrAssignment
Binary X or assignment.
|
class |
ComparativeOperator
Comparative operator.
|
class |
Conditional
The most weird ternary C operator ?:
|
class |
CopyAssignment
Copy assignment.
|
class |
Divide
Divide.
|
class |
DivideAssignment
Divide assignment.
|
class |
DLEmbeddedExpression |
class |
Equals
Equals.
|
class |
ExactInstanceof
Instanceof.
|
class |
GreaterOrEquals
Greater or equals.
|
class |
GreaterThan
Greater than.
|
class |
Instanceof
Instanceof.
|
class |
Intersect |
class |
LessOrEquals
Less or equals.
|
class |
LessThan
Less than.
|
class |
LogicalAnd
Logical and.
|
class |
LogicalNot
Logical not.
|
class |
LogicalOr
Logical or.
|
class |
Minus
Minus.
|
class |
MinusAssignment
Minus assignment.
|
class |
Modulo
Modulo.
|
class |
ModuloAssignment
Modulo assignment.
|
class |
Negative
Negative.
|
class |
New
The object allocation operator.
|
class |
NewArray
The array allocation operator.
|
class |
NotEquals
Not equals.
|
class |
Plus
Addition or string concatenation operator "+".
|
class |
PlusAssignment
Addition or string concatenation assignment "+=".
|
class |
Positive
Positive.
|
class |
PostDecrement
Post decrement.
|
class |
PostIncrement
Post increment.
|
class |
PreDecrement
Pre decrement.
|
class |
PreIncrement
Pre increment.
|
class |
ShiftLeft
Shift left.
|
class |
ShiftLeftAssignment
Shift left assignment.
|
class |
ShiftRight
Shift right.
|
class |
ShiftRightAssignment
Shift right assignment.
|
class |
Times
Times.
|
class |
TimesAssignment
Times assignment.
|
class |
TypeCast
Type cast.
|
class |
TypeOperator
Type operator.
|
class |
UnsignedShiftRight
Unsigned shift right.
|
class |
UnsignedShiftRightAssignment
Unsigned shift right assignment.
|
Modifier and Type | Method and Description |
---|---|
Expression |
NewArray.getExpressionAt(int index) |
Constructor and Description |
---|
BinaryOperator(Expression lhs,
Expression rhs) |
ComparativeOperator(Expression lhs,
Expression rhs) |
CopyAssignment(Expression lhs,
Expression rhs)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Divide(Expression lhs,
Expression rhs) |
Equals(Expression lhs,
Expression rhs)
Creates the equals expression
lhs==rhs |
ExactInstanceof(Expression unaryChild,
TypeReference typeref) |
GreaterThan(Expression lhs,
Expression rhs)
Greater than.
|
Instanceof(Expression unaryChild,
TypeReference typeref) |
LessOrEquals(Expression lhs,
Expression rhs) |
LessThan(Expression lhs,
Expression rhs)
Less than.
|
LogicalAnd(Expression lhs,
Expression rhs) |
LogicalOr(Expression lhs,
Expression rhs) |
Minus(Expression lhs,
Expression rhs) |
Modulo(Expression lhs,
Expression rhs) |
Negative(Expression expr) |
New(Expression[] arguments,
TypeReference type,
ReferencePrefix rp)
Constructor for the transformation of COMPOST ASTs to KeY.
|
NewArray(Expression[] arguments,
TypeReference typeRef,
KeYJavaType keyJavaType,
ArrayInitializer init,
int dimensions)
New array.
|
Plus(Expression lhs,
Expression rhs) |
Positive(Expression expr)
Positive.
|
PostIncrement(Expression unary)
Post increment.
|
ShiftLeft(Expression lhs,
Expression rhs)
Shift left.
|
ShiftLeftAssignment(Expression lhs,
Expression rhs)
Shift left assignment.
|
ShiftRight(Expression lhs,
Expression rhs)
Shift right.
|
ShiftRightAssignment(Expression lhs,
Expression rhs)
Shift right assignment.
|
Times(Expression lhs,
Expression rhs)
Times.
|
TimesAssignment(Expression lhs,
Expression rhs)
Times assignment.
|
TypeCast(Expression child,
TypeReference typeref)
Note: The ordering of the arguments does not match the syntactical
appearance of a Java type case, but the order in the superclass
TypeOperator.
|
TypeOperator(Expression[] arguments,
TypeReference typeref) |
TypeOperator(Expression unaryChild,
TypeReference typeref) |
UnsignedShiftRight(Expression lhs,
Expression rhs)
Unsigned shift right.
|
UnsignedShiftRightAssignment(Expression lhs,
Expression rhs)
Unsigned shift right assignment.
|
Modifier and Type | Class and Description |
---|---|
class |
AllFields |
class |
AllObjects |
class |
SeqConcat |
class |
SeqGet
Represents a sequence getter function.
|
class |
SeqIndexOf
Represents a function giving the index of some element in a sequence (if it exists).
|
class |
SeqLength
Represents a function giving the length of a sequence.
|
class |
SeqReverse |
class |
SeqSingleton |
class |
SeqSub |
class |
SetMinus |
class |
SetUnion |
class |
Singleton |
Constructor and Description |
---|
SeqConcat(Expression seq1,
Expression seq2) |
SeqSingleton(Expression child) |
Modifier and Type | Class and Description |
---|---|
class |
ArrayLengthReference
Array length reference.
|
class |
ArrayReference
Array reference.
|
class |
FieldReference |
class |
MetaClassReference
Meta class reference.
|
class |
MethodReference
Method reference.
|
class |
SchematicFieldReference
Field reference.
|
class |
SuperReference
Super reference.
|
class |
ThisReference
A reference to the current object.
|
class |
VariableReference |
Modifier and Type | Field and Description |
---|---|
protected ImmutableArray<? extends Expression> |
MethodReference.arguments
Arguments.
|
protected ImmutableArray<Expression> |
SpecialConstructorReference.arguments |
protected ImmutableArray<Expression> |
ArrayReference.inits
Inits.
|
Modifier and Type | Method and Description |
---|---|
Expression |
MethodReference.getArgumentAt(int index)
Gets index-th argument
|
Expression |
MethodReference.getExpressionAt(int index) |
Expression |
TypeReferenceImp.getExpressionAt(int index) |
Expression |
ArrayReference.getExpressionAt(int index) |
Expression |
SuperReference.getExpressionAt(int index) |
Expression |
SpecialConstructorReference.getExpressionAt(int index) |
Expression |
SchematicFieldReference.getExpressionAt(int index)
Return the expression at the specified index in this node's
"virtual" expression array.
|
Expression |
FieldReference.getExpressionAt(int index) |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<? extends Expression> |
MethodReference.getArguments()
Get arguments.
|
ImmutableArray<Expression> |
SpecialConstructorReference.getArguments()
Get arguments.
|
ImmutableArray<? extends Expression> |
MethodOrConstructorReference.getArguments() |
ImmutableArray<Expression> |
ArrayReference.getDimensionExpressions()
Get dimension expressions.
|
Constructor and Description |
---|
ArrayReference(ReferencePrefix accessPath,
Expression[] initializers)
Array reference.
|
SpecialConstructorReference(Expression[] arguments)
Special constructor reference.
|
SuperConstructorReference(Expression[] arguments)
Super constructor reference.
|
SuperConstructorReference(ReferencePrefix accessPath,
Expression[] arguments)
Super constructor reference.
|
ThisConstructorReference(Expression[] arguments)
This constructor reference.
|
Constructor and Description |
---|
MethodReference(ImmutableArray<? extends Expression> args,
MethodName n,
ReferencePrefix p) |
MethodReference(ImmutableArray<Expression> args,
MethodName n,
ReferencePrefix p,
PositionInfo pos) |
SpecialConstructorReference(ImmutableArray<Expression> arguments)
Special constructor reference.
|
SuperConstructorReference(ReferencePrefix accessPath,
ImmutableArray<Expression> arguments)
Super constructor reference.
|
ThisConstructorReference(ImmutableArray<Expression> arguments)
This constructor reference.
|
Modifier and Type | Field and Description |
---|---|
protected Expression |
Switch.expression
Expression.
|
protected Expression |
SynchronizedBlock.expression
Expression.
|
protected Expression |
ExpressionJumpStatement.expression
Expression.
|
protected Expression |
Case.expression
Expression.
|
protected Expression |
If.expression
Expression.
|
Modifier and Type | Method and Description |
---|---|
Expression |
Assert.getCondition() |
Expression |
Switch.getExpression()
Get expression.
|
Expression |
MergePointStatement.getExpression()
Get expression.
|
Expression |
SynchronizedBlock.getExpression()
Get expression.
|
Expression |
Guard.getExpression() |
Expression |
ExpressionJumpStatement.getExpression()
Get expression.
|
Expression |
Case.getExpression()
Get expression.
|
Expression |
If.getExpression()
Get expression.
|
Expression |
LoopStatement.getExpressionAt(int index) |
Expression |
Switch.getExpressionAt(int index) |
Expression |
LoopScopeBlock.getExpressionAt(int index)
Return the expression at the specified index in this node's "virtual"
expression array.
|
Expression |
IForUpdates.getExpressionAt(int i) |
Expression |
MergePointStatement.getExpressionAt(int index)
Return the expression at the specified index in this node's "virtual"
expression array.
|
Expression |
ForUpdates.getExpressionAt(int index) |
Expression |
SynchronizedBlock.getExpressionAt(int index) |
Expression |
Assert.getExpressionAt(int index) |
Expression |
ExpressionJumpStatement.getExpressionAt(int index)
Return the expression at the specified index in this node's
"virtual" expression array.
|
Expression |
Case.getExpressionAt(int index) |
Expression |
If.getExpressionAt(int index) |
Expression |
LoopStatement.getGuardExpression()
Get guard.
|
Expression |
Assert.getMessage() |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<? extends Expression> |
MethodBodyStatement.getArguments() |
ImmutableArray<Expression> |
LoopStatement.getUpdates()
Get updates.
|
ImmutableArray<Expression> |
IForUpdates.getUpdates() |
ImmutableArray<Expression> |
ForUpdates.getUpdates() |
Constructor and Description |
---|
Assert(Expression condition,
Expression message,
PositionInfo pos) |
Case(Expression e)
Case.
|
Case(Expression e,
Statement[] body)
Case.
|
Case(ExtList children,
Expression expr,
PositionInfo pos)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Do(Expression guard)
Do.
|
Do(Expression guard,
Statement body,
ExtList l,
PositionInfo pos)
Do.
|
Do(Expression guard,
Statement body,
PositionInfo pos)
Do.
|
ExpressionJumpStatement(Expression expr)
Expression jump statement.
|
For(LoopInitializer[] inits,
Expression guard,
Expression[] updates,
Statement body)
For.
|
For(LoopInitializer[] inits,
Expression guard,
Expression[] updates,
Statement body)
For.
|
Guard(Expression expression) |
If(Expression e,
Then thenBranch)
If.
|
If(Expression e,
Then thenBranch,
Else elseBranch)
If.
|
LoopStatement(Expression guard)
Loop 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(LoopInitializer[] inits,
Expression guard,
Expression[] updates,
Statement body)
Loop statement.
|
LoopStatement(LoopInitializer[] inits,
Expression guard,
Expression[] updates,
Statement body)
Loop statement.
|
Return(Expression expr)
Expression jump statement.
|
Switch(Expression e)
Switch.
|
Switch(Expression e,
Branch[] branches)
Switch.
|
SynchronizedBlock(Expression e,
StatementBlock body)
Synchronized block.
|
Throw(Expression expr)
Throw.
|
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.
|
Constructor and Description |
---|
ForUpdates(ImmutableArray<Expression> exprarr) |
MethodBodyStatement(IProgramMethod method,
ReferencePrefix newContext,
IProgramVariable res,
ImmutableArray<Expression> args) |
MethodBodyStatement(IProgramMethod method,
ReferencePrefix newContext,
IProgramVariable res,
ImmutableArray<Expression> args,
boolean useSpecification) |
MethodBodyStatement(IProgramMethod method,
ReferencePrefix newContext,
IProgramVariable res,
ImmutableArray<Expression> args,
boolean useSpecification,
ProgramElement scope) |
MethodBodyStatement(IProgramMethod method,
ReferencePrefix newContext,
IProgramVariable res,
ImmutableArray<Expression> args,
ProgramElement scope) |
Modifier and Type | Method and Description |
---|---|
Expression |
DoubleLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
CharListLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
FreeLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
MapLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
RealLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
BooleanLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
PermissionLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
LocSetLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
IntegerLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
HeapLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
FloatLDT.translateTerm(Term t,
ExtList children,
Services services) |
Expression |
SeqLDT.translateTerm(Term t,
ExtList children,
Services services) |
abstract Expression |
LDT.translateTerm(Term t,
ExtList children,
Services services)
Is called whenever
hasLiteralFunction() returns true. |
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 | Method and Description |
---|---|
Expression |
ProgramInLogic.convertToProgram(Term t,
ExtList list) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
VariableNamer.getSuggestiveNameProposalForSchemaVariable(Expression e) |
Modifier and Type | Class and Description |
---|---|
class |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
class |
ProgramConstant
This class represents currently only static final fields initialised with
a compile time constant.
|
class |
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
class |
ProgramVariable
The objects of this class represent program variables and program
constants (resulting from static final declarations in programs; TODO: it is
weird that constants are a special case of variables).
|
Modifier and Type | Method and Description |
---|---|
Expression |
ProgramVariable.convertToProgram(Term t,
ExtList l) |
Expression |
ProgramMethod.convertToProgram(Term t,
ExtList l) |
Expression |
ProgramSV.getExpressionAt(int index) |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<Expression> |
ProgramSV.getUpdates() |
Modifier and Type | Field and Description |
---|---|
Expression |
UseOperationContractRule.Instantiation.actualResult
The actual result expression.
|
Constructor and Description |
---|
Instantiation(Term u,
Term progPost,
Modality mod,
Expression actualResult,
Term actualSelf,
KeYJavaType staticType,
MethodOrConstructorReference mr,
IProgramMethod pm,
ImmutableList<Term> actualParams,
boolean transaction)
Creates a new instantiation for the contract rule and the given variables.
|
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 | Field and Description |
---|---|
protected ImmutableArray<Expression> |
MethodCall.arguments |
Modifier and Type | Method and Description |
---|---|
protected Expression |
InitArray.createArrayCreation(NewArray p_creationExpression)
Create an array creation expression for an array of the size
given by the array initializer
|
Expression |
ProgramTransformer.getExpressionAt(int index) |
Modifier and Type | Method and Description |
---|---|
protected ImmutableArray<Expression> |
InitArray.extractInitializers(NewArray p_creationExpression)
Extract the variable initializers from the array initializer
|
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)
|
static ProgramVariable |
EvaluateArgs.evaluate(Expression e,
java.util.List<? super LocalVariableDeclaration> l,
Services services,
ExecutionContext ec)
TODO Comment.
|
Constructor and Description |
---|
ArrayLength(Expression expr)
creates a typeof ProgramTransformer
|
StaticInitialisation(Expression expr) |
Modifier and Type | Method and Description |
---|---|
Expression |
LoopContract.getGuard() |
Expression |
LoopContractImpl.getGuard() |
Modifier and Type | Method and Description |
---|---|
Expression |
ExecutionNodeReader.KeYlessLoopCondition.getGuardExpression()
Returns the loop expression which is executed.
|
Modifier and Type | Method and Description |
---|---|
Expression |
IExecutionLoopCondition.getGuardExpression()
Returns the loop expression which is executed.
|
Modifier and Type | Method and Description |
---|---|
Expression |
ExecutionLoopCondition.getGuardExpression()
Returns the loop expression which is executed.
|
Modifier and Type | Method and Description |
---|---|
static Term |
AbstractSlicer.toTerm(Services services,
Expression expression,
ExecutionContext ec)
Converts the given
Expression into a Term . |
Modifier and Type | Method and Description |
---|---|
static ImmutableArray<Term> |
AbstractSlicer.toTerm(Services services,
ImmutableArray<Expression> expressions,
ExecutionContext ec)
Converts the given
Expression s into Term s. |
Copyright © 2003-2019 The KeY-Project.