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.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.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.logic.sort |
This package contains different kinds and implementations subtyping interface Sort.
|
de.uka.ilkd.key.macros | |
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.proof_references.analyst | |
de.uka.ilkd.key.proof.io |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.inst |
contains classes for the instantiation of schema variables of
Taclet s. |
de.uka.ilkd.key.rule.match.legacy | |
de.uka.ilkd.key.rule.match.vm | |
de.uka.ilkd.key.rule.match.vm.instructions | |
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 | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Interface and Description |
---|---|
interface |
Declaration
Declaration.
|
interface |
Expression
Expression
taken from COMPOST and changed to achieve an immutable structure
|
interface |
ExpressionContainer
Expression container.
|
interface |
Label |
interface |
LoopInitializer
Loop initializer.
|
interface |
NamedProgramElement
Named program element.
|
interface |
NonTerminalProgramElement
Non terminal program element.
|
interface |
ParameterContainer
Describes program elements that contain
ParameterDeclaration s. |
interface |
ProgramVariableName |
interface |
Reference
References are uses of names, variables or members.
|
interface |
ScopeDefiningElement
The property of a non terminal program element to define a scope.
|
interface |
Statement
Statement.
|
interface |
StatementContainer
Statement container.
|
interface |
TerminalProgramElement
Terminal program element.
|
interface |
TypeScope
The property of a non terminal program element to define a scope for
types.
|
interface |
VariableScope
The property of a non terminal program element to define a scope for
variables.
|
Modifier and Type | Class and Description |
---|---|
class |
CcatchBreakLabelParameterDeclaration
A "\Break label" parameter declaration of a ccatch clause.
|
class |
CcatchBreakParameterDeclaration
A "\Break" parameter declaration of a ccatch clause.
|
class |
CcatchBreakWildcardParameterDeclaration
A "\Break *" parameter declaration of a ccatch clause.
|
class |
CcatchContinueLabelParameterDeclaration
A "\Continue label" parameter declaration of a ccatch clause.
|
class |
CcatchContinueParameterDeclaration
A "\Continue" parameter declaration of a ccatch clause.
|
class |
CcatchContinueWildcardParameterDeclaration
A "\Continue *" parameter declaration of a ccatch clause.
|
class |
CcatchNonstandardParameterDeclaration
A "non-standard" parameter declaration of a Ccatch clause, e.g., "\Return".
|
class |
CcatchReturnParameterDeclaration
A "\Return" parameter declaration of a ccatch clause.
|
class |
CcatchReturnValParameterDeclaration
A "\Return int v" parameter declaration of a ccatch clause.
|
class |
CompilationUnit
A node representing a single source file containing
TypeDeclaration s and an optional PackageSpecification
and an optional set of Import s. |
class |
ContextStatementBlock
In the DL-formulae description of Taclets the program part can have
the following form < pi alpha;...; omega > Phi where pi is a prefix
consisting of open brackets, try's and so on and omega is the rest
of the program.
|
class |
Import
Import.
|
class |
JavaNonTerminalProgramElement
Top level implementation of a Java
NonTerminalProgramElement . |
class |
JavaProgramElement
Top level implementation of a Java
ProgramElement . |
class |
PackageSpecification
Package specification.
|
class |
StatementBlock
Statement block.
|
Modifier and Type | Method and Description |
---|---|
ProgramElement |
Recoder2KeYConverter.convert(JavaProgramElement pe)
The default procedure.
|
ProgramElement |
Recoder2KeYConverter.convert(UncollatedReferenceQualifier urq)
if an UncollatedReferenceQualifier appears throw a ConvertExceception
because these qualifiers have to be resolved by running the
CrossReferencer
|
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.
|
ProgramElement |
CcatchReturnValParameterDeclaration.getChildAt(int index)
Returns the child at the specified index in this node's "virtual" child
array
|
ProgramElement |
CcatchReturnParameterDeclaration.getChildAt(int index) |
ProgramElement |
PackageSpecification.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
CcatchContinueWildcardParameterDeclaration.getChildAt(int index) |
ProgramElement |
ContextStatementBlock.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
Import.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
CcatchBreakWildcardParameterDeclaration.getChildAt(int index) |
ProgramElement |
NonTerminalProgramElement.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array.
|
ProgramElement |
CcatchContinueLabelParameterDeclaration.getChildAt(int index) |
ProgramElement |
CcatchContinueParameterDeclaration.getChildAt(int index) |
ProgramElement |
CcatchBreakParameterDeclaration.getChildAt(int index) |
ProgramElement |
StatementBlock.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
CompilationUnit.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
CcatchBreakLabelParameterDeclaration.getChildAt(int index) |
ProgramElement |
SourceData.getElement()
returns always the parent node
|
ProgramElement |
SourceData.getSource()
returns the element to be matched, i.e.
|
ProgramElement |
Recoder2KeYConverter.process(ProgramElement pe) |
ProgramElement |
JavaInfo.readJava(java.lang.String java)
reads a Java statement not necessarily a block
|
ProgramElement |
KeYRecoderMapping.toKeY(ProgramElement pe)
returns a matching ProgramElement (KeY) to a given
ProgramElement (Recoder)
|
Modifier and Type | Method and Description |
---|---|
Term |
TypeConverter.convertToLogicElement(ProgramElement pe) |
Term |
TypeConverter.convertToLogicElement(ProgramElement pe,
ExecutionContext ec) |
protected int |
JavaNonTerminalProgramElement.getArrayPos(ImmutableArray<ProgramElement> arr,
ProgramElement el)
returns the index of element el in array arr
|
static MethodFrame |
JavaTools.getInnermostMethodFrame(ProgramElement pe,
Services services)
Returns the innermost method frame of the passed java block
|
protected void |
PrettyPrinter.printFooter(ProgramElement x)
Print program element footer.
|
protected void |
PrettyPrinter.printHeader(int lf,
int levelChange,
int blanks,
ProgramElement x)
Print program element header.
|
protected void |
PrettyPrinter.printHeader(int lf,
int blanks,
ProgramElement elem)
Print program element header.
|
protected void |
PrettyPrinter.printHeader(int blanks,
ProgramElement elem)
Print program element header.
|
protected void |
PrettyPrinter.printHeader(ProgramElement elem)
Print program element header.
|
void |
SourceData.setElement(ProgramElement element)
sets the parent node
|
ProgramElement |
KeYRecoderMapping.toRecoder(ProgramElement pe)
returns the Recoder-equivalent to a given ProgramElement (KeY).
|
Modifier and Type | Method and Description |
---|---|
protected int |
JavaNonTerminalProgramElement.getArrayPos(ImmutableArray<ProgramElement> arr,
ProgramElement el)
returns the index of element el in array arr
|
protected void |
PrettyPrinter.writeBlockList(ImmutableArray<? extends ProgramElement> list)
Write block list.
|
protected void |
PrettyPrinter.writeBlockList(int firstLF,
int levelChange,
int firstBlanks,
ImmutableArray<? extends ProgramElement> list)
Write a complete ArrayOf
|
protected void |
PrettyPrinter.writeCommaList(ImmutableArray<? extends ProgramElement> list)
Write comma list.
|
protected void |
PrettyPrinter.writeCommaList(int separationBlanks,
ImmutableArray<? extends ProgramElement> list)
Write comma list.
|
protected void |
PrettyPrinter.writeCommaList(int firstLF,
int levelChange,
int firstBlanks,
ImmutableArray<? extends ProgramElement> list)
Write a complete ArrayOf
|
protected void |
PrettyPrinter.writeImmutableArrayOfProgramElement(int firstLF,
int levelChange,
int firstBlanks,
java.lang.String separationSymbol,
int separationLF,
int separationBlanks,
ImmutableArray<? extends ProgramElement> list)
Write a complete ArrayOf
|
protected void |
PrettyPrinter.writeKeywordList(ImmutableArray<? extends ProgramElement> list)
Write keyword list.
|
protected void |
PrettyPrinter.writeKeywordList(int firstLF,
int levelChange,
int firstBlanks,
ImmutableArray<? extends ProgramElement> list)
Write a complete ArrayOf
|
protected void |
PrettyPrinter.writeLineList(ImmutableArray<? extends ProgramElement> list)
Write line list.
|
protected void |
PrettyPrinter.writeLineList(int firstLF,
int levelChange,
int firstBlanks,
ImmutableArray<? extends ProgramElement> list)
Write a complete ArrayOf
|
Constructor and Description |
---|
SourceData(ProgramElement element,
int childPos,
Services services)
creates a new source data object with parent node element whose
childPos-th child has to be matched (-1 denotes element itself
has to be matched
|
Modifier and Type | Interface and Description |
---|---|
interface |
MemberDeclaration
Member declaration.
|
interface |
TypeDeclarationContainer
Type declaration container.
|
Modifier and Type | Class and Description |
---|---|
class |
ArrayDeclaration
KeY used to model arrays using only the
ArrayType . |
class |
ClassDeclaration
There are several types of class declarations:
package-less outer classes
getClassContainer() == null
getStatementContainer() == null
getName() != null
ordinary outer classes
getClassContainer() instanceof Package
getStatementContainer() == null
getName() != null
member classes
getClassContainer() instanceof ClassDeclaration
getStatementContainer() == null
getName() != null
local class
getClassContainer() == null
getStatementContainer() != null
getName() != null
local anonymous class
getClassContainer() == null
getStatementContainer() instanceof expression.New
getName() == null
Anonymous local classes have exactly one supertype and no
subtypes.
|
class |
ClassInitializer |
class |
ConstructorDeclaration
The getTypeReference method returns null - constructors do not have
explicite return types.
|
class |
EnumClassDeclaration
This class is used for wrapping an enum into a standard class type.
|
class |
Extends
Extends.
|
class |
FieldDeclaration
Field declaration.
|
class |
FieldSpecification |
class |
Implements
Implements.
|
class |
ImplicitFieldSpecification |
class |
InheritanceSpecification
Inheritance specification.
|
class |
InterfaceDeclaration
Interface declaration.
|
class |
JavaDeclaration
Java declaration.
|
class |
LocalVariableDeclaration
Local variable declaration.
|
class |
MethodDeclaration
Method declaration.
|
class |
Modifier
Modifier.
|
class |
ParameterDeclaration
Formal parameters require a VariableSpecificationList of size() <= 1
(size() == 0 for abstract methods) without initializer (for Java).
|
class |
SuperArrayDeclaration
At the moment the mere purpose of this Class is to provide an encapsulation
for the length attribute.
|
class |
Throws
Throws.
|
class |
TypeDeclaration
Type declaration.
|
class |
VariableDeclaration
Variable declaration.
|
class |
VariableSpecification
Variable specification that defines a variable name.
|
Modifier and Type | Method and Description |
---|---|
ProgramElement |
InterfaceDeclaration.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
LocalVariableDeclaration.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
ArrayDeclaration.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
ClassDeclaration.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
Throws.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
VariableSpecification.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
FieldDeclaration.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
ClassInitializer.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
InheritanceSpecification.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
ParameterDeclaration.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
MethodDeclaration.getChildAt(int index) |
ProgramElement |
SuperArrayDeclaration.getChildAt(int i) |
Modifier and Type | Class and Description |
---|---|
class |
Abstract
Abstract.
|
class |
AnnotationUseSpecification |
class |
Final
Final.
|
class |
Ghost
The JML modifier "ghost".
|
class |
Model
The JML modifier "model".
|
class |
Native
Native.
|
class |
NoState
The JML modifier "no_state".
|
class |
Private
Private.
|
class |
Protected
Protected.
|
class |
Public
Public.
|
class |
Static
Static.
|
class |
StrictFp
Strict fp.
|
class |
Synchronized
Synchronized.
|
class |
Transient
Transient.
|
class |
TwoState
The JML modifier "two_state".
|
class |
VisibilityModifier
Visibility modifier.
|
class |
Volatile
Volatile.
|
Modifier and Type | Method and Description |
---|---|
ProgramElement |
AnnotationUseSpecification.getChildAt(int index) |
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 | Method and Description |
---|---|
ProgramElement |
ArrayInitializer.getChildAt(int index) |
ProgramElement |
Operator.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
ParenthesizedExpression.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
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 |
---|---|
ProgramElement |
ExactInstanceof.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
TypeCast.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
Instanceof.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
New.getChildAt(int index) |
ProgramElement |
NewArray.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
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 |
Modifier and Type | Interface and Description |
---|---|
interface |
ConstructorReference
Constructor reference.
|
interface |
IExecutionContext
extracted interface to allow schema variabes to stand for an
execution context
|
interface |
MemberReference
Member reference.
|
interface |
MethodName
Method name.
|
interface |
MethodOrConstructorReference |
interface |
NameReference
A NameReference references an entity by its explicite name.
|
interface |
PackageReferenceContainer
Element that contains a PackageReference.
|
interface |
ReferencePrefix
Reference prefix.
|
interface |
ReferenceSuffix
Reference suffix.
|
interface |
TypeReference
TypeReferences reference
Type s by name. |
interface |
TypeReferenceContainer
Type reference container.
|
interface |
TypeReferenceInfix
ReferencePrefix and -suffix that is admissible for outer type references.
|
Modifier and Type | Class and Description |
---|---|
class |
ArrayLengthReference
Array length reference.
|
class |
ArrayReference
Array reference.
|
class |
ExecutionContext |
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 | Method and Description |
---|---|
ProgramElement |
ArrayLengthReference.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
MetaClassReference.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
MethodReference.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
TypeReferenceImp.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
PackageReference.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
ExecutionContext.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array.
|
ProgramElement |
ArrayReference.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
SuperReference.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
ThisReference.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
SpecialConstructorReference.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
VariableReference.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
SchematicFieldReference.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
FieldReference.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
SchemaTypeReference.getConcreteProgramElement(Services services) |
Modifier and Type | Interface and Description |
---|---|
interface |
Branch
Branch.
|
interface |
IForUpdates |
interface |
IGuard |
interface |
ILoopInit |
Modifier and Type | Class and Description |
---|---|
class |
Assert |
class |
BranchImp
Branch.
|
class |
BranchStatement
Branch statement.
|
class |
Break
Break.
|
class |
Case
Case.
|
class |
Catch
Catch.
|
class |
CatchAllStatement |
class |
Ccatch
Ccatch.
|
class |
Continue
Continue.
|
class |
Default
Default.
|
class |
Do
Do.
|
class |
Else
Else.
|
class |
EmptyStatement
Empty statement.
|
class |
EnhancedFor
The new enhanced form of a for-loop.
|
class |
Exec
Exec.
|
class |
ExpressionJumpStatement
Expression jump statement.
|
class |
Finally
Finally.
|
class |
For
For.
|
class |
ForUpdates |
class |
Guard |
class |
If
If.
|
class |
JavaStatement
Default implementation for non-terminal Java statements.
|
class |
JumpStatement
Jump statement.
|
class |
LabeledStatement
Labeled statement.
|
class |
LabelJumpStatement
Label jump statement.
|
class |
LoopInit |
class |
LoopScopeBlock
Loop scope block.
|
class |
LoopStatement
Loop statement.
|
class |
MergePointStatement
A statement indicating a merge point.
|
class |
MethodBodyStatement
A shortcut-statement for a method body, i.e.
|
class |
MethodFrame
The statement inserted by KeY if a method call is executed.
|
class |
Return
Return.
|
class |
Switch
Switch.
|
class |
SynchronizedBlock
Synchronized block.
|
class |
Then
Then.
|
class |
Throw
Throw.
|
class |
TransactionStatement |
class |
Try
Try.
|
class |
While
While.
|
Modifier and Type | Method and Description |
---|---|
ProgramElement |
MethodBodyStatement.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array.
|
ProgramElement |
LoopStatement.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
Catch.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
Switch.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
Exec.getChildAt(int index)
Returns the child at the specified index in this node's "virtual" child
array
|
ProgramElement |
LoopScopeBlock.getChildAt(int index)
Returns the child at the specified index in this node's "virtual" child
array
|
ProgramElement |
MethodFrame.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
CatchAllStatement.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array.
|
ProgramElement |
LoopInit.getChildAt(int index) |
ProgramElement |
MergePointStatement.getChildAt(int index)
Returns the child at the specified index in this node's "virtual" child
array
|
ProgramElement |
ForUpdates.getChildAt(int index) |
ProgramElement |
Finally.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
Default.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
Try.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
SynchronizedBlock.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
Guard.getChildAt(int index) |
ProgramElement |
LabeledStatement.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
Then.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
Assert.getChildAt(int index) |
ProgramElement |
LabelJumpStatement.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
Else.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
Ccatch.getChildAt(int index)
Returns the child at the specified index in this node's "virtual" child
array
|
ProgramElement |
TransactionStatement.getChildAt(int index) |
ProgramElement |
ExpressionJumpStatement.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
Case.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
ProgramElement |
If.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array
|
Constructor and Description |
---|
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 | Field and Description |
---|---|
protected ProgramElement |
CreatingASTVisitor.DefaultAction.pe |
Modifier and Type | Method and Description |
---|---|
ProgramElement |
ProgramElementReplacer.replace(ProgramElement oldElement,
ProgramElement newElement) |
ProgramElement |
ProgVarReplaceVisitor.result() |
ProgramElement |
FieldReplaceVisitor.result() |
ProgramElement |
ProgramReplaceVisitor.result() |
ProgramElement |
JavaASTWalker.root()
returns start point of the walker
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<ProgramElement> |
JavaASTCollector.getNodes()
returns the found nodes of the specified type
|
Modifier and Type | Method and Description |
---|---|
protected void |
ProgVarReplaceVisitor.doAction(ProgramElement node)
the action that is performed just before leaving the node the last time
|
protected void |
JavaASTCollector.doAction(ProgramElement node)
the action that is performed just before leaving the node the
last time
|
protected void |
LabelCollector.doAction(ProgramElement node) |
void |
CreatingASTVisitor.DefaultAction.doAction(ProgramElement x) |
protected void |
JavaASTVisitor.doAction(ProgramElement node)
the action that is performed just before leaving the node the last time
|
protected void |
ProgramElementReplacer.doAction(ProgramElement element) |
protected void |
OuterBreakContinueAndReturnCollector.doAction(ProgramElement node) |
protected void |
ProgramSVCollector.doAction(ProgramElement node)
the action that is performed just before leaving the node the last time.
|
protected abstract void |
JavaASTWalker.doAction(ProgramElement node)
the action that is performed just before leaving the node the
last time
|
protected void |
ProgramReplaceVisitor.doAction(ProgramElement node)
the action that is performed just before leaving the node the last time
|
boolean |
FreeLabelFinder.findLabel(Label label,
ProgramElement node) |
protected static int |
CreatingASTVisitor.getPosition(NonTerminalProgramElement pe1,
ProgramElement pe2)
returns the position of pe2 in the virtual child array of pe1
|
ProgramElement |
ProgramElementReplacer.replace(ProgramElement oldElement,
ProgramElement newElement) |
protected void |
ProgVarReplaceVisitor.walk(ProgramElement node) |
protected void |
OuterBreakContinueAndReturnReplacer.walk(ProgramElement node) |
protected void |
InnerBreakAndContinueReplacer.walk(ProgramElement node) |
protected void |
CreatingASTVisitor.walk(ProgramElement node) |
protected void |
JavaASTVisitor.walk(ProgramElement node) |
protected void |
OuterBreakContinueAndReturnCollector.walk(ProgramElement node) |
protected void |
JavaASTWalker.walk(ProgramElement node)
walks through the AST.
|
Modifier and Type | Method and Description |
---|---|
protected void |
CreatingASTVisitor.addChildren(ImmutableArray<ProgramElement> arr) |
Constructor and Description |
---|
ContainsStatementVisitor(ProgramElement root,
SourceElement toSearch,
Services services)
Constructor.
|
CreatingASTVisitor(ProgramElement root,
boolean preservesPos,
Services services)
create the CreatingASTVisitor
|
DeclarationProgramVariableCollector(ProgramElement root,
Services services)
creates a new declaration visitor
|
DefaultAction(ProgramElement pe) |
FieldReplaceVisitor(ProgramElement pe,
Services services) |
JavaASTCollector(ProgramElement root,
java.lang.Class<?> type)
create the JavaASTWalker
|
JavaASTVisitor(ProgramElement root,
Services services)
create the JavaASTVisitor
|
JavaASTWalker(ProgramElement root)
create the JavaASTWalker
|
LabelCollector(ProgramElement root,
Services services) |
OuterBreakContinueAndReturnCollector(ProgramElement root,
java.util.List<Label> alwaysInnerLabels,
Services services) |
ProgramReplaceVisitor(ProgramElement root,
Services services,
SVInstantiations svi)
create the ProgramReplaceVisitor
|
ProgramSVCollector(ProgramElement root,
ImmutableList<SchemaVariable> vars)
create the ProgramSVCollector
|
ProgramSVCollector(ProgramElement root,
ImmutableList<SchemaVariable> vars,
SVInstantiations svInst)
create the ProgramSVCollector
|
ProgramVariableCollector(ProgramElement root,
Services services)
collects all program variables occurring in the AST root using
this constructor is equivalent to
ProggramVariableCollector(root, false)
|
ProgVarReplaceVisitor(ProgramElement st,
java.util.Map<ProgramVariable,ProgramVariable> map,
boolean replaceall,
Services services)
creates a visitor that replaces the program variables in the given
statement
|
ProgVarReplaceVisitor(ProgramElement st,
java.util.Map<ProgramVariable,ProgramVariable> map,
Services services)
creates a visitor that replaces the program variables in the given
statement by new ones with the same name
|
UndeclaredProgramVariableCollector(ProgramElement root,
Services services)
Constructor.
|
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.
|
interface |
ProgramPrefix
this interface is implemented by program elements that may be matched
by the inactive program prefix
|
Modifier and Type | Class and Description |
---|---|
class |
ProgramElementName |
static class |
VariableNamer.IndProgramElementName
ProgramElementName carrying an additional index
|
Modifier and Type | Method and Description |
---|---|
ProgramElement |
PosInProgram.getProgram(ProgramElement pe) |
static ProgramElement |
PosInProgram.getProgramAt(PosInProgram pos,
ProgramElement prg)
returns the ProgramElement at the given position
|
protected ProgramElement |
VariableNamer.getProgramFromPIO(PosInOccurrence pio)
returns the program contained in a PosInOccurrence
|
Modifier and Type | Method and Description |
---|---|
static NameCreationInfo |
MethodStackInfo.create(ProgramElement program) |
protected int |
VariableNamer.getMaxCounterInProgram(java.lang.String basename,
ProgramElement program,
PosInProgram posOfDeclaration)
returns the maximum counter value already associated with the passed
basename in the passed program (ignoring temporary counters), or -1
|
ProgramElement |
PosInProgram.getProgram(ProgramElement pe) |
static ProgramElement |
PosInProgram.getProgramAt(PosInProgram pos,
ProgramElement prg)
returns the ProgramElement at the given position
|
protected boolean |
VariableNamer.isUniqueInProgram(java.lang.String name,
ProgramElement program,
PosInProgram posOfDeclaration)
tells whether a name is unique in the passed program
|
Constructor and Description |
---|
MethodStackInfo(ProgramElement element) |
Modifier and Type | Interface and Description |
---|---|
interface |
IProgramMethod |
interface |
IProgramVariable |
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 |
ProgramMethod
The program method represents a (pure) method in the logic.
|
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 |
---|---|
ProgramElement |
ProgramMethod.getChildAt(int i) |
ProgramElement |
ProgramSV.getChildAt(int index) |
Modifier and Type | Method and Description |
---|---|
ProgramElement |
ProgramSVSort.getSVWithSort(ExtList l,
java.lang.Class<?> alternative) |
Modifier and Type | Method and Description |
---|---|
boolean |
ProgramSVSort.canStandFor(ProgramElement check,
ExecutionContext ec,
Services services) |
boolean |
ProgramSVSort.SimpleExpressionStringSort.canStandFor(ProgramElement check,
ExecutionContext ec,
Services services) |
boolean |
ProgramSVSort.SimpleExpressionNonStringObjectSort.canStandFor(ProgramElement check,
ExecutionContext ec,
Services services) |
protected abstract boolean |
ProgramSVSort.canStandFor(ProgramElement check,
Services services) |
Constructor and Description |
---|
FinishSymbolicExecutionUntilMergePointMacro(java.util.HashSet<ProgramElement> blockElems) |
Modifier and Type | Method and Description |
---|---|
void |
LogicPrinter.printProgramElement(ProgramElement pe)
Pretty-prints a ProgramElement.
|
Modifier and Type | Method and Description |
---|---|
ProgramElement |
ProgVarReplacer.replace(ProgramElement pe)
replaces in a statement
|
Modifier and Type | Method and Description |
---|---|
ProgramElement |
ProgVarReplacer.replace(ProgramElement pe)
replaces in a statement
|
Modifier and Type | Method and Description |
---|---|
protected void |
ProgramVariableReferencesAnalyst.listReferences(Node node,
ProgramElement pe,
ProgramVariable arrayLength,
java.util.LinkedHashSet<IProofReference<?>> toFill,
boolean includeExpressionContainer)
Extracts the proof references recursive.
|
Modifier and Type | Method and Description |
---|---|
static java.lang.StringBuffer |
OutputStreamProofSaver.printProgramElement(ProgramElement pe) |
Modifier and Type | Interface and Description |
---|---|
interface |
AbstractProgramElement |
Modifier and Type | Method and Description |
---|---|
ProgramElement |
AbstractProgramElement.getConcreteProgramElement(Services services) |
ProgramElement |
TacletApp.getProgramElement(java.lang.String instantiation,
SchemaVariable sv,
Services services) |
Modifier and Type | Method and Description |
---|---|
TacletApp |
TacletApp.addCheckedInstantiation(SchemaVariable sv,
ProgramElement pe,
Services services,
boolean interesting)
checks if the instantiation of
sv with pe is
possible. |
TacletApp |
NoPosTacletApp.addInstantiation(SchemaVariable sv,
ProgramElement pe,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
TacletApp |
PosTacletApp.addInstantiation(SchemaVariable sv,
ProgramElement pe,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
abstract TacletApp |
TacletApp.addInstantiation(SchemaVariable sv,
ProgramElement pe,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp.
|
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(ProgramElement el,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses) |
Term |
AuxiliaryContractBuilders.UpdatesBuilder.buildAnonOutUpdate(ProgramElement el,
java.util.Map<LocationVariable,Function> anonymisationHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses,
java.lang.String prefix) |
AuxiliaryContract.Variables |
AuxiliaryContractBuilders.VariablesCreatorAndRegistrar.createAndRegister(Term self,
boolean existingPO,
ProgramElement pe) |
MatchConditions |
TacletMatcher.matchSV(SchemaVariable sv,
ProgramElement term,
MatchConditions matchCond,
Services services)
|
Modifier and Type | Method and Description |
---|---|
ProgramElement |
ContextInstantiationEntry.contextProgram()
returns the context program with an ignorable part between prefix
and suffix position
|
ProgramElement |
ContextStatementBlockInstantiation.programElement()
returns the program element this context term instantiation refers to
|
Modifier and Type | Method and Description |
---|---|
ImmutableArray<ProgramElement> |
ProgramList.getList() |
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
SVInstantiations.add(PosInProgram prefix,
PosInProgram postfix,
ExecutionContext activeStatementContext,
ProgramElement pe,
Services services)
adds the given pair to the instantiations for the context.If the context
has been instantiated already, the new pair is taken without a warning.
|
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
ProgramElement pe,
Services services)
adds the given pair to the instantiations.
|
SVInstantiations |
SVInstantiations.addInteresting(SchemaVariable sv,
ProgramElement pe,
Services services) |
SVInstantiations |
SVInstantiations.replace(PosInProgram prefix,
PosInProgram postfix,
ExecutionContext activeStatementContext,
ProgramElement pe,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
SVInstantiations.replace(SchemaVariable sv,
ProgramElement pe,
Services services)
replaces the given pair in the instantiations.
|
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
SVInstantiations.replace(SchemaVariable sv,
ImmutableArray<ProgramElement> pes,
Services services)
replaces the given pair in the instantiations.
|
Constructor and Description |
---|
ContextStatementBlockInstantiation(PosInProgram prefixEnd,
PosInProgram suffixStart,
ExecutionContext activeStatementContext,
ProgramElement pe)
creates a ContextStatementBlockInstantiation of a context term
|
Constructor and Description |
---|
ProgramList(ImmutableArray<ProgramElement> list) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
LegacyTacletMatcher.matchSV(SchemaVariable sv,
ProgramElement pe,
MatchConditions matchCond,
Services services)
|
Modifier and Type | Method and Description |
---|---|
MatchConditions |
VMTacletMatcher.matchSV(SchemaVariable sv,
ProgramElement pe,
MatchConditions matchCond,
Services services)
|
Modifier and Type | Method and Description |
---|---|
protected MatchConditions |
MatchProgramSVInstruction.addInstantiation(ProgramElement pe,
MatchConditions matchCond,
Services services)
tries to add the pair (this,pe) to the match conditions.
|
MatchConditions |
MatchProgramSVInstruction.match(ProgramElement instantiationCandidate,
MatchConditions matchCond,
Services services)
tries to match the schema variable of this instruction with the specified
ProgramElement instantiationCandidate
w.r.t. |
MatchConditions |
MatchSchemaVariableInstruction.match(ProgramElement instantiationCandidate,
MatchConditions mc,
Services services)
tries to match the schema variable of this instruction with the specified
ProgramElement instantiationCandidate
w.r.t. |
Constructor and Description |
---|
MatchProgramInstruction(ProgramElement pe) |
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 ProgramElement |
WhileLoopTransformation.replacement
the replacement element
|
protected ProgramElement |
WhileLoopTransformation.result
the result of the transformation
|
protected ProgramElement |
ReplaceWhileLoop.result
the result of the transformation
|
Modifier and Type | Method and Description |
---|---|
ProgramElement |
ProgramTransformer.body()
returns the body of the meta construct
|
ProgramElement |
ProgramTransformer.getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array.
|
ProgramElement |
WhileLoopTransformation.result() |
ProgramElement |
ReplaceWhileLoop.result() |
ProgramElement[] |
ReattachLoopInvariant.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
SpecialConstructorCall.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
UnwindLoop.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
ForToWhile.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
StaticInitialisation.transform(ProgramElement pe,
Services services,
SVInstantiations insts) |
ProgramElement[] |
InitArrayCreation.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
ArrayLength.transform(ProgramElement pe,
Services services,
SVInstantiations insts) |
ProgramElement[] |
IsStatic.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
MultipleVarDecl.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
EvaluateArgs.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
TypeOf.transform(ProgramElement pe,
Services services,
SVInstantiations insts) |
ProgramElement[] |
ArrayPostDecl.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
DoBreak.transform(ProgramElement pe,
Services services,
SVInstantiations insts)
performs the program transformation needed for symbolic program
transformation
|
ProgramElement[] |
ConstructorCall.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
MethodCall.transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
performs the program transformation needed for symbolic program execution
|
ProgramElement[] |
ForInitUnfoldTransformer.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
EnhancedForElimination.transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
An enhanced for loop is executed by transforming it into a "normal" for loop.
|
ProgramElement[] |
Unpack.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
PostWork.transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
performs the program transformation needed for symbolic program
transformation
|
abstract ProgramElement[] |
ProgramTransformer.transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
performs the program transformation needed for symbolic
program transformation
|
ProgramElement[] |
SwitchToIf.transform(ProgramElement pe,
Services services,
SVInstantiations insts) |
ProgramElement[] |
CreateObject.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
ExpandMethodBody.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
Modifier and Type | Method and Description |
---|---|
protected void |
WhileLoopTransformation.doAction(ProgramElement node)
the action that is performed just before leaving the node the
last time
|
ImmutableList<SchemaVariable> |
WhileInvariantTransformer.neededInstantiations(ProgramElement originalLoop,
SVInstantiations svInst)
returns the schemavariables that are needed to transform the given loop.
|
ProgramElement[] |
ReattachLoopInvariant.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
SpecialConstructorCall.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
UnwindLoop.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
ForToWhile.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
StaticInitialisation.transform(ProgramElement pe,
Services services,
SVInstantiations insts) |
ProgramElement[] |
InitArrayCreation.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
ArrayLength.transform(ProgramElement pe,
Services services,
SVInstantiations insts) |
ProgramElement[] |
IsStatic.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
MultipleVarDecl.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
EvaluateArgs.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
TypeOf.transform(ProgramElement pe,
Services services,
SVInstantiations insts) |
ProgramElement[] |
ArrayPostDecl.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
DoBreak.transform(ProgramElement pe,
Services services,
SVInstantiations insts)
performs the program transformation needed for symbolic program
transformation
|
ProgramElement[] |
ConstructorCall.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
MethodCall.transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
performs the program transformation needed for symbolic program execution
|
ProgramElement[] |
ForInitUnfoldTransformer.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
EnhancedForElimination.transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
An enhanced for loop is executed by transforming it into a "normal" for loop.
|
ProgramElement[] |
Unpack.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
PostWork.transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
performs the program transformation needed for symbolic program
transformation
|
abstract ProgramElement[] |
ProgramTransformer.transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
performs the program transformation needed for symbolic
program transformation
|
ProgramElement[] |
SwitchToIf.transform(ProgramElement pe,
Services services,
SVInstantiations insts) |
ProgramElement[] |
CreateObject.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
ProgramElement[] |
ExpandMethodBody.transform(ProgramElement pe,
Services services,
SVInstantiations svInst) |
protected void |
WhileLoopTransformation.walk(ProgramElement node)
walks through the AST.
|
protected void |
ReplaceWhileLoop.walk(ProgramElement node) |
Constructor and Description |
---|
ConstructorCall(Name name,
SchemaVariable newObjectSV,
ProgramElement consRef) |
ConstructorCall(SchemaVariable newObjectSV,
ProgramElement consRef)
creates the metaconstruct
|
CreateObject(ProgramElement newExpr) |
EvaluateArgs(ProgramElement pe)
creates a typeof ProgramTransformer
|
ForToWhileTransformation(ProgramElement root,
ProgramElementName outerLabel,
ProgramElementName innerLabel,
Services services) |
InitArray(java.lang.String name,
ProgramElement body) |
InitArrayCreation(SchemaVariable newObjectSV,
ProgramElement newExpr) |
IsStatic(ProgramElement pe)
creates a typeof ProgramTransformer
|
MethodCall(Name name,
ProgramSV ec,
SchemaVariable result,
ProgramElement body)
creates the methodcall-MetaConstruct
|
MethodCall(ProgramElement body)
creates the methodcall-MetaConstruct
|
MethodCall(ProgramSV ec,
SchemaVariable result,
ProgramElement body)
creates the methodcall-MetaConstruct
|
MethodCall(SchemaVariable result,
ProgramElement body)
creates the methodcall-MetaConstruct
|
ProgramTransformer(Name name,
ProgramElement body)
creates a ProgramTransformer
|
ProgramTransformer(java.lang.String name,
ProgramElement body)
creates a ProgramTransformer
|
ReplaceWhileLoop(ProgramElement root,
StatementBlock toInsert,
Services services)
creates the WhileLoopTransformation for the transformation mode
|
ReplaceWhileLoop(ProgramElement root,
SVInstantiations inst,
StatementBlock toInsert,
Services services)
creates the WhileLoopTransformation for the check mode
|
SpecialConstructorCall(ProgramElement consRef) |
TypeOf(ProgramElement pe)
creates a typeof ProgramTransformer
|
WhileInvariantTransformation(ProgramElement root,
ProgramElementName outerLabel,
ProgramElementName innerLabel,
ProgramVariable cont,
ProgramVariable exc,
ProgramVariable excParam,
ProgramVariable thrownException,
ProgramVariable brk,
ProgramVariable rtrn,
ProgramVariable returnExpr,
java.util.LinkedList<de.uka.ilkd.key.rule.metaconstruct.BreakToBeReplaced> breakList,
Services services)
creates the WhileLoopTransformation for the transformation mode
|
WhileInvariantTransformation(ProgramElement root,
SVInstantiations inst,
Services services)
creates the WhileLoopTransformation for the check mode
|
WhileLoopTransformation(ProgramElement root,
ProgramElementName outerLabel,
ProgramElementName innerLabel,
Services services)
creates the WhileLoopTransformation for the transformation mode
|
WhileLoopTransformation(ProgramElement root,
SVInstantiations inst,
Services services)
creates the WhileLoopTransformation for the check mode
|
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractBackwardSlicer.updateRelevantLocations(ProgramElement read,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info,
Services services)
Updates the relevant locations.
|
Modifier and Type | Method and Description |
---|---|
static boolean |
SymbolicExecutionUtil.containsStatement(ProgramElement toSearchIn,
SourceElement toSearch,
Services services)
Checks if the given
ProgramElement contains the given SourceElement . |
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<ProgramVariable> |
MiscTools.getLocalIns(ProgramElement pe,
Services services)
All variables read in the specified program element, excluding newly declared variables.
|
static ImmutableSet<ProgramVariable> |
MiscTools.getLocallyDeclaredVars(ProgramElement pe,
Services services)
All variables newly declared in the specified program element.
|
static ImmutableSet<ProgramVariable> |
MiscTools.getLocalOuts(ProgramElement pe,
Services services)
All variables changed in the specified program element, excluding newly declared variables.
|
static ImmutableSet<ProgramVariable> |
MiscTools.getLocalOutsAndDeclared(ProgramElement pe,
Services services)
All variables changed in the specified program element, including newly declared variables.
|
Copyright © 2003-2019 The KeY-Project.