Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.reference |
Elements of the Java syntax tree representing implicit or explicit (named)
references to other program elements.
|
de.uka.ilkd.key.java.statement |
Elements of the Java syntax tree representing pure statements.
|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.symbolic_execution.util |
Modifier and Type | Method and Description |
---|---|
IExecutionContext |
ContextStatementBlock.getExecutionContext() |
Modifier and Type | Method and Description |
---|---|
static MethodFrame |
KeYJavaASTFactory.methodFrame(IExecutionContext executionContext,
StatementBlock block)
Create a method call substitution.
|
static MethodFrame |
KeYJavaASTFactory.methodFrame(IExecutionContext executionContext,
StatementBlock block,
PositionInfo position)
Create a method call substitution at a specific source position.
|
static MethodFrame |
KeYJavaASTFactory.methodFrame(IProgramVariable result,
IExecutionContext executionContext,
StatementBlock block)
Create a method call substitution with a return value assignment.
|
static MethodFrame |
KeYJavaASTFactory.methodFrame(IProgramVariable result,
IExecutionContext executionContext,
StatementBlock block,
PositionInfo position)
Create a method call substitution with a return value assignment at a
specific source position.
|
Constructor and Description |
---|
ContextStatementBlock(ExtList children,
IExecutionContext executionContext)
creates a ContextStatementBlock
|
ContextStatementBlock(Statement[] body,
IExecutionContext executionContext) |
ContextStatementBlock(Statement s,
IExecutionContext executionContext) |
Modifier and Type | Class and Description |
---|---|
class |
ExecutionContext |
Modifier and Type | Method and Description |
---|---|
IExecutionContext |
MethodFrame.getExecutionContext()
returns the execution context for the elements in the method
frame's body
|
Constructor and Description |
---|
MethodFrame(IProgramVariable resultVar,
IExecutionContext execContext,
StatementBlock body)
Labeled statement.
|
MethodFrame(IProgramVariable resultVar,
IExecutionContext execContext,
StatementBlock body,
PositionInfo pos)
Labeled statement.
|
Modifier and Type | Interface and Description |
---|---|
interface |
ProgramConstruct
A type that implement this interface can be used in all java
programs instead of an expression or statement.
|
Modifier and Type | Class and Description |
---|---|
class |
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
Modifier and Type | Method and Description |
---|---|
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractReturnVariableValueSequent(Services services,
IExecutionContext context,
Node methodReturnNode,
Node methodCallEmptyNode,
IProgramVariable variable)
Creates a
Sequent which can be used in site proofs to
extract the return value of the given IProgramVariable from the
sequent of the given Node . |
Copyright © 2003-2019 The KeY-Project.