Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
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.rule.inst |
contains classes for the instantiation of schema variables of
Taclet s. |
Modifier and Type | Method and Description |
---|---|
PosInProgram |
StatementBlock.getFirstActiveChildPos() |
Modifier and Type | Method and Description |
---|---|
PosInProgram |
Exec.getFirstActiveChildPos() |
PosInProgram |
LoopScopeBlock.getFirstActiveChildPos() |
PosInProgram |
MethodFrame.getFirstActiveChildPos() |
PosInProgram |
Try.getFirstActiveChildPos() |
PosInProgram |
SynchronizedBlock.getFirstActiveChildPos() |
PosInProgram |
LabeledStatement.getFirstActiveChildPos() |
Modifier and Type | Method and Description |
---|---|
protected JavaNonTerminalProgramElement |
ProgramContextAdder.wrap(JavaNonTerminalProgramElement context,
StatementBlock putIn,
IntIterator prefixPos,
int prefixDepth,
PosInProgram prefix,
PosInProgram suffix) |
Modifier and Type | Field and Description |
---|---|
static PosInProgram |
PosInProgram.ONE |
static PosInProgram |
PosInProgram.ONE_ONE |
static PosInProgram |
PosInProgram.ONE_ZERO |
static PosInProgram |
PosInProgram.TOP
pos at the beginning of the program
|
static PosInProgram |
PosInProgram.ZERO
often used positions
|
static PosInProgram |
PosInProgram.ZERO_ONE |
static PosInProgram |
PosInProgram.ZERO_ZERO |
Modifier and Type | Method and Description |
---|---|
PosInProgram |
PosInProgram.append(PosInProgram pp) |
PosInProgram |
PosInProgram.down(int n)
descending downwards choosing the n'th statement of the program
|
PosInProgram |
ProgramPrefix.getFirstActiveChildPos()
returns the position of the first active child
|
PosInProgram |
PosInProgram.prepend(PosInProgram pp) |
PosInProgram |
PosInProgram.up()
ascends one AST level
|
Modifier and Type | Method and Description |
---|---|
PosInProgram |
PosInProgram.append(PosInProgram pp) |
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
|
protected ProgramElementName |
VariableNamer.getNameProposalForSchemaVariable(java.lang.String basename,
SchemaVariable sv,
PosInOccurrence posOfFind,
PosInProgram posOfDeclaration,
ImmutableList<java.lang.String> previousProposals)
proposes a unique name for the instantiation of a schema variable
(like getProposal(), but somewhat less nicely)
|
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
|
boolean |
VariableNamer.isUniqueNameForSchemaVariable(java.lang.String name,
SchemaVariable sv,
PosInOccurrence posOfFind,
PosInProgram posOfDeclaration)
tells whether a name for instantiating a schema variable is unique
within its scope
|
boolean |
PosInProgram.leq(PosInProgram pip) |
PosInProgram |
PosInProgram.prepend(PosInProgram pp) |
Modifier and Type | Method and Description |
---|---|
PosInProgram |
ContextStatementBlockInstantiation.prefix()
returns the end position of the prefix
|
PosInProgram |
ContextInstantiationEntry.prefix()
returns the position of the first statement after the prefix
|
PosInProgram |
ContextStatementBlockInstantiation.suffix()
returns the PosInProgram describing
the statement just before the suffix begins
|
PosInProgram |
ContextInstantiationEntry.suffix()
returns the position of the statement just before the suffix
starts
|
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.replace(PosInProgram prefix,
PosInProgram postfix,
ExecutionContext activeStatementContext,
ProgramElement pe,
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
|
Copyright © 2003-2019 The KeY-Project.