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.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.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.model | |
de.uka.ilkd.key.symbolic_execution.model.impl | |
de.uka.ilkd.key.symbolic_execution.slicing | |
de.uka.ilkd.key.symbolic_execution.strategy | |
de.uka.ilkd.key.symbolic_execution.strategy.breakpoint | |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.util.mergerule |
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 |
ProgramElement
A part of the program syntax that carries semantics in the model.
|
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 |
Comment |
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 |
JavaSourceElement
Top level implementation of a Java
SourceElement . |
class |
PackageSpecification
Package specification.
|
class |
SingleLineComment
Any non-SingleLineComment is a multi line comment.
|
class |
StatementBlock
Statement block.
|
Modifier and Type | Field and Description |
---|---|
protected java.util.HashMap<SourceElement,Position> |
PrettyPrinter.indentMap |
Modifier and Type | Method and Description |
---|---|
static SourceElement |
JavaTools.getActiveStatement(JavaBlock jb)
Returns the active statement of the passed a java block.
|
SourceElement |
SourceElement.getFirstElement()
Finds the source element that occurs first in the source.
|
SourceElement |
Label.getFirstElement() |
SourceElement |
StatementBlock.getFirstElement() |
SourceElement |
CompilationUnit.getFirstElement() |
SourceElement |
JavaSourceElement.getFirstElement()
Finds the source element that occurs first in the source.
|
SourceElement |
SourceElement.getFirstElementIncludingBlocks()
Finds the source element that occurs first in the source.
|
SourceElement |
StatementBlock.getFirstElementIncludingBlocks() |
SourceElement |
CompilationUnit.getFirstElementIncludingBlocks() |
SourceElement |
JavaSourceElement.getFirstElementIncludingBlocks() |
SourceElement |
SourceElement.getLastElement()
Finds the source element that occurs last in the source.
|
SourceElement |
PackageSpecification.getLastElement() |
SourceElement |
Label.getLastElement() |
SourceElement |
Import.getLastElement() |
SourceElement |
CompilationUnit.getLastElement() |
SourceElement |
JavaSourceElement.getLastElement()
Finds the source element that occurs last in the source.
|
Modifier and Type | Method and Description |
---|---|
void |
NameAbstractionTable.add(SourceElement pe1,
SourceElement pe2)
adds the given two elements to the table
|
boolean |
JavaNonTerminalProgramElement.equalsModRenaming(SourceElement se,
NameAbstractionTable nat)
commented in interface SourceElement.
|
boolean |
SourceElement.equalsModRenaming(SourceElement se,
NameAbstractionTable nat)
This method returns true if two program parts are equal modulo
renaming.
|
boolean |
JavaProgramElement.equalsModRenaming(SourceElement se,
NameAbstractionTable nat)
commented in interface SourceElement.
|
boolean |
StatementBlock.equalsModRenaming(SourceElement se,
NameAbstractionTable nat) |
boolean |
Comment.equalsModRenaming(SourceElement se,
NameAbstractionTable nat)
comments can be ignored
|
protected Position |
PrettyPrinter.getRelativePosition(SourceElement first) |
boolean |
NameAbstractionTable.sameAbstractName(SourceElement pe0,
SourceElement pe1)
tests if the given elements have been assigned to the same
abstract name.
|
protected void |
PrettyPrinter.writeElement(int lf,
int levelChange,
int blanks,
SourceElement elem)
Adds indentation for a program element if necessary and if required,
but does not print the indentation itself.
|
protected void |
PrettyPrinter.writeElement(int lf,
int blanks,
SourceElement elem)
Write a source element.
|
protected void |
PrettyPrinter.writeElement(int blanks,
SourceElement elem)
Write source element.
|
protected void |
PrettyPrinter.writeElement(SourceElement elem)
Write source element.
|
protected void |
PrettyPrinter.writeIndentation(SourceElement elem)
Write indentation.
|
protected void |
PrettyPrinter.writeInternalIndentation(SourceElement elem)
Write internal indentation.
|
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 |
---|---|
SourceElement |
VariableDeclaration.getFirstElement() |
SourceElement |
TypeDeclaration.getFirstElement() |
SourceElement |
VariableSpecification.getFirstElement() |
SourceElement |
MethodDeclaration.getFirstElement() |
SourceElement |
VariableDeclaration.getFirstElementIncludingBlocks() |
SourceElement |
VariableDeclaration.getLastElement() |
SourceElement |
TypeDeclaration.getLastElement() |
SourceElement |
Throws.getLastElement() |
SourceElement |
VariableSpecification.getLastElement() |
SourceElement |
ClassInitializer.getLastElement() |
SourceElement |
InheritanceSpecification.getLastElement() |
SourceElement |
MethodDeclaration.getLastElement() |
Modifier and Type | Method and Description |
---|---|
boolean |
VariableSpecification.equalsModRenaming(SourceElement se,
NameAbstractionTable nat)
equals modulo renaming is described in the corresponding
comment in class SourceElement.
|
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 | 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 |
---|---|
SourceElement |
Operator.getFirstElement() |
SourceElement |
ParenthesizedExpression.getFirstElement() |
SourceElement |
Operator.getFirstElementIncludingBlocks() |
SourceElement |
Operator.getLastElement() |
SourceElement |
ParenthesizedExpression.getLastElement() |
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 | Method and Description |
---|---|
boolean |
EmptySeqLiteral.equalsModRenaming(SourceElement o,
NameAbstractionTable nat) |
boolean |
StringLiteral.equalsModRenaming(SourceElement o,
NameAbstractionTable nat) |
boolean |
DoubleLiteral.equalsModRenaming(SourceElement o,
NameAbstractionTable nat)
tests if equals
|
boolean |
EmptySetLiteral.equalsModRenaming(SourceElement o,
NameAbstractionTable nat) |
boolean |
RealLiteral.equalsModRenaming(SourceElement o,
NameAbstractionTable nat)
tests if equals
|
boolean |
FloatLiteral.equalsModRenaming(SourceElement o,
NameAbstractionTable nat)
tests if equals
|
boolean |
BooleanLiteral.equalsModRenaming(SourceElement o,
NameAbstractionTable nat)
tests if equals
|
boolean |
AbstractIntegerLiteral.equalsModRenaming(SourceElement o,
NameAbstractionTable nat) |
boolean |
EmptyMapLiteral.equalsModRenaming(SourceElement o,
NameAbstractionTable nat) |
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 |
---|---|
SourceElement |
New.getFirstElement() |
SourceElement |
New.getFirstElementIncludingBlocks() |
SourceElement |
ExactInstanceof.getLastElement() |
SourceElement |
Instanceof.getLastElement() |
SourceElement |
New.getLastElement() |
SourceElement |
NewArray.getLastElement() |
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 | 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 |
---|---|
boolean |
LabeledStatement.equalsModRenaming(SourceElement se,
NameAbstractionTable nat)
testing if programelements are equal modulo renaming abstract
from names.
|
boolean |
TransactionStatement.equalsModRenaming(SourceElement source,
NameAbstractionTable nat) |
Modifier and Type | Method and Description |
---|---|
protected void |
CreatingASTVisitor.addChild(SourceElement x) |
protected void |
CreatingASTVisitor.addToTopOfStack(SourceElement x) |
protected void |
LabelCollector.doDefaultAction(SourceElement node) |
protected void |
OuterBreakContinueAndReturnReplacer.doDefaultAction(SourceElement x) |
protected void |
InnerBreakAndContinueReplacer.doDefaultAction(SourceElement x) |
protected void |
CreatingASTVisitor.doDefaultAction(SourceElement x)
called if the program element x is unchanged
|
protected abstract void |
JavaASTVisitor.doDefaultAction(SourceElement node)
the action that is performed just before leaving the node the
last time
|
protected void |
OuterBreakContinueAndReturnCollector.doDefaultAction(SourceElement x) |
protected void |
ProgramVariableCollector.doDefaultAction(SourceElement x) |
protected void |
ContainsStatementVisitor.doDefaultAction(SourceElement se)
the action that is performed just before leaving the node the
last time
|
protected void |
DeclarationProgramVariableCollector.doDefaultAction(SourceElement x) |
protected void |
ProgramReplaceVisitor.doDefaultAction(SourceElement x)
the implemented default action is called if a program element is, and if
it has children all its children too are left unchanged
|
static boolean |
ContainsStatementVisitor.equalsWithPosition(SourceElement first,
SourceElement second)
Compares the given
SourceElement s including their
PositionInfo s. |
Constructor and Description |
---|
ContainsStatementVisitor(ProgramElement root,
SourceElement toSearch,
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 |
---|---|
SourceElement |
ProgramElementName.getFirstElement()
to be compatible to a ProgramElement
|
SourceElement |
ProgramElementName.getFirstElementIncludingBlocks() |
SourceElement |
ProgramElementName.getLastElement()
to be compatible to a ProgramElement
|
SourceElement |
MultiRenamingTable.getRenaming(SourceElement se) |
SourceElement |
SingleRenamingTable.getRenaming(SourceElement se) |
abstract SourceElement |
RenamingTable.getRenaming(SourceElement se) |
Modifier and Type | Method and Description |
---|---|
java.util.HashMap<? extends SourceElement,? extends SourceElement> |
MultiRenamingTable.getHashMap() |
java.util.HashMap<? extends SourceElement,? extends SourceElement> |
MultiRenamingTable.getHashMap() |
java.util.HashMap<SourceElement,SourceElement> |
SingleRenamingTable.getHashMap() |
java.util.HashMap<SourceElement,SourceElement> |
SingleRenamingTable.getHashMap() |
abstract java.util.HashMap<? extends SourceElement,? extends SourceElement> |
RenamingTable.getHashMap() |
abstract java.util.HashMap<? extends SourceElement,? extends SourceElement> |
RenamingTable.getHashMap() |
java.util.Iterator<? extends SourceElement> |
MultiRenamingTable.getRenamingIterator() |
java.util.Iterator<SourceElement> |
SingleRenamingTable.getRenamingIterator() |
abstract java.util.Iterator<? extends SourceElement> |
RenamingTable.getRenamingIterator() |
Modifier and Type | Method and Description |
---|---|
boolean |
ProgramElementName.equalsModRenaming(SourceElement se,
NameAbstractionTable nat)
equals modulo renaming is described in the corresponding
comment in class SourceElement.
|
SourceElement |
MultiRenamingTable.getRenaming(SourceElement se) |
SourceElement |
SingleRenamingTable.getRenaming(SourceElement se) |
abstract SourceElement |
RenamingTable.getRenaming(SourceElement se) |
Modifier and Type | Method and Description |
---|---|
static RenamingTable |
RenamingTable.getRenamingTable(java.util.HashMap<? extends SourceElement,? extends SourceElement> hmap) |
static RenamingTable |
RenamingTable.getRenamingTable(java.util.HashMap<? extends SourceElement,? extends SourceElement> hmap) |
Constructor and Description |
---|
SingleRenamingTable(SourceElement oldVar,
SourceElement newVar) |
Constructor and Description |
---|
MultiRenamingTable(java.util.HashMap<? extends SourceElement,? extends SourceElement> hmap) |
MultiRenamingTable(java.util.HashMap<? extends SourceElement,? extends SourceElement> hmap) |
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 |
---|---|
SourceElement |
ProgramVariable.getFirstElement() |
SourceElement |
ProgramMethod.getFirstElement() |
SourceElement |
ProgramSV.getFirstElement() |
SourceElement |
ProgramVariable.getFirstElementIncludingBlocks() |
SourceElement |
ProgramMethod.getFirstElementIncludingBlocks() |
SourceElement |
ProgramSV.getFirstElementIncludingBlocks() |
SourceElement |
ProgramVariable.getLastElement() |
SourceElement |
ProgramMethod.getLastElement() |
SourceElement |
ProgramSV.getLastElement() |
Modifier and Type | Method and Description |
---|---|
boolean |
ProgramVariable.equalsModRenaming(SourceElement se,
NameAbstractionTable nat)
equals modulo renaming is described in the corresponding
comment in class SourceElement.
|
boolean |
ProgramMethod.equalsModRenaming(SourceElement se,
NameAbstractionTable nat)
equals modulo renaming is described in class SourceElement.
|
boolean |
ProgramSV.equalsModRenaming(SourceElement se,
NameAbstractionTable nat)
this method tests on object identity
|
Modifier and Type | Method and Description |
---|---|
static SourceElement |
NodeInfo.computeActiveStatement(RuleApp ruleApp)
Computes the active statement in the given
RuleApp . |
static SourceElement |
NodeInfo.computeActiveStatement(SourceElement firstStatement)
Computes the active statement in the given
SourceElement . |
static SourceElement |
NodeInfo.computeFirstStatement(RuleApp ruleApp)
Computes the first statement in the given
RuleApp . |
SourceElement |
NodeInfo.getActiveStatement()
returns the active statement of the JavaBlock the applied
rule has been matched against or null if no rule has been applied yet
or the applied rule was no taclet or program transformation rule
|
Modifier and Type | Method and Description |
---|---|
static SourceElement |
NodeInfo.computeActiveStatement(SourceElement firstStatement)
Computes the active statement in the given
SourceElement . |
Modifier and Type | Interface and Description |
---|---|
interface |
AbstractProgramElement |
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 |
---|---|
SourceElement |
ProgramTransformer.getLastElement()
Finds the source element that occurs last in the source.
|
Modifier and Type | Method and Description |
---|---|
protected void |
WhileLoopTransformation.addChild(SourceElement x) |
protected void |
WhileLoopTransformation.doDefaultAction(SourceElement x)
the implemented default action is called if a program element is,
and if it has children all its children too are left unchanged
|
Modifier and Type | Class and Description |
---|---|
static class |
ExecutionNodeReader.AbstractKeYlessBaseExecutionNode<S extends SourceElement>
An implementation of
IExecutionBaseMethodReturn which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode<S extends SourceElement>
An abstract implementation of
IExecutionBlockStartNode which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.AbstractKeYlessExecutionNode<S extends SourceElement>
An abstract implementation of
IExecutionNode which is independent
from KeY and provides such only children and default attributes. |
Modifier and Type | Method and Description |
---|---|
protected void |
SymbolicExecutionTreeBuilder.addToBlockMap(Node node,
AbstractExecutionBlockStartNode<?> blockStartNode,
int stackSize,
SourceElement... sourceElements)
Adds the given
AbstractExecutionNode add reason for a new block to the block maps. |
protected AbstractExecutionNode<?> |
SymbolicExecutionTreeBuilder.createExecutionTreeModelRepresentation(AbstractExecutionNode<?> parent,
Node node,
SourceElement statement)
Creates a new execution tree model representation (
IExecutionNode )
if possible for the given Node in KeY's proof tree. |
protected AbstractExecutionMethodReturn<?> |
SymbolicExecutionTreeBuilder.createMehtodReturn(AbstractExecutionNode<?> parent,
Node node,
SourceElement statement,
SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions)
Creates an method return node.
|
protected boolean |
SymbolicExecutionTreeBuilder.isAfterBlockReached(int currentStackSize,
MethodFrame currentInnerMostMethodFrame,
SourceElement currentActiveStatement,
int expectedStackSize,
java.util.Iterator<SourceElement> expectedStatementsIterator)
Checks if the after block condition is fulfilled.
|
protected boolean |
SymbolicExecutionTreeBuilder.isAfterBlockReached(int currentStackSize,
MethodFrame currentInnerMostMethodFrame,
SourceElement currentActiveStatement,
SymbolicExecutionTreeBuilder.JavaPair expectedPair)
Checks if the after block condition is fulfilled.
|
protected void |
SymbolicExecutionTreeBuilder.updateCallStack(Node node,
SourceElement statement)
Updates the call stack (
#methodCallStack ) if the given Node
in KeY's proof tree is a method call. |
Modifier and Type | Method and Description |
---|---|
protected boolean |
SymbolicExecutionTreeBuilder.isAfterBlockReached(int currentStackSize,
MethodFrame currentInnerMostMethodFrame,
SourceElement currentActiveStatement,
int expectedStackSize,
java.util.Iterator<SourceElement> expectedStatementsIterator)
Checks if the after block condition is fulfilled.
|
Constructor and Description |
---|
JavaPair(java.lang.Integer stackSize,
ImmutableList<SourceElement> elementsOfInterest)
Constructor.
|
Modifier and Type | Interface and Description |
---|---|
interface |
IExecutionBaseMethodReturn<S extends SourceElement>
Defines the common interface of
IExecutionMethodReturn
and IExecutionExceptionalMethodReturn . |
interface |
IExecutionBlockStartNode<S extends SourceElement>
An extended
IExecutionNode which groups several child nodes. |
interface |
IExecutionNode<S extends SourceElement>
Provides the basic methods each node in a symbolic execution tree
should have and allows to access the children.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractExecutionBlockStartNode<S extends SourceElement>
Provides a basic implementation of
IExecutionBlockStartNode . |
class |
AbstractExecutionMethodReturn<S extends SourceElement>
The default implementation of
IExecutionBaseMethodReturn . |
class |
AbstractExecutionNode<S extends SourceElement>
Provides a basic implementation of
IExecutionNode . |
Modifier and Type | Method and Description |
---|---|
SourceElement |
ExecutionStart.getActiveStatement()
Returns the active statement which is executed in the code.
|
SourceElement |
ExecutionBranchCondition.getActiveStatement()
Returns the active statement which is executed in the code.
|
Modifier and Type | Method and Description |
---|---|
protected boolean |
ThinBackwardSlicer.accept(Node node,
Node previousChild,
Services services,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info,
SourceElement activeStatement)
Decides if the given
Node is part of the slice or not. |
protected abstract boolean |
AbstractBackwardSlicer.accept(Node node,
Node previousChild,
Services services,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info,
SourceElement activeStatement)
Decides if the given
Node is part of the slice or not. |
protected ReferencePrefix |
AbstractSlicer.toReferencePrefix(SourceElement sourceElement)
Computes the
ReferencePrefix of the given SourceElement . |
Modifier and Type | Method and Description |
---|---|
protected boolean |
SymbolicExecutionBreakpointStopCondition.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Checks if a breakpoint is hit.
|
protected boolean |
BreakpointStopCondition.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Checks if a breakpoint is hit.
|
Modifier and Type | Method and Description |
---|---|
boolean |
AbstractHitCountBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
AbstractConditionalBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
SymbolicExecutionExceptionBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
ExceptionBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
FieldWatchpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
IBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
KeYWatchpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node) |
boolean |
MethodBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node) |
boolean |
LineBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node) |
Modifier and Type | Method and Description |
---|---|
static Pair<java.lang.Integer,SourceElement> |
SymbolicExecutionUtil.computeSecondStatement(RuleApp ruleApp)
Computes the call stack size and the second statement
similar to
NodeInfo.computeActiveStatement(SourceElement) . |
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 . |
static boolean |
SymbolicExecutionUtil.equalsWithPosition(SourceElement first,
SourceElement second)
Compares the given
SourceElement s including their PositionInfo s. |
static boolean |
SymbolicExecutionUtil.hasLoopCondition(Node node,
RuleApp ruleApp,
SourceElement statement)
Checks if the given
Node has a loop condition. |
static boolean |
SymbolicExecutionUtil.isBranchStatement(Node node,
RuleApp ruleApp,
SourceElement statement,
PositionInfo posInfo)
Checks if the given node should be represented as branch statement.
|
static boolean |
SymbolicExecutionUtil.isDoWhileLoopCondition(Node node,
SourceElement statement)
Checks if the given
SourceElement is a do while loop. |
static boolean |
SymbolicExecutionUtil.isForLoopCondition(Node node,
SourceElement statement)
Checks if the given
SourceElement is a for loop. |
static boolean |
SymbolicExecutionUtil.isLoopStatement(Node node,
RuleApp ruleApp,
SourceElement statement,
PositionInfo posInfo)
Checks if the given node should be represented as loop statement.
|
static boolean |
SymbolicExecutionUtil.isMethodCallNode(Node node,
RuleApp ruleApp,
SourceElement statement)
Checks if the given node should be represented as method call.
|
static boolean |
SymbolicExecutionUtil.isMethodCallNode(Node node,
RuleApp ruleApp,
SourceElement statement,
boolean allowImpliciteMethods)
Checks if the given node should be represented as method call.
|
static boolean |
SymbolicExecutionUtil.isStatementNode(Node node,
RuleApp ruleApp,
SourceElement statement,
PositionInfo posInfo)
Checks if the given node should be represented as statement.
|
Modifier and Type | Method and Description |
---|---|
static boolean |
MergeRuleUtils.equalsModBranchUniqueRenaming(SourceElement se1,
SourceElement se2,
Node node,
Services services)
An equals method that, before the comparison, replaces all program
locations in the supplied arguments by their branch-unique versions.
|
Copyright © 2003-2019 The KeY-Project.