Package | Description |
---|---|
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
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.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.jml | |
de.uka.ilkd.key.speclang.jml.pretranslation | |
de.uka.ilkd.key.speclang.njml |
This package provides the functionalities of parsing JML comments into KeY constructs.
|
de.uka.ilkd.key.speclang.translation | |
de.uka.ilkd.key.symbolic_execution.po |
Modifier and Type | Method and Description |
---|---|
static int |
IssueDialog.getOffsetFromLineColumn(java.lang.String source,
Position pos) |
Modifier and Type | Field and Description |
---|---|
static Position |
Position.UNDEFINED
The "undefined position" constant used to compare to undefined
positions or remove positional information.
|
Modifier and Type | Field and Description |
---|---|
protected java.util.HashMap<SourceElement,Position> |
PrettyPrinter.indentMap |
Modifier and Type | Method and Description |
---|---|
Position |
PositionInfo.getEndPosition() |
Position |
SourceElement.getEndPosition()
Returns the end position of the primary token of this element.
|
Position |
Label.getEndPosition() |
Position |
JavaSourceElement.getEndPosition()
Returns the end position of the primary token of this element.
|
Position |
PositionInfo.getRelativePosition() |
Position |
SourceElement.getRelativePosition()
Returns the relative position (number of blank heading lines and
columns) of the primary token of this element.
|
Position |
Label.getRelativePosition() |
Position |
JavaSourceElement.getRelativePosition()
Returns the relative position (number of blank heading lines and
columns) of the primary token of this element.
|
protected Position |
PrettyPrinter.getRelativePosition(SourceElement first) |
Position |
PositionInfo.getStartPosition() |
Position |
SourceElement.getStartPosition()
Returns the start position of the primary token of this element.
|
Position |
Label.getStartPosition() |
Position |
JavaSourceElement.getStartPosition()
Returns the start position of the primary token of this element.
|
Modifier and Type | Method and Description |
---|---|
int |
Position.compareTo(Position p)
Compares this position with the given object for order.
|
protected void |
PrettyPrinter.writeIndentation(Position relative)
Convenience method to write indentation chars.
|
Constructor and Description |
---|
PositionInfo(Position relPos,
Position startPos,
Position endPos)
Creates a new PositionInfo without resource information but only with positions.
|
PositionInfo(Position relPos,
Position startPos,
Position endPos,
java.net.URI fileURI)
Creates a new PositionInfo without the given resource information.
|
Modifier and Type | Method and Description |
---|---|
Position |
ProgramElementName.getEndPosition()
Returns the end position of the primary token of this element.
|
Position |
ProgramElementName.getRelativePosition()
Returns the relative position (number of blank heading lines and
columns) of the primary token of this element.
|
Position |
ProgramElementName.getStartPosition()
Returns the start position of the primary token of this element.
|
Modifier and Type | Method and Description |
---|---|
Position |
ProgramVariable.getEndPosition() |
Position |
ProgramMethod.getEndPosition()
Returns the end position of the primary token of this element.
|
Position |
ProgramSV.getEndPosition() |
Position |
ProgramVariable.getRelativePosition() |
Position |
ProgramMethod.getRelativePosition()
Returns the relative position (number of blank heading lines and columns)
of the primary token of this element.
|
Position |
ProgramSV.getRelativePosition() |
Position |
ProgramVariable.getStartPosition() |
Position |
ProgramMethod.getStartPosition()
Returns the start position of the primary token of this element.
|
Position |
ProgramSV.getStartPosition() |
Modifier and Type | Method and Description |
---|---|
Position |
NodeInfo.getExecStatementPosition()
returns the position of the executed statement in its source code
or Position.UNDEFINED
|
Modifier and Type | Field and Description |
---|---|
Position |
PositionedString.pos |
Constructor and Description |
---|
PositionedLabeledString(java.lang.String text,
java.lang.String fileName,
Position pos,
ImmutableArray<TermLabel> labels) |
PositionedLabeledString(java.lang.String text,
java.lang.String fileName,
Position pos,
TermLabel label) |
PositionedString(java.lang.String text,
java.lang.String fileName,
Position pos) |
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<LabeledParserRuleContext> |
JMLSpecExtractor.createNonNullPositionedString(java.lang.String varName,
KeYJavaType kjt,
boolean isImplicitVar,
java.lang.String fileName,
Position pos,
Services services)
creates a JML specification expressing that the given variable/field is
not null and in case of a reference array type that also its elements are
non-null In case of implicit fields or primitive typed fields/variables
the empty set is returned
|
Modifier and Type | Method and Description |
---|---|
Position |
TextualJMLConstruct.getApproxPosition()
Return the approximate position of this construct.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<TextualJMLConstruct> |
JmlIO.parseClassLevel(java.lang.String concatenatedComment,
java.lang.String fileName,
Position pos)
Parse and interpret class level comments.
|
ImmutableList<TextualJMLConstruct> |
JmlIO.parseMethodLevel(java.lang.String concatenatedComment,
java.lang.String fileName,
Position position)
Parse and interpret the given string as a method level construct.
|
Modifier and Type | Method and Description |
---|---|
Position |
SLTranslationException.getPosition() |
Modifier and Type | Method and Description |
---|---|
PositionedString |
SLExceptionFactory.createPositionedString(java.lang.String text,
Position pos)
Creates a string with position information from the given relative
position.
|
Constructor and Description |
---|
SLExceptionFactory(org.antlr.runtime.Parser parser,
java.lang.String fileName,
Position offsetPos) |
SLTranslationException(java.lang.String message,
java.lang.String fileName,
Position pos) |
SLTranslationException(java.lang.String message,
java.lang.String fileName,
Position pos,
java.lang.Throwable cause) |
SLTranslationException(java.lang.String message,
java.lang.Throwable cause,
java.lang.String fileName,
Position pos) |
SLWarningException(java.lang.String text,
java.lang.String fileName,
Position pos) |
Modifier and Type | Method and Description |
---|---|
Position |
ProgramMethodSubsetPO.getEndPosition()
Returns the end position.
|
protected static Position |
ProgramMethodSubsetPO.getEndPosition(java.util.Properties properties)
Extracts the end position from the given
Properties . |
Position |
ProgramMethodSubsetPO.getStartPosition()
Returns the start position.
|
protected static Position |
ProgramMethodSubsetPO.getStartPosition(java.util.Properties properties)
Extracts the start position from the given
Properties . |
Constructor and Description |
---|
ProgramMethodSubsetPO(InitConfig initConfig,
java.lang.String name,
IProgramMethod pm,
java.lang.String precondition,
Position startPosition,
Position endPosition)
Constructor.
|
ProgramMethodSubsetPO(InitConfig initConfig,
java.lang.String name,
IProgramMethod pm,
java.lang.String precondition,
Position startPosition,
Position endPosition,
boolean addUninterpretedPredicate,
boolean addSymbolicExecutionLabel)
Constructor.
|
Copyright © 2003-2019 The KeY-Project.