Package | Description |
---|---|
de.uka.ilkd.key.api |
This package gives an high-level entry point to the KeY world.
|
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.expression |
Elements of the Java syntax tree representing expressions.
|
de.uka.ilkd.key.java.expression.literal |
This package contains representations for the various Java literal types.
|
de.uka.ilkd.key.java.expression.operator |
Elements of the Java syntax tree representing operators and operator-like
expressions.
|
de.uka.ilkd.key.java.reference |
Elements of the Java syntax tree representing implicit or explicit (named)
references to other program elements.
|
de.uka.ilkd.key.java.statement |
Elements of the Java syntax tree representing pure statements.
|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.model | |
de.uka.ilkd.key.symbolic_execution.model.impl | |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
java.util.List<PositionInfo> |
ScriptResult.getLinenumbers() |
Modifier and Type | Method and Description |
---|---|
ScriptResult |
ScriptResult.setLinenumbers(java.util.List<PositionInfo> linenumbers) |
Modifier and Type | Field and Description |
---|---|
static PositionInfo |
PositionInfo.UNDEFINED
PositionInfo with undefined positions.
|
Modifier and Type | Method and Description |
---|---|
PositionInfo |
SourceElement.getPositionInfo()
complete position information
|
PositionInfo |
JavaSourceElement.getPositionInfo() |
static PositionInfo |
PositionInfo.join(PositionInfo p1,
PositionInfo p2)
Creates a new PositionInfo from joining the intervals of the given PositionInfos.
|
Modifier and Type | Method and Description |
---|---|
static CopyAssignment |
KeYJavaASTFactory.assign(Expression lhs,
Expression rhs,
PositionInfo posInfo)
creates an assignment
lhs:=rhs |
static Statement |
KeYJavaASTFactory.breakStatement(Label label,
PositionInfo positionInfo) |
static Case |
KeYJavaASTFactory.caseBlock(ExtList parameters,
Expression expression,
PositionInfo position)
Create a case block.
|
static Do |
KeYJavaASTFactory.doLoop(Expression condition,
Statement statement,
PositionInfo positionInfo)
Create a do loop.
|
static PositionInfo |
PositionInfo.join(PositionInfo p1,
PositionInfo p2)
Creates a new PositionInfo from joining the intervals of the given PositionInfos.
|
static LabeledStatement |
KeYJavaASTFactory.labeledStatement(ExtList parameters,
Label label,
PositionInfo position)
Create a labeled statement.
|
static Statement |
KeYJavaASTFactory.labeledStatement(Label label,
Statement[] statements,
PositionInfo pos)
Create a labeled block of statements.
|
static LabeledStatement |
KeYJavaASTFactory.labeledStatement(Label label,
Statement statement,
PositionInfo pos)
Create a labeled statement.
|
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,
PositionInfo position)
Create a method call substitution with a return value assignment at a
specific source position.
|
static While |
KeYJavaASTFactory.whileLoop(Expression condition,
Statement body,
PositionInfo position)
Create a while loop at a specific source position.
|
Constructor and Description |
---|
Comment(java.lang.String text,
PositionInfo pInfo) |
JavaNonTerminalProgramElement(ExtList children,
PositionInfo pos) |
JavaNonTerminalProgramElement(PositionInfo pos) |
JavaProgramElement(ExtList children,
PositionInfo pos) |
JavaProgramElement(PositionInfo pos)
creates a java program element with the given position information
|
JavaSourceElement(ExtList children,
PositionInfo pos) |
JavaSourceElement(PositionInfo pi)
Java source element.
|
Constructor and Description |
---|
VariableSpecification(IProgramVariable var,
int dim,
Expression init,
Type type,
PositionInfo pi) |
Constructor and Description |
---|
Literal(ExtList children,
PositionInfo pos)
Literal with specific source code position.
|
Literal(PositionInfo pos)
Literal with specific source code position.
|
Constructor and Description |
---|
BooleanLiteral(ExtList children,
PositionInfo pos,
boolean value)
Boolean literal.
|
BooleanLiteral(PositionInfo pos,
boolean value)
Boolean literal.
|
Constructor and Description |
---|
New(ExtList children,
ReferencePrefix rp,
PositionInfo pi)
Constructor for the transformation of COMPOST ASTs to KeY.
|
TypeOperator(ExtList children,
PositionInfo pi)
Constructor for the transformation of COMPOST ASTs to KeY.
|
Constructor and Description |
---|
ArrayReference(ExtList children,
ReferencePrefix accessPath,
PositionInfo pi)
Constructor for the transformation of COMPOST ASTs to KeY.
|
FieldReference(ProgramVariable pv,
ReferencePrefix prefix,
PositionInfo pi) |
MethodReference(ExtList args,
MethodName n,
ReferencePrefix p,
PositionInfo pos) |
MethodReference(ExtList children,
MethodName n,
ReferencePrefix p,
PositionInfo pos,
java.lang.String scope) |
MethodReference(ImmutableArray<Expression> args,
MethodName n,
ReferencePrefix p,
PositionInfo pos) |
SpecialConstructorReference(ExtList children,
PositionInfo pi)
Constructor for the transformation of COMPOST ASTs to KeY.
|
SuperConstructorReference(ExtList children,
ReferencePrefix accessPath,
PositionInfo pi)
Constructor for the transformation of COMPOST ASTs to KeY.
|
VariableReference(ProgramVariable variable,
PositionInfo pi) |
Modifier and Type | Method and Description |
---|---|
PositionInfo |
ProgramElementName.getPositionInfo() |
Modifier and Type | Method and Description |
---|---|
PositionInfo |
ProgramVariable.getPositionInfo() |
PositionInfo |
ProgramMethod.getPositionInfo() |
PositionInfo |
ProgramSV.getPositionInfo() |
Constructor and Description |
---|
ProgramMethod(MethodDeclaration method,
KeYJavaType container,
KeYJavaType kjt,
PositionInfo pi,
Sort heapSort) |
ProgramMethod(MethodDeclaration method,
KeYJavaType container,
KeYJavaType kjt,
PositionInfo pi,
Sort heapSort,
int heapCount) |
Modifier and Type | Method and Description |
---|---|
PositionInfo |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getActivePositionInfo()
Returns the
PositionInfo of IExecutionNode.getActiveStatement() . |
PositionInfo |
ExecutionNodeReader.KeYlessLoopCondition.getGuardExpressionPositionInfo()
Returns the code position of the executed loop expression (
IExecutionLoopCondition.getGuardExpression() ). |
Modifier and Type | Method and Description |
---|---|
PositionInfo |
IExecutionNode.getActivePositionInfo()
Returns the
PositionInfo of IExecutionNode.getActiveStatement() . |
PositionInfo |
IExecutionLoopCondition.getGuardExpressionPositionInfo()
Returns the code position of the executed loop expression (
IExecutionLoopCondition.getGuardExpression() ). |
Modifier and Type | Method and Description |
---|---|
PositionInfo |
AbstractExecutionNode.getActivePositionInfo()
Returns the
PositionInfo of IExecutionNode.getActiveStatement() . |
PositionInfo |
ExecutionLoopCondition.getGuardExpressionPositionInfo()
Returns the code position of the executed loop expression (
IExecutionLoopCondition.getGuardExpression() ). |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
SymbolicExecutionUtil.getSourcePath(PositionInfo posInfo)
Returns the path to the source file defined by the given
PositionInfo . |
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.isLoopStatement(Node node,
RuleApp ruleApp,
SourceElement statement,
PositionInfo posInfo)
Checks if the given node should be represented as loop statement.
|
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 java.lang.String |
MiscTools.getSourcePath(PositionInfo posInfo)
Returns the path to the source file defined by the given
PositionInfo . |
Copyright © 2003-2019 The KeY-Project.