Package | Description |
---|---|
de.uka.ilkd.key.control.instantiation_model | |
de.uka.ilkd.key.core | |
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.abstraction |
This package contains the meta model abstractions as used by the
semantical services.
|
de.uka.ilkd.key.java.declaration |
Elements of the Java syntax tree representing declarations.
|
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.nparser.builder | |
de.uka.ilkd.key.parser |
This package contains the parser for .key and .proof files.
|
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.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.proof.io |
Classes related to loading and saving proof files.
|
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.object_model | |
de.uka.ilkd.key.symbolic_execution.object_model.impl | |
de.uka.ilkd.key.symbolic_execution.util |
Modifier and Type | Method and Description |
---|---|
Namespace<IProgramVariable> |
TacletInstantiationModel.programVariables() |
Modifier and Type | Method and Description |
---|---|
Namespace<IProgramVariable> |
KeYMediator.progVar_ns()
returns the program variable namespace
|
Modifier and Type | Method and Description |
---|---|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ImmutableArray<Modifier> modifiers,
IProgramVariable variable,
Expression init,
KeYJavaType type)
Create a local variable declaration with an arbitrary number of
modifiers.
|
static ProgramElement |
KeYJavaASTFactory.declare(ImmutableArray<Modifier> modifiers,
IProgramVariable variable,
Expression init,
ProgramElementName typeName,
int dimensions,
ReferencePrefix typePrefix,
KeYJavaType baseType)
Create a local array variable declaration with an arbitrary number of
modifiers.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ImmutableArray<Modifier> modifiers,
IProgramVariable variable,
Expression init,
TypeReference typeRef)
Create a local variable declaration with an arbitrary number of
modifiers.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(IProgramVariable variable)
Create a local variable declaration without initialization.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(IProgramVariable variable,
Expression init)
Create a local variable declaration.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(IProgramVariable var,
Expression init,
KeYJavaType type)
Create a local variable declaration.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(IProgramVariable var,
KeYJavaType type)
Create a local variable declaration without initialization.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(Modifier[] modifiers,
IProgramVariable variable,
Expression init,
KeYJavaType type)
Create a local variable declaration with an arbitrary number of
modifiers.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(Modifier modifier,
IProgramVariable variable,
Expression init,
KeYJavaType type)
Create a local variable declaration with a single modifier.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declareMethodCall(IProgramVariable variable,
ReferencePrefix reference,
java.lang.String method)
Create a local variable declaration that assigns a method's return value
initially.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declareMethodCall(KeYJavaType type,
IProgramVariable variable,
ReferencePrefix reference,
java.lang.String method)
Create a local variable declaration that assigns a method's return value
initially.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declareZero(KeYJavaType type,
IProgramVariable variable)
Create a local variable declaration that assigns zero initially.
|
static ILoopInit |
KeYJavaASTFactory.loopInitZero(KeYJavaType type,
IProgramVariable variable)
Create a loop initialization that declares and assigns zero to a local
variable.
|
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.
|
static ParameterDeclaration |
KeYJavaASTFactory.parameterDeclaration(JavaInfo javaInfo,
KeYJavaType kjt,
IProgramVariable var)
Create a parameter declaration.
|
static VariableSpecification |
KeYJavaASTFactory.variableSpecification(IProgramVariable variable,
Expression initializer,
KeYJavaType keyJavaType)
Create a variable specification.
|
static VariableSpecification |
KeYJavaASTFactory.variableSpecification(IProgramVariable variable,
int dimensions,
Expression initializer,
Type type)
Create a variable specification.
|
Modifier and Type | Method and Description |
---|---|
JavaBlock |
Recoder2KeY.readBlockWithProgramVariables(Namespace<IProgramVariable> varns,
java.lang.String s)
parses a given JavaBlock using a namespace to determine the right
references using an empty context.
|
JavaBlock |
JavaReader.readBlockWithProgramVariables(Namespace<IProgramVariable> varns,
java.lang.String s) |
Modifier and Type | Method and Description |
---|---|
IProgramVariable |
Field.getProgramVariable()
returns the program variable associated with this field
|
Modifier and Type | Field and Description |
---|---|
protected IProgramVariable |
VariableSpecification.var |
Modifier and Type | Method and Description |
---|---|
IProgramVariable |
VariableSpecification.getProgramVariable()
Get program variable
|
Modifier and Type | Method and Description |
---|---|
static boolean |
EnumClassDeclaration.isEnumConstant(IProgramVariable attribute)
check whether a PV is an enum constant of any enum type.
|
Constructor and Description |
---|
VariableSpecification(ExtList children,
IProgramVariable var,
int dim,
Type type)
Constructor for the transformation of RECODER ASTs to KeY.
|
VariableSpecification(IProgramVariable var) |
VariableSpecification(IProgramVariable var,
Expression init,
Type type) |
VariableSpecification(IProgramVariable var,
int dim,
Expression init,
Type type) |
VariableSpecification(IProgramVariable var,
int dim,
Expression init,
Type type,
PositionInfo pi) |
VariableSpecification(IProgramVariable var,
Type type) |
Modifier and Type | Field and Description |
---|---|
protected IProgramVariable |
MergePointStatement.identifier |
protected IProgramVariable |
LoopScopeBlock.indexPV |
Modifier and Type | Method and Description |
---|---|
IProgramVariable |
LoopScopeBlock.getIndexPV()
Get expression.
|
IProgramVariable |
MethodFrame.getProgramVariable()
Get the method call header.
|
IProgramVariable |
MethodBodyStatement.getResultVariable() |
Modifier and Type | Method and Description |
---|---|
java.util.Set<IProgramVariable> |
UndeclaredProgramVariableCollector.getDeclaredVariables()
Returns the found declared variables.
|
java.util.Set<IProgramVariable> |
DeclarationProgramVariableCollector.result() |
Modifier and Type | Method and Description |
---|---|
protected void |
DeclarationProgramVariableCollector.addVariable(IProgramVariable var)
adds the given variable if we are currently at top level
|
void |
Visitor.performActionOnIProgramVariable(IProgramVariable x) |
void |
JavaASTVisitor.performActionOnIProgramVariable(IProgramVariable x) |
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 | Method and Description |
---|---|
Namespace<IProgramVariable> |
NamespaceSet.programVariables() |
Modifier and Type | Method and Description |
---|---|
void |
NamespaceSet.setProgramVariables(Namespace<IProgramVariable> progVarNS) |
Constructor and Description |
---|
NamespaceSet(Namespace<QuantifiableVariable> varNS,
Namespace<Function> funcNS,
Namespace<Sort> sortNS,
Namespace<RuleSet> ruleSetNS,
Namespace<Choice> choiceNS,
Namespace<IProgramVariable> programVarNS) |
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 |
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 |
---|---|
protected Namespace<IProgramVariable> |
DefaultBuilder.programVariables() |
Modifier and Type | Method and Description |
---|---|
Term |
DefaultTermParser.parse(java.io.Reader in,
Sort sort,
Services services,
Namespace<QuantifiableVariable> var_ns,
Namespace<Function> func_ns,
Namespace<Sort> sort_ns,
Namespace<IProgramVariable> progVar_ns,
AbbrevMap scm)
Deprecated.
The method reads the input and parses a term with the
specified namespaces.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<IProgramVariable> |
Node.getLocalProgVars()
Returns the set of created program variables known in this node.
|
ImmutableSet<IProgramVariable> |
ProgVarReplacer.replace(ImmutableSet<IProgramVariable> vars)
replaces in a set
|
Modifier and Type | Method and Description |
---|---|
void |
Node.addLocalProgVars(java.lang.Iterable<? extends IProgramVariable> elements) |
ImmutableSet<IProgramVariable> |
ProgVarReplacer.replace(ImmutableSet<IProgramVariable> vars)
replaces in a set
|
Modifier and Type | Method and Description |
---|---|
Namespace<IProgramVariable> |
InitConfig.progVarNS()
returns the program variable namespace of this initial configuration
|
Modifier and Type | Method and Description |
---|---|
static Term |
IntermediateProofReplayer.parseTerm(java.lang.String value,
Proof proof,
Namespace<QuantifiableVariable> varNS,
Namespace<IProgramVariable> progVarNS,
Namespace<Function> functNS)
Parses a given term in String representation.
|
Modifier and Type | Method and Description |
---|---|
IProgramVariable |
ExecutionNodeReader.KeYlessTermination.getExceptionVariable()
Returns the
IProgramVariable which is used in the Sequent
of Proof.root() to check if a normal or exceptional termination
occurred. |
IProgramVariable |
SymbolicLayoutReader.KeYlessValue.getProgramVariable()
Returns the represented
IProgramVariable or null if an array index is represented. |
IProgramVariable |
SymbolicLayoutReader.KeYlessAssociation.getProgramVariable()
Returns the represented
IProgramVariable . |
IProgramVariable |
ExecutionNodeReader.KeYlessVariable.getProgramVariable()
Returns the
IProgramVariable which contains the represented value. |
Modifier and Type | Method and Description |
---|---|
ISymbolicAssociation |
SymbolicLayoutReader.KeYlessState.getAssociation(IProgramVariable programVariable,
boolean isArrayIndex,
Term arrayIndex,
Term condition)
Returns the
ISymbolicAssociation with the given IProgramVariable . |
ISymbolicAssociation |
SymbolicLayoutReader.KeYlessObject.getAssociation(IProgramVariable programVariable,
boolean isArrayIndex,
Term arrayIndex,
Term condition)
Returns the
ISymbolicAssociation with the given IProgramVariable . |
ISymbolicValue |
SymbolicLayoutReader.KeYlessState.getValue(IProgramVariable programVariable,
boolean isArrayIndex,
Term arrayIndex,
Term condition)
Returns the
ISymbolicValue with the given IProgramVariable . |
ISymbolicValue |
SymbolicLayoutReader.KeYlessObject.getValue(IProgramVariable programVariable,
boolean isArrayIndex,
Term arrayIndex,
Term condition)
Returns the
ISymbolicValue with the given IProgramVariable . |
Constructor and Description |
---|
ExtractedExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
IProgramVariable programVariable,
Term arrayIndex,
Term arrayStartIndex,
Term arrayEndIndex,
Term additionalCondition,
ExecutionVariableExtractor.ExtractedExecutionValue parentValue)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
IProgramVariable |
IExecutionTermination.getExceptionVariable()
Returns the
IProgramVariable which is used in the Sequent
of Proof.root() to check if a normal or exceptional termination
occurred. |
IProgramVariable |
IExecutionVariable.getProgramVariable()
Returns the
IProgramVariable which contains the represented value. |
Modifier and Type | Method and Description |
---|---|
IProgramVariable |
ExecutionTermination.getExceptionVariable()
Returns the
IProgramVariable which is used in the Sequent
of Proof.root() to check if a normal or exceptional termination
occurred. |
IProgramVariable |
AbstractExecutionVariable.getProgramVariable()
Returns the
IProgramVariable which contains the represented value. |
Constructor and Description |
---|
AbstractExecutionVariable(ITreeSettings settings,
Node proofNode,
IProgramVariable programVariable,
IExecutionValue parentValue,
Term arrayIndex,
Term additionalCondition,
PosInOccurrence modalityPIO)
Constructor.
|
ExecutionAllArrayIndicesVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
IProgramVariable arrayProgramVariable,
Term additionalCondition)
Constructor.
|
ExecutionTermination(ITreeSettings settings,
Node proofNode,
IProgramVariable exceptionVariable,
IExecutionTermination.TerminationKind terminationKind)
Constructor.
|
ExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
IProgramVariable programVariable,
Term additionalCondition)
Constructor for a "normal" child value.
|
ExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
IProgramVariable programVariable,
Term additionalCondition)
Constructor for a "normal" value.
|
Modifier and Type | Method and Description |
---|---|
IProgramVariable |
ISymbolicValue.getProgramVariable()
Returns the represented
IProgramVariable or null if an array index is represented. |
IProgramVariable |
ISymbolicAssociation.getProgramVariable()
Returns the represented
IProgramVariable . |
Modifier and Type | Method and Description |
---|---|
ISymbolicAssociation |
ISymbolicAssociationValueContainer.getAssociation(IProgramVariable programVariable,
boolean isArrayIndex,
Term arrayIndex,
Term condition)
Returns the
ISymbolicAssociation with the given IProgramVariable . |
ISymbolicValue |
ISymbolicAssociationValueContainer.getValue(IProgramVariable programVariable,
boolean isArrayIndex,
Term arrayIndex,
Term condition)
Returns the
ISymbolicValue with the given IProgramVariable . |
Modifier and Type | Method and Description |
---|---|
IProgramVariable |
SymbolicAssociation.getProgramVariable()
Returns the represented
IProgramVariable . |
IProgramVariable |
SymbolicValue.getProgramVariable()
Returns the represented
IProgramVariable or null if an array index is represented. |
Modifier and Type | Method and Description |
---|---|
ISymbolicAssociation |
AbstractSymbolicAssociationValueContainer.getAssociation(IProgramVariable programVariable,
boolean isArrayIndex,
Term arrayIndex,
Term condition)
Returns the
ISymbolicAssociation with the given IProgramVariable . |
ISymbolicValue |
AbstractSymbolicAssociationValueContainer.getValue(IProgramVariable programVariable,
boolean isArrayIndex,
Term arrayIndex,
Term condition)
Returns the
ISymbolicValue with the given IProgramVariable . |
Constructor and Description |
---|
SymbolicAssociation(Services services,
IProgramVariable programVariable,
ISymbolicObject target,
Term condition,
IModelSettings settings)
Constructor.
|
SymbolicValue(Services services,
IProgramVariable programVariable,
Term value,
Term condition,
IModelSettings settings)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
static IProgramVariable |
SymbolicExecutionUtil.extractExceptionVariable(Proof proof)
Extracts the exception variable which is used to check if the executed program in proof terminates normally.
|
static IProgramVariable |
SymbolicExecutionUtil.findSelfTerm(Node node,
PosInOccurrence pio)
|
Modifier and Type | Method and Description |
---|---|
static java.util.List<IProgramVariable> |
SymbolicExecutionUtil.collectAllElementaryUpdateTerms(Node node)
Collects all
IProgramVariable used in ElementaryUpdate s. |
static java.util.Set<IProgramVariable> |
SymbolicExecutionUtil.getProgramVariables(FieldDeclaration fd)
Collects all
IProgramVariable s of the given FieldDeclaration . |
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 . |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractReturnVariableValueSequent(Services services,
TypeReference contextObjectType,
IProgramMethod contextMethod,
ReferencePrefix contextObject,
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 . |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractVariableValueSequent(Services services,
Node node,
PosInOccurrence pio,
Term additionalConditions,
IProgramVariable variable)
Creates a
Sequent which can be used in site proofs to
extract the value of the given IProgramVariable from the
sequent of the given Node . |
protected static ImmutableArray<Term> |
SymbolicExecutionUtil.extractValueFromUpdate(Term term,
IProgramVariable variable)
Utility method to extract the value of the
IProgramVariable
from the given update term. |
static java.lang.String |
SymbolicExecutionUtil.getDisplayString(IProgramVariable pv)
Returns the human readable name of the given
IProgramVariable . |
static boolean |
SymbolicExecutionUtil.hasReferenceSort(Services services,
IProgramVariable var)
Checks if the
Sort of the given IProgramVariable is a reference type. |
static boolean |
SymbolicExecutionUtil.isStaticVariable(IProgramVariable programVariable)
Checks if the given
IProgramVariable is static or not. |
static Sort |
SymbolicExecutionUtil.lazyComputeExceptionSort(Node node,
IProgramVariable exceptionVariable)
Computes the exception
Sort lazily when #getExceptionSort()
is called the first time. |
static boolean |
SymbolicExecutionUtil.lazyComputeIsExceptionalTermination(Node node,
IProgramVariable exceptionVariable)
Checks if is an exceptional termination.
|
Copyright © 2003-2019 The KeY-Project.