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.operator |
Elements of the Java syntax tree representing operators and operator-like
expressions.
|
de.uka.ilkd.key.java.reference |
Elements of the Java syntax tree representing implicit or explicit (named)
references to other program elements.
|
de.uka.ilkd.key.java.statement |
Elements of the Java syntax tree representing pure statements.
|
de.uka.ilkd.key.java.visitor |
contains classes representing visitors traversing the tree
structure of Java programs.
|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
TypeReference |
Recoder2KeYConverter.convert(TypeReference tr)
convert a recoder TypeReference to a KeY TypeReference (checks dimension
and hands it over)
|
TypeReference |
SchemaRecoder2KeYConverter.convert(TypeReference tr)
convert a recoder TypeReference to a KeY TypeReference (checks dimension
and hands it over)
|
TypeReference |
JavaInfo.createTypeReference(KeYJavaType kjt)
creates a new TypeReference for the given KeYJavaType
|
TypeReference |
Import.getTypeReference()
Returns the type reference of this import, if there is one.
|
TypeReference |
Import.getTypeReferenceAt(int index) |
Modifier and Type | Method and Description |
---|---|
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(ImmutableArray<Modifier> modifiers,
TypeReference typeRef,
VariableSpecification specification)
Create a local variable declaration.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ImmutableArray<Modifier> modifiers,
TypeReference typeRef,
VariableSpecification[] specifications)
Create local variable declarations.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ProgramElementName name,
TypeReference typeRef)
creates a local variable declaration
typeRef name; |
IProgramMethod |
CreateArrayMethodBuilder.getArrayInstanceAllocatorMethod(TypeReference arrayTypeReference)
creates the implicit method
<allocate> which is a
stump and given meaning by a contract |
protected StatementBlock |
CreateArrayMethodBuilder.getCreateArrayBody(TypeReference arrayRef,
ProgramVariable paramLength) |
IProgramMethod |
CreateArrayMethodBuilder.getCreateArrayHelperMethod(TypeReference arrayTypeReference,
ProgramVariable length,
ImmutableList<Field> fields)
create the method declaration of the
<createArrayHelper> method |
IProgramMethod |
CreateArrayMethodBuilder.getCreateArrayMethod(TypeReference arrayTypeReference,
IProgramMethod prepare,
ImmutableList<Field> fields)
creates the implicit method
<createArray> it
fulfills a similar purpose as <createObject> in
addition it sets the arrays length and calls the prepare method |
Type |
KeYProgModelInfo.getType(TypeReference tr) |
static NewArray |
KeYJavaASTFactory.newArray(TypeReference typeRef,
int dimensions,
ArrayInitializer initializer,
KeYJavaType keyJavaType)
Create an array instantiation.
|
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,
TypeReference typeReference,
Expression[] args)
Create an object allocation.
|
void |
PrettyPrinter.printTypeReference(TypeReference x) |
void |
PrettyPrinter.printTypeReference(TypeReference x,
boolean fullTypeNames) |
Constructor and Description |
---|
Import(TypeReference t,
boolean multi)
Import.
|
Modifier and Type | Method and Description |
---|---|
TypeReference |
ArrayType.getBaseType()
returns the type reference to the arrays base type
|
Modifier and Type | Field and Description |
---|---|
protected TypeReference |
MethodDeclaration.returnType |
protected TypeReference |
VariableDeclaration.typeReference
Type reference.
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableArray<TypeReference> |
Throws.exceptions
Exceptions.
|
protected ImmutableArray<TypeReference> |
InheritanceSpecification.supertypes
Supertypes.
|
Modifier and Type | Method and Description |
---|---|
TypeReference |
ArrayDeclaration.getBaseType()
Get the element/base type.
|
TypeReference |
VariableDeclaration.getTypeReference()
Get type reference.
|
TypeReference |
MethodDeclaration.getTypeReference()
Get return type.
|
TypeReference |
VariableDeclaration.getTypeReferenceAt(int index) |
TypeReference |
Throws.getTypeReferenceAt(int index) |
TypeReference |
InheritanceSpecification.getTypeReferenceAt(int index) |
TypeReference |
MethodDeclaration.getTypeReferenceAt(int index) |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<TypeReference> |
Throws.getExceptions()
Get exceptions.
|
ImmutableArray<TypeReference> |
InheritanceSpecification.getSupertypes()
Get supertypes.
|
Modifier and Type | Method and Description |
---|---|
static ProgramElementName |
ArrayDeclaration.createName(TypeReference basetype) |
Constructor and Description |
---|
ArrayDeclaration(ExtList children,
TypeReference baseType,
KeYJavaType superType)
ArrayDeclaration
|
Extends(TypeReference supertype)
Extends.
|
FieldDeclaration(Modifier[] mods,
TypeReference typeRef,
FieldSpecification[] vars,
boolean parentIsInterfaceDeclaration)
Field declaration.
|
Implements(TypeReference supertype)
Implements.
|
Implements(TypeReference[] typeRefs)
Implements.
|
InheritanceSpecification(TypeReference supertype)
Inheritance specification.
|
InheritanceSpecification(TypeReference[] supertypes)
Inheritance specification.
|
LocalVariableDeclaration(ImmutableArray<Modifier> mods,
TypeReference typeRef,
VariableSpecification var)
Local variable declaration.
|
LocalVariableDeclaration(ImmutableArray<Modifier> mods,
TypeReference typeRef,
VariableSpecification[] vars)
Local variable declaration.
|
LocalVariableDeclaration(Modifier[] mods,
TypeReference typeRef,
VariableSpecification[] vars)
Local variable declaration.
|
LocalVariableDeclaration(TypeReference typeRef,
VariableSpecification var)
Local variable declaration which declared exactly
one variable.
|
MethodDeclaration(Modifier[] modifiers,
TypeReference returnType,
ProgramElementName name,
ImmutableArray<ParameterDeclaration> parameters,
Throws exceptions,
StatementBlock body,
boolean parentIsInterfaceDeclaration)
Method declaration.
|
MethodDeclaration(Modifier[] modifiers,
TypeReference returnType,
ProgramElementName name,
ParameterDeclaration[] parameters,
Throws exceptions,
StatementBlock body,
boolean parentIsInterfaceDeclaration)
Method declaration.
|
ParameterDeclaration(Modifier[] mods,
TypeReference typeRef,
VariableSpecification var,
boolean parentIsInterfaceDeclaration)
Parameter declaration.
|
ParameterDeclaration(Modifier[] mods,
TypeReference typeRef,
VariableSpecification var,
boolean parentIsInterfaceDeclaration,
boolean parameterIsVarArg)
Parameter declaration.
|
Throws(TypeReference exception)
Throws.
|
Throws(TypeReference[] list)
Throws.
|
VariableDeclaration(ImmutableArray<Modifier> mods,
TypeReference typeRef,
boolean parentIsInterfaceDeclaration)
Variable declaration.
|
VariableDeclaration(Modifier[] mods,
TypeReference typeRef,
boolean parentIsInterfaceDeclaration)
Variable declaration.
|
Modifier and Type | Field and Description |
---|---|
protected TypeReference |
AnnotationUseSpecification.tr |
Modifier and Type | Method and Description |
---|---|
TypeReference |
AnnotationUseSpecification.getTypeReferenceAt(int index) |
Constructor and Description |
---|
AnnotationUseSpecification(TypeReference tr) |
Modifier and Type | Field and Description |
---|---|
protected TypeReference |
TypeOperator.typeReference
Type reference.
|
Modifier and Type | Method and Description |
---|---|
TypeReference |
TypeOperator.getTypeReference()
Get type reference.
|
TypeReference |
TypeOperator.getTypeReferenceAt(int index) |
Constructor and Description |
---|
ExactInstanceof(Expression unaryChild,
TypeReference typeref) |
Instanceof(Expression unaryChild,
TypeReference typeref) |
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.
|
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) |
Modifier and Type | Class and Description |
---|---|
class |
SchemaTypeReference |
class |
TypeRef |
class |
TypeReferenceImp
TypeReferences reference
Type s by name. |
Modifier and Type | Field and Description |
---|---|
protected TypeReference |
ExecutionContext.classContext
the class context
|
protected TypeReference |
MetaClassReference.typeReference
Type reference.
|
Modifier and Type | Method and Description |
---|---|
TypeReference |
MetaClassReference.getTypeReference()
Get type reference.
|
TypeReference |
ExecutionContext.getTypeReference()
returns the type reference to the next enclosing class
|
TypeReference |
IExecutionContext.getTypeReference()
returns the type reference to the next enclosing class
|
TypeReference |
TypeReferenceContainer.getTypeReferenceAt(int index) |
TypeReference |
MetaClassReference.getTypeReferenceAt(int index) |
TypeReference |
MethodReference.getTypeReferenceAt(int index) |
TypeReference |
TypeReferenceImp.getTypeReferenceAt(int index) |
TypeReference |
ArrayReference.getTypeReferenceAt(int index) |
TypeReference |
SuperReference.getTypeReferenceAt(int index) |
TypeReference |
ThisReference.getTypeReferenceAt(int index) |
TypeReference |
SchematicFieldReference.getTypeReferenceAt(int index)
Return the type reference at the specified index in this node's
"virtual" type reference array.
|
TypeReference |
FieldReference.getTypeReferenceAt(int index) |
Constructor and Description |
---|
ExecutionContext(TypeReference classContext,
IProgramMethod methodContext,
ReferencePrefix runtimeInstance)
creates an execution context reference
|
MetaClassReference(TypeReference reference)
Meta class reference.
|
ThisReference(TypeReference outer)
This reference.
|
Modifier and Type | Method and Description |
---|---|
TypeReference |
MethodBodyStatement.getBodySourceAsTypeReference() |
Constructor and Description |
---|
MethodBodyStatement(TypeReference bodySource,
IProgramVariable resultVar,
MethodReference methodReference)
Construct a method body shortcut
|
Modifier and Type | Method and Description |
---|---|
void |
Visitor.performActionOnTypeReference(TypeReference x) |
void |
CreatingASTVisitor.performActionOnTypeReference(TypeReference x) |
void |
JavaASTVisitor.performActionOnTypeReference(TypeReference x) |
Modifier and Type | Interface and Description |
---|---|
interface |
ProgramConstruct
A type that implement this interface can be used in all java
programs instead of an expression or statement.
|
Modifier and Type | Class and Description |
---|---|
class |
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
Modifier and Type | Method and Description |
---|---|
TypeReference |
ProgramSV.getTypeReference() |
TypeReference |
ProgramSV.getTypeReferenceAt(int index) |
Modifier and Type | Class and Description |
---|---|
class |
ArrayLength |
class |
ArrayPostDecl
Replaces a local variable declaration
#t #v[]; with
#t[] #v; |
class |
ConstructorCall
The constructor call meta construct is used to handle a allocation expression
like
new Class(...) . |
class |
CreateObject
If an allocation expression
new Class(...) occurs, a new object
has to be created, in KeY this is quite similar to take it out of a list of
objects and setting the implicit flag <created> to
true as well as setting all fields of the object to their
default values. |
class |
DoBreak
This class performs a labeled break.
|
class |
EnhancedForElimination
This class defines a meta operator to resolve an enhanced for loop - by transformation to a
"normal" loop.
|
class |
EvaluateArgs
TODO
|
class |
ExpandMethodBody
Replaces the MethodBodyStatement shortcut with the full body, performs prefix
adjustments in the body (execution context).
|
class |
ForInitUnfoldTransformer
Pulls the initializor out of a for-loop.
|
class |
ForToWhile
converts a for-loop to a while loop.
|
class |
InitArray
Split an array creation expression with explicit array initializer,
creating a creation expression with dimension expression and a list
of assignments (-> Java language specification, 15.10)
|
class |
InitArrayCreation
Split an array creation expression with explicit array initializer, creating
a creation expression with dimension expression and a list of assignments (->
Java language specification, 15.10)
This meta construct delivers the creation expression
|
class |
IsStatic
Creates a true or false literal if the given program element is or is not a
static variable reference.
|
class |
MethodCall
Symbolically executes a method invocation
|
class |
MultipleVarDecl
Replaces a declaration of multiple variables by two variable declarations
where the first one declares a single variable and the second one the
remaining variables.
|
class |
PostWork
creates an assignment instantiationOf(#newObjectsV).
|
class |
ProgramTransformer
ProgramTransformers are used to describe schematic transformations
that cannot be expressed by the taclet language itself.
|
class |
ReattachLoopInvariant
Construct for re-attaching a loop invariant that otherwise would get lost
after a transformation, for instance, the loop scope-based unwinding rule.
|
class |
SpecialConstructorCall
The constructor call meta construct is used to handle a allocation expression
like
new Class(...) . |
class |
StaticInitialisation |
class |
SwitchToIf
This class is used to perform program transformations needed for the symbolic
execution of a switch-case statement.
|
class |
TypeOf |
class |
Unpack |
class |
UnwindLoop
This class is used to perform program transformations needed for the symbolic
execution of a loop.
|
Modifier and Type | Method and Description |
---|---|
TypeReference |
ProgramTransformer.getTypeReferenceAt(int index) |
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)
|
Modifier and Type | Method and Description |
---|---|
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractReturnVariableValueSequent(Services services,
TypeReference contextObjectType,
IProgramMethod contextMethod,
ReferencePrefix contextObject,
Node methodReturnNode,
Node methodCallEmptyNode,
IProgramVariable variable)
Creates a
Sequent which can be used in site proofs to
extract the return value of the given IProgramVariable from the
sequent of the given Node . |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
KeYTypeUtil.resolveType(TypeReference typeReference)
Resolves the type of the given
TypeReference . |
Copyright © 2003-2019 The KeY-Project.