Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.abstraction |
This package contains the meta model abstractions as used by the
semantical services.
|
de.uka.ilkd.key.java.declaration |
Elements of the Java syntax tree representing declarations.
|
de.uka.ilkd.key.java.declaration.modifier |
This package collects all Java modifiers.
|
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.recoderext.expression.literal | |
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.java.visitor |
contains classes representing visitors traversing the tree
structure of Java programs.
|
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.logic.sort |
This package contains different kinds and implementations subtyping interface Sort.
|
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
Modifier and Type | Method and Description |
---|---|
protected ExtList |
Recoder2KeYConverter.collectChildren(NonTerminalProgramElement pe)
iterate over all children and call convert upon them.
|
Modifier and Type | Method and Description |
---|---|
static CopyAssignment |
KeYJavaASTFactory.assign(ExtList parameters)
Create an assignment.
|
static StatementBlock |
KeYJavaASTFactory.block(ExtList statements)
Create a block from an arbitrary number of statements.
|
static Case |
KeYJavaASTFactory.caseBlock(ExtList parameters,
Expression expression,
PositionInfo position)
Create a case block.
|
static Catch |
KeYJavaASTFactory.catchClause(ExtList parameters)
Create a catch clause.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ExtList parameters)
Create a local variable declaration without initialization.
|
static Default |
KeYJavaASTFactory.defaultBlock(ExtList parameters)
Create a default block.
|
static Else |
KeYJavaASTFactory.elseBlock(ExtList parameters)
Create an else block.
|
static EnhancedFor |
KeYJavaASTFactory.enhancedForLoop(ExtList parameters)
Create an enhanced for loop.
|
static Equals |
KeYJavaASTFactory.equalsOperator(ExtList operands)
Create an equals operator.
|
static Finally |
KeYJavaASTFactory.finallyBlock(ExtList parameters)
Create a finally block.
|
static For |
KeYJavaASTFactory.forLoop(ExtList parameters)
Create a for loop.
|
static If |
KeYJavaASTFactory.ifStatement(ExtList parameters)
Create an if statement.
|
static LabeledStatement |
KeYJavaASTFactory.labeledStatement(ExtList parameters,
Label label,
PositionInfo position)
Create a labeled statement.
|
static NotEquals |
KeYJavaASTFactory.notEqualsOperator(ExtList operands)
Create an unequal operator.
|
static Switch |
KeYJavaASTFactory.switchBlock(ExtList parameters)
Create a switch block.
|
static SynchronizedBlock |
KeYJavaASTFactory.synchronizedBlock(ExtList parameters)
Create a synchronized block.
|
static Then |
KeYJavaASTFactory.thenBlock(ExtList parameters)
Create a then block.
|
static Try |
KeYJavaASTFactory.tryBlock(ExtList parameters)
Create a try block.
|
Constructor and Description |
---|
DefaultConstructor(ExtList children)
Deprecated.
|
Constructor and Description |
---|
ArrayDeclaration(ExtList children,
TypeReference baseType,
KeYJavaType superType)
ArrayDeclaration
|
ClassDeclaration(ExtList children,
ProgramElementName fullName,
boolean isLibrary) |
ClassDeclaration(ExtList children,
ProgramElementName fullName,
boolean isLibrary,
boolean innerClass,
boolean anonymousClass,
boolean localClass)
uses children list to create non-anonymous class
|
ClassInitializer(ExtList children)
Class initializer.
|
ConstructorDeclaration(ExtList children,
boolean parentIsInterfaceDeclaration)
Constructor declaration.
|
EnumClassDeclaration(ExtList children,
ProgramElementName fullName,
boolean isLibrary,
java.util.List<EnumConstantDeclaration> enumConstantDeclarations)
create a new EnumClassDeclaration that describes an enum defintion.
|
Extends(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
FieldDeclaration(ExtList children,
boolean parentIsInterfaceDeclaration)
Field declaration.
|
FieldSpecification(ExtList children,
ProgramVariable var,
int dimensions,
Type type)
Field specification.
|
Implements(ExtList children)
Implements.
|
InheritanceSpecification(ExtList children)
Inheritance specification.
|
InterfaceDeclaration(ExtList children,
ProgramElementName fullName,
boolean isLibrary)
uses children list to create non-anonymous class
|
JavaDeclaration(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
LocalVariableDeclaration(ExtList children)
Local variable declaration.
|
MethodDeclaration(ExtList children,
boolean parentIsInterfaceDeclaration,
Comment[] voidComments)
Method declaration.
|
Modifier(ExtList children)
Modifier.
|
ParameterDeclaration(ExtList children,
boolean parentIsInterfaceDeclaration,
boolean parameterIsVarArg)
Parameter declaration.
|
Throws(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
TypeDeclaration(ExtList children,
ProgramElementName fullName,
boolean isLibrary) |
TypeDeclaration(ExtList children,
ProgramElementName name,
ProgramElementName fullName,
boolean isLibrary) |
VariableDeclaration(ExtList children,
boolean parentIsInterfaceDeclaration)
Variable declaration.
|
VariableSpecification(ExtList children,
IProgramVariable var,
int dim,
Type type)
Constructor for the transformation of RECODER ASTs to KeY.
|
Constructor and Description |
---|
Abstract(ExtList children)
Abstract.
|
Final(ExtList children)
Abstract.
|
Ghost(ExtList children) |
Model(ExtList children) |
Native(ExtList children)
Native
|
NoState(ExtList children) |
Private(ExtList children)
Private
|
Protected(ExtList children)
Protected.
|
Public(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Static(ExtList children)
Static
|
StrictFp(ExtList children)
Strict fp.
|
Synchronized(ExtList children)
Synchronized.
|
Transient(ExtList children)
Transient.
|
TwoState(ExtList children) |
VisibilityModifier(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Volatile(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Constructor and Description |
---|
ArrayInitializer(ExtList list,
KeYJavaType kjt)
Array initializer.
|
Assignment(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Literal(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Literal(ExtList children,
PositionInfo pos)
Literal with specific source code position.
|
Operator(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
ParenthesizedExpression(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
PassiveExpression(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Constructor and Description |
---|
AbstractIntegerLiteral(ExtList children)
Constructor for Recoder2KeY transformation.
|
BooleanLiteral(ExtList children,
boolean value)
Boolean literal.
|
BooleanLiteral(ExtList children,
PositionInfo pos,
boolean value)
Boolean literal.
|
CharLiteral(ExtList children,
java.lang.String valueStr)
Creates a new CharLiteral from the given String.
|
DoubleLiteral(ExtList children,
java.lang.String value)
Double literal.
|
FloatLiteral(ExtList children,
java.lang.String value)
Float literal.
|
IntLiteral(ExtList children,
java.lang.String valStr)
Constructor for Recoder2KeY transformation.
|
LongLiteral(ExtList children,
java.lang.String valStr)
Constructor for Recoder2KeY transformation.
|
RealLiteral(ExtList children) |
RealLiteral(ExtList children,
java.lang.String value) |
StringLiteral(ExtList children,
java.lang.String value)
String literal.
|
Constructor and Description |
---|
BinaryAnd(ExtList children)
Binary and.
|
BinaryAndAssignment(ExtList children) |
BinaryNot(ExtList children)
Binary not.
|
BinaryOperator(ExtList children) |
BinaryOr(ExtList children)
Binary or.
|
BinaryOrAssignment(ExtList children)
Binary or assignment.
|
BinaryXOr(ExtList children)
Binary X or.
|
BinaryXOrAssignment(ExtList children)
Binary X or assignment.
|
ComparativeOperator(ExtList children)
Comparative operator.
|
Conditional(ExtList children)
Conditional.
|
CopyAssignment(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Divide(ExtList children)
Divide.
|
DivideAssignment(ExtList children)
Divide assignment.
|
DLEmbeddedExpression(Function f,
ExtList children) |
Equals(ExtList children)
Equals.
|
ExactInstanceof(ExtList children)
Instanceof.
|
GreaterOrEquals(ExtList children)
Greater or equals.
|
GreaterThan(ExtList children)
Greater than.
|
Instanceof(ExtList children)
Instanceof.
|
Intersect(ExtList children) |
LessOrEquals(ExtList children)
Less or equals.
|
LessThan(ExtList children)
Less than.
|
LogicalAnd(ExtList children)
Logical and.
|
LogicalNot(ExtList children)
Logical not.
|
LogicalOr(ExtList children)
Logical or.
|
Minus(ExtList children)
Minus.
|
MinusAssignment(ExtList children)
Minus assignment.
|
Modulo(ExtList children)
Modulo.
|
ModuloAssignment(ExtList children)
Modulo assignment.
|
Negative(ExtList children)
Negative.
|
New(ExtList children,
ReferencePrefix rp)
Constructor for the transformation of COMPOST ASTs to KeY.
|
New(ExtList children,
ReferencePrefix rp,
PositionInfo pi)
Constructor for the transformation of COMPOST ASTs to KeY.
|
NewArray(ExtList children,
KeYJavaType keyJavaType,
ArrayInitializer init,
int dimensions)
New array.
|
NotEquals(ExtList children)
Not equals.
|
Plus(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
PlusAssignment(ExtList children)
Plus assignment.
|
Positive(ExtList children)
Positive.
|
PostDecrement(ExtList children)
Post decrement.
|
PostIncrement(ExtList children)
Post increment.
|
PreDecrement(ExtList children)
Pre decrement.
|
PreIncrement(ExtList children)
Pre increment.
|
ShiftLeft(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
ShiftLeftAssignment(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
ShiftRight(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
ShiftRightAssignment(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Times(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
TimesAssignment(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
TypeCast(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
TypeOperator(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
TypeOperator(ExtList children,
PositionInfo pi)
Constructor for the transformation of COMPOST ASTs to KeY.
|
UnsignedShiftRight(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
UnsignedShiftRightAssignment(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Constructor and Description |
---|
AllFields(ExtList children) |
AllObjects(ExtList children) |
SeqConcat(ExtList children) |
SeqGet(ExtList children) |
SeqIndexOf(ExtList children) |
SeqLength(ExtList children) |
SeqReverse(ExtList children) |
SeqSingleton(ExtList children) |
SeqSub(ExtList children) |
SetMinus(ExtList children) |
SetUnion(ExtList children) |
Singleton(ExtList children) |
Constructor and Description |
---|
RealLiteral(ExtList el) |
Constructor and Description |
---|
ArrayLengthReference(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
ArrayReference(ExtList children,
ReferencePrefix accessPath)
Constructor for the transformation of COMPOST ASTs to KeY.
|
ArrayReference(ExtList children,
ReferencePrefix accessPath,
PositionInfo pi)
Constructor for the transformation of COMPOST ASTs to KeY.
|
ExecutionContext(ExtList children)
creates an execution context reference
|
FieldReference(ExtList children,
ReferencePrefix prefix) |
MetaClassReference(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
MethodReference(ExtList children,
MethodName n,
ReferencePrefix p) |
MethodReference(ExtList args,
MethodName n,
ReferencePrefix p,
PositionInfo pos) |
MethodReference(ExtList children,
MethodName n,
ReferencePrefix p,
PositionInfo pos,
java.lang.String scope) |
PackageReference(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
SchematicFieldReference(ExtList children,
ReferencePrefix prefix) |
SpecialConstructorReference(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
SpecialConstructorReference(ExtList children,
PositionInfo pi)
Constructor for the transformation of COMPOST ASTs to KeY.
|
SuperConstructorReference(ExtList children,
ReferencePrefix accessPath)
Constructor for the transformation of COMPOST ASTs to KeY.
|
SuperConstructorReference(ExtList children,
ReferencePrefix accessPath,
PositionInfo pi)
Constructor for the transformation of COMPOST ASTs to KeY.
|
SuperReference(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
ThisConstructorReference(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
ThisReference(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
TypeRef(ExtList children,
KeYJavaType kjt,
int dim) |
TypeReferenceImp(ExtList children,
int dim)
Constructor for the transformation of RECODER ASTs to KeY.
|
VariableReference(ExtList children) |
Constructor and Description |
---|
BranchImp(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
BranchImp(ExtList children,
PositionInfo pos) |
BranchStatement(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Break(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Case(ExtList children,
Expression expr,
PositionInfo pos)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Catch(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
CatchAllStatement(ExtList children) |
Ccatch(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Continue(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Default(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Do(Expression guard,
Statement body,
ExtList l,
PositionInfo pos)
Do.
|
Else(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
EmptyStatement(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
EnhancedFor(ExtList children)
Used by the
CreatingASTVisitor . |
EnhancedFor(LoopInit init,
Guard guard,
Statement statement,
ExtList comments,
PositionInfo info)
Used for the Recoder2KeY transformation.
|
Exec(ExtList children)
Exec.
|
ExpressionJumpStatement(ExtList children)
Expression jump statement.
|
Finally(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
For(ExtList children) |
For(ILoopInit inits,
IGuard guard,
IForUpdates updates,
Statement body,
ExtList comments) |
For(ILoopInit inits,
IGuard guard,
IForUpdates updates,
Statement body,
ExtList comments,
PositionInfo pos) |
ForUpdates(ExtList ups,
PositionInfo pos) |
Guard(ExtList children) |
If(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
JavaStatement(ExtList children)
Java statement.
|
JavaStatement(ExtList children,
PositionInfo pos) |
JumpStatement(ExtList children)
Jump statement.
|
LabeledStatement(ExtList children,
Label label,
PositionInfo pos)
Constructor for the transformation of COMPOST ASTs to KeY.
|
LabelJumpStatement(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
LoopInit(ExtList ups,
PositionInfo pos) |
LoopScopeBlock(ExtList children)
Synchronized block.
|
LoopStatement(Expression guard,
Statement body,
ExtList comments)
Loop statement.
|
LoopStatement(Expression guard,
Statement body,
ExtList comments,
PositionInfo pos) |
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) |
MergePointStatement(ExtList children) |
MethodBodyStatement(ExtList list) |
Return(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Switch(ExtList children)
Switch.
|
SynchronizedBlock(ExtList children)
Synchronized block.
|
Then(ExtList children)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Throw(ExtList children)
Throw.
|
Try(ExtList children)
Try.
|
While(Expression guard,
Statement body,
PositionInfo pos,
ExtList comments)
While.
|
Modifier and Type | Field and Description |
---|---|
protected java.util.Deque<ExtList> |
CreatingASTVisitor.stack |
Modifier and Type | Method and Description |
---|---|
protected void |
CreatingASTVisitor.DefaultAction.addNewChild(ExtList changeList) |
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 | Method and Description |
---|---|
Expression |
ProgramInLogic.convertToProgram(Term t,
ExtList list) |
Modifier and Type | Method and Description |
---|---|
Expression |
ProgramVariable.convertToProgram(Term t,
ExtList l) |
Expression |
ProgramMethod.convertToProgram(Term t,
ExtList l) |
Modifier and Type | Method and Description |
---|---|
ProgramElement |
ProgramSVSort.getSVWithSort(ExtList l,
java.lang.Class<?> alternative) |
Modifier and Type | Field and Description |
---|---|
protected ExtList |
WhileLoopTransformation.labelList |
Modifier and Type | Field and Description |
---|---|
protected java.util.Stack<ExtList> |
WhileLoopTransformation.stack |
Copyright © 2003-2019 The KeY-Project.