Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
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.reference |
Elements of the Java syntax tree representing implicit or explicit (named)
references to other program elements.
|
de.uka.ilkd.key.java.statement |
Elements of the Java syntax tree representing pure statements.
|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.symbolic_execution.slicing | |
de.uka.ilkd.key.symbolic_execution.util |
Modifier and Type | Method and Description |
---|---|
static ArrayReference |
KeYJavaASTFactory.arrayFieldAccess(ReferencePrefix array,
Expression index)
Create an array field access with a single index.
|
static FieldReference |
KeYJavaASTFactory.arrayLength(JavaInfo model,
ReferencePrefix array)
Create an array length access.
|
static CopyAssignment |
KeYJavaASTFactory.assignArrayField(ProgramVariable variable,
ReferencePrefix array,
Expression index)
Create a statement that assigns an array element to a variable.
|
static Expression |
KeYJavaASTFactory.attribute(ReferencePrefix prefix,
ProgramVariable field)
creates an attribute access
prefix.field |
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.declareMethodCall(IProgramVariable variable,
ReferencePrefix reference,
java.lang.String method)
Create a local variable declaration that assigns a method's return value
initially.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.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 ExecutionContext |
KeYJavaASTFactory.executionContext(KeYJavaType classType,
IProgramMethod method,
ReferencePrefix reference)
Create an execution context.
|
static FieldReference |
KeYJavaASTFactory.fieldReference(ReferencePrefix prefix,
ProgramVariable field)
Create a field access.
|
static IGuard |
KeYJavaASTFactory.lessThanArrayLengthGuard(JavaInfo model,
ProgramVariable variable,
ReferencePrefix array)
Create a condition that compares a variable and an array length using the
less than operator.
|
static MethodBodyStatement |
KeYJavaASTFactory.methodBody(JavaInfo model,
ProgramVariable result,
ReferencePrefix reference,
KeYJavaType classType,
java.lang.String methodName,
ProgramVariable[] arguments)
Create a method body shortcut.
|
static MethodBodyStatement |
KeYJavaASTFactory.methodBody(ProgramVariable result,
ReferencePrefix reference,
IProgramMethod method,
Expression[] arguments)
Create a method body shortcut.
|
static MethodBodyStatement |
KeYJavaASTFactory.methodBody(ProgramVariable result,
ReferencePrefix reference,
IProgramMethod method,
ImmutableArray<Expression> arguments)
Create a method body shortcut.
|
static MethodReference |
KeYJavaASTFactory.methodCall(ReferencePrefix reference,
MethodName name,
Expression... args)
Create a method call.
|
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)
Create a method call with no arguments.
|
static MethodReference |
KeYJavaASTFactory.methodCall(ReferencePrefix reference,
java.lang.String name,
Expression... args)
Create a method call.
|
static MethodReference |
KeYJavaASTFactory.methodCall(ReferencePrefix reference,
java.lang.String name,
ImmutableArray<? extends Expression> args)
Create a method call.
|
static New |
KeYJavaASTFactory.newOperator(ReferencePrefix referencePrefix,
KeYJavaType type)
Create an object allocation without arguments.
|
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 SuperConstructorReference |
KeYJavaASTFactory.superConstructor(ReferencePrefix referencePrefix,
Expression[] args)
Create a call to the super constructor.
|
Modifier and Type | Class and Description |
---|---|
class |
ParenthesizedExpression
Redundant Parentheses.
|
class |
PassiveExpression
Marks an active statement as inactive.
|
Modifier and Type | Method and Description |
---|---|
ReferencePrefix |
ParenthesizedExpression.getReferencePrefix()
We do not have a prefix, so fake it!
This way we implement ReferencePrefix
|
ReferencePrefix |
ParenthesizedExpression.setReferencePrefix(ReferencePrefix r) |
Modifier and Type | Method and Description |
---|---|
ReferencePrefix |
ParenthesizedExpression.setReferencePrefix(ReferencePrefix r) |
Modifier and Type | Class and Description |
---|---|
class |
StringLiteral |
Modifier and Type | Method and Description |
---|---|
ReferencePrefix |
StringLiteral.getReferencePrefix()
We do not have a prefix, so fake it!
This way we implement ReferencePrefix
|
ReferencePrefix |
StringLiteral.setReferencePrefix(ReferencePrefix r) |
Modifier and Type | Method and Description |
---|---|
ReferencePrefix |
StringLiteral.setReferencePrefix(ReferencePrefix r) |
Modifier and Type | Class and Description |
---|---|
class |
New
The object allocation operator.
|
class |
NewArray
The array allocation operator.
|
Modifier and Type | Field and Description |
---|---|
protected ReferencePrefix |
New.accessPath |
Modifier and Type | Method and Description |
---|---|
ReferencePrefix |
New.getReferencePrefix()
Get reference prefix.
|
ReferencePrefix |
NewArray.getReferencePrefix()
We do not have a prefix, so fake it!
This way we implement ReferencePrefix
|
ReferencePrefix |
New.setReferencePrefix(ReferencePrefix r) |
Modifier and Type | Method and Description |
---|---|
ReferencePrefix |
New.setReferencePrefix(ReferencePrefix r) |
Constructor and Description |
---|
New(Expression[] arguments,
TypeReference type,
ReferencePrefix rp)
Constructor for the transformation of COMPOST ASTs to KeY.
|
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.
|
Modifier and Type | Interface and Description |
---|---|
interface |
ConstructorReference
Constructor reference.
|
interface |
MethodOrConstructorReference |
interface |
TypeReference
TypeReferences reference
Type s by name. |
interface |
TypeReferenceInfix
ReferencePrefix and -suffix that is admissible for outer type references.
|
Modifier and Type | Class and Description |
---|---|
class |
ArrayReference
Array reference.
|
class |
FieldReference |
class |
MetaClassReference
Meta class reference.
|
class |
MethodReference
Method reference.
|
class |
PackageReference
Package reference.
|
class |
SchematicFieldReference
Field reference.
|
class |
SchemaTypeReference |
class |
SpecialConstructorReference
Occurs in a constructor declaration as the first statement
as this(...) or super(...) reference.
|
class |
SuperConstructorReference
Super constructor reference.
|
class |
SuperReference
Super reference.
|
class |
ThisConstructorReference
This constructor reference.
|
class |
ThisReference
A reference to the current object.
|
class |
TypeRef |
class |
TypeReferenceImp
TypeReferences reference
Type s by name. |
class |
VariableReference |
Modifier and Type | Field and Description |
---|---|
protected ReferencePrefix |
ArrayLengthReference.prefix
Reference prefix.
|
protected ReferencePrefix |
MethodReference.prefix
Access path.
|
protected ReferencePrefix |
SuperConstructorReference.prefix
Access path to enclosing class.
|
protected ReferencePrefix |
TypeReferenceImp.prefix
Prefix.
|
protected ReferencePrefix |
PackageReference.prefix
Prefix.
|
protected ReferencePrefix |
ArrayReference.prefix
Access path.
|
protected ReferencePrefix |
FieldReference.prefix
Reference prefix.
|
protected ReferencePrefix |
ExecutionContext.runtimeInstance
the reference to the active object
|
Modifier and Type | Method and Description |
---|---|
ReferencePrefix |
ArrayLengthReference.getReferencePrefix()
Get reference prefix.
|
ReferencePrefix |
ThisConstructorReference.getReferencePrefix() |
ReferencePrefix |
MetaClassReference.getReferencePrefix()
Get reference prefix.
|
ReferencePrefix |
ReferencePrefix.getReferencePrefix() |
ReferencePrefix |
MethodReference.getReferencePrefix()
Get reference prefix.
|
ReferencePrefix |
SuperConstructorReference.getReferencePrefix() |
ReferencePrefix |
TypeReferenceImp.getReferencePrefix()
Get reference prefix.
|
ReferencePrefix |
PackageReference.getReferencePrefix()
Get reference prefix.
|
ReferencePrefix |
ArrayReference.getReferencePrefix()
Get reference prefix.
|
ReferencePrefix |
SuperReference.getReferencePrefix()
Get reference prefix.
|
ReferencePrefix |
ThisReference.getReferencePrefix()
Get reference prefix.
|
ReferencePrefix |
VariableReference.getReferencePrefix()
We do not have a prefix, so fake it!
This way we implement ReferencePrefix
|
ReferencePrefix |
SchematicFieldReference.getReferencePrefix()
Get reference prefix.
|
ReferencePrefix |
TypeReference.getReferencePrefix() |
ReferencePrefix |
FieldReference.getReferencePrefix()
Get reference prefix.
|
ReferencePrefix |
ExecutionContext.getRuntimeInstance()
returns the runtime instance object
|
ReferencePrefix |
IExecutionContext.getRuntimeInstance()
returns the runtime instance object
|
ReferencePrefix |
MetaClassReference.setReferencePrefix(ReferencePrefix r) |
ReferencePrefix |
PackageReference.setReferencePrefix(ReferencePrefix r) |
ReferencePrefix |
ArrayReference.setReferencePrefix(ReferencePrefix r) |
ReferencePrefix |
SuperReference.setReferencePrefix(ReferencePrefix r) |
ReferencePrefix |
ThisReference.setReferencePrefix(ReferencePrefix r) |
ReferencePrefix |
VariableReference.setReferencePrefix(ReferencePrefix r) |
ReferencePrefix |
SchematicFieldReference.setReferencePrefix(ReferencePrefix rp)
Set reference prefix.
|
ReferencePrefix |
FieldReference.setReferencePrefix(ReferencePrefix rp)
Set reference prefix.
|
Modifier and Type | Method and Description |
---|---|
ReferencePrefix |
MetaClassReference.setReferencePrefix(ReferencePrefix r) |
ReferencePrefix |
PackageReference.setReferencePrefix(ReferencePrefix r) |
ReferencePrefix |
ArrayReference.setReferencePrefix(ReferencePrefix r) |
ReferencePrefix |
SuperReference.setReferencePrefix(ReferencePrefix r) |
ReferencePrefix |
ThisReference.setReferencePrefix(ReferencePrefix r) |
ReferencePrefix |
VariableReference.setReferencePrefix(ReferencePrefix r) |
ReferencePrefix |
SchematicFieldReference.setReferencePrefix(ReferencePrefix rp)
Set reference prefix.
|
ReferencePrefix |
FieldReference.setReferencePrefix(ReferencePrefix rp)
Set reference prefix.
|
Modifier and Type | Method and Description |
---|---|
ReferencePrefix |
MethodBodyStatement.getDesignatedContext() |
Constructor and Description |
---|
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 | 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 |
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 |
---|---|
ReferencePrefix |
ProgramVariable.getReferencePrefix()
We do not have a prefix, so fake it!
This way we implement ReferencePrefix
|
ReferencePrefix |
ProgramSV.getReferencePrefix() |
ReferencePrefix |
ProgramSV.getRuntimeInstance() |
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 ReferencePrefix |
MethodCall.newContext |
Modifier and Type | Method and Description |
---|---|
ReferencePrefix |
ProgramTransformer.getReferencePrefix() |
ReferencePrefix |
ProgramTransformer.setReferencePrefix(ReferencePrefix r) |
Modifier and Type | Method and Description |
---|---|
protected void |
InitArray.createArrayAssignments(int p_start,
Statement[] p_statements,
ProgramVariable[] p_initializers,
ReferencePrefix p_array,
NewArray p_creationExpression)
Convert the variable initializers to assignments to the array
elements (the initializers may itself be array initializers, in
which case valid creation expressions are created by inserting
the new-operator)
|
protected 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)
|
ReferencePrefix |
ProgramTransformer.setReferencePrefix(ReferencePrefix r) |
Modifier and Type | Method and Description |
---|---|
ReferencePrefix |
AbstractSlicer.SequentInfo.getThisReference()
Returns the this reference if available.
|
protected ReferencePrefix |
AbstractSlicer.toReferencePrefix(SourceElement sourceElement)
Computes the
ReferencePrefix of the given SourceElement . |
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractSlicer.analyzeEquality(Services services,
Term equality,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Analyzes the given equality
Term for aliased locations. |
protected void |
AbstractSlicer.analyzeEquivalenceClasses(Services services,
ImmutableList<ISymbolicEquivalenceClass> sec,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Analyzes the gievn
ISymbolicEquivalenceClass es. |
protected void |
AbstractSlicer.analyzeHeapUpdate(Term term,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Recursive utility method used by
#analyzeUpdate(Term, Services, HeapLDT, Map) to analyze a given update. |
protected void |
AbstractSlicer.analyzeSequent(Services services,
Sequent sequent,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Analyzes the given
Sequent for equalities specified by top level formulas. |
protected void |
AbstractSlicer.analyzeUpdate(Term term,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext ec,
ReferencePrefix thisReference)
Recursive utility method used by
#analyzeUpdates(ImmutableList, Services, HeapLDT, Map) to analyze a given update. |
protected void |
AbstractSlicer.analyzeUpdates(ImmutableList<Term> updates,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext ec,
ReferencePrefix thisReference)
Utility method used by
#analyzeSequent(Node) to analyze the given updates. |
protected void |
AbstractSlicer.listModifiedHeapLocations(Term term,
Services services,
HeapLDT heapLDT,
java.util.List<Location> listToFill,
ReferencePrefix thisReference,
java.util.Set<Location> relevantLocations,
Node node)
Recursive utility method used by
#listModifiedLocations(Term, Services, HeapLDT, List, ReferencePrefix) to analyze a given update. |
protected void |
AbstractSlicer.listModifiedLocations(Term term,
Services services,
HeapLDT heapLDT,
java.util.List<Location> listToFill,
ExecutionContext ec,
ReferencePrefix thisReference,
java.util.Set<Location> relevantLocations,
Node node)
|
protected Location |
AbstractSlicer.normalizeAlias(Services services,
ReferencePrefix referencePrefix,
AbstractSlicer.SequentInfo info)
Returns the representative alias for the given
ReferencePrefix . |
protected boolean |
AbstractSlicer.removeRelevant(Services services,
ReferencePrefix sourceElement,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info)
Checks if the given
SourceElement is directly or indirectly
contained (aliased) in the Set of relevant locations. |
ImmutableArray<Node> |
AbstractSlicer.slice(Node seedNode,
ReferencePrefix seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the slice.
|
protected Location |
AbstractSlicer.toLocation(Services services,
ReferencePrefix prefix,
ExecutionContext ec,
ReferencePrefix thisReference)
Converts the given
ReferencePrefix into a Location . |
protected ImmutableList<Access> |
AbstractSlicer.toLocationRecursive(Services services,
ReferencePrefix prefix,
ExecutionContext ec,
ReferencePrefix thisReference,
ImmutableList<Access> children)
Utility method used by
#toLocation(Services, ReferencePrefix, ReferencePrefix)
to recursively extract the Access instances. |
protected void |
AbstractSlicer.updateAliases(Services services,
Location first,
Location second,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Adds the found alias consisting of first and second
ReferencePrefix to the alias Map . |
protected java.util.Set<Location> |
AbstractBackwardSlicer.updateOutdatedLocations(Services services,
java.util.Set<Location> oldLocationsToUpdate,
java.util.Map<Location,java.util.SortedSet<Location>> newAliases,
java.util.Map<Location,java.util.SortedSet<Location>> oldAliases,
Location outdatedPrefix,
ReferencePrefix thisReference)
Updates the outdated locations.
|
Constructor and Description |
---|
SequentInfo(java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext executionContext,
ReferencePrefix thisReference)
Constructor.
|
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 . |
Copyright © 2003-2019 The KeY-Project.