Package | Description |
---|---|
de.uka.ilkd.key.informationflow.po | |
de.uka.ilkd.key.informationflow.po.snippet | |
de.uka.ilkd.key.informationflow.rule.tacletbuilder | |
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.expression |
Elements of the Java syntax tree representing expressions.
|
de.uka.ilkd.key.java.expression.operator |
Elements of the Java syntax tree representing operators and operator-like
expressions.
|
de.uka.ilkd.key.java.expression.operator.adt | |
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.java.visitor |
contains classes representing visitors traversing the tree
structure of Java programs.
|
de.uka.ilkd.key.ldt |
This package contains the "language data types" (LDTs) of KeY.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.logic.sort |
This package contains different kinds and implementations subtyping interface Sort.
|
de.uka.ilkd.key.proof_references.analyst | |
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.inst |
contains classes for the instantiation of schema variables of
Taclet s. |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.strategy.feature | |
de.uka.ilkd.key.symbolic_execution.slicing |
Modifier and Type | Method and Description |
---|---|
ExecutionContext |
LoopInvExecutionPO.getExecutionContext() |
ExecutionContext |
BlockExecutionPO.getExecutionContext() |
Constructor and Description |
---|
BlockExecutionPO(InitConfig initConfig,
BlockContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context) |
BlockExecutionPO(InitConfig initConfig,
BlockContract contract,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
Services services)
To be used only for auxiliary proofs where the services object of
the actual proof has to be used instead of the initial services form
the InitConfig.
|
LoopInvExecutionPO(InitConfig initConfig,
LoopSpecification loopInv,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
Term guardTerm) |
LoopInvExecutionPO(InitConfig initConfig,
LoopSpecification loopInv,
ProofObligationVars symbExecVars,
Goal initiatingGoal,
ExecutionContext context,
Term guardTerm,
Services services)
To be used only for auxiliary proofs where the services object of
the actual proof has to be used instead of the initial services form
the InitConfig.
|
Modifier and Type | Method and Description |
---|---|
static BasicPOSnippetFactory |
POSnippetFactory.getBasicFactory(BlockContract contract,
ProofObligationVars vars,
ExecutionContext context,
Services services) |
static BasicPOSnippetFactory |
POSnippetFactory.getBasicFactory(LoopSpecification invariant,
ProofObligationVars vars,
ExecutionContext context,
Term guardTerm,
Services services) |
static InfFlowPOSnippetFactory |
POSnippetFactory.getInfFlowFactory(BlockContract contract,
ProofObligationVars vars1,
ProofObligationVars vars2,
ExecutionContext context,
Services services) |
static InfFlowPOSnippetFactory |
POSnippetFactory.getInfFlowFactory(LoopSpecification invariant,
ProofObligationVars vars1,
ProofObligationVars vars2,
ExecutionContext context,
Term guardTerm,
Services services) |
Modifier and Type | Method and Description |
---|---|
void |
InfFlowBlockContractTacletBuilder.setExecutionContext(ExecutionContext context) |
void |
LoopInfFlowUnfoldTacletBuilder.setExecutionContext(ExecutionContext context) |
void |
InfFlowLoopInvariantTacletBuilder.setExecutionContext(ExecutionContext context) |
void |
BlockInfFlowUnfoldTacletBuilder.setExecutionContext(ExecutionContext context) |
Modifier and Type | Field and Description |
---|---|
protected ExecutionContext |
JavaInfo.defaultExecutionContext
The default execution context is for the case of program statements on
the top level.
|
Modifier and Type | Method and Description |
---|---|
ExecutionContext |
Recoder2KeYConverter.convert(ExecutionContext arg) |
ExecutionContext |
SchemaRecoder2KeYConverter.convert(ExecutionContext ec)
translate exection contexts
|
static ExecutionContext |
KeYJavaASTFactory.executionContext(KeYJavaType classType,
IProgramMethod method,
ReferencePrefix reference)
Create an execution context.
|
ExecutionContext |
JavaInfo.getDefaultExecutionContext()
returns the default execution context.
|
static ExecutionContext |
JavaTools.getInnermostExecutionContext(JavaBlock jb,
Services services) |
Modifier and Type | Method and Description |
---|---|
Term |
TypeConverter.convertArrayReference(ArrayReference ar,
ExecutionContext ec) |
Term |
TypeConverter.convertMethodReference(MethodReference mr,
ExecutionContext ec) |
Term |
TypeConverter.convertToLogicElement(ProgramElement pe,
ExecutionContext ec) |
Term |
TypeConverter.convertVariableReference(VariableReference fr,
ExecutionContext ec) |
static FieldReference |
KeYJavaASTFactory.fieldReference(Services services,
java.lang.String name,
Expression expression,
ExecutionContext context)
Create a field access.
|
Term |
TypeConverter.findThisForSort(Sort s,
ExecutionContext ec) |
Term |
TypeConverter.findThisForSortExact(Sort s,
ExecutionContext ec) |
KeYJavaType |
TypeConverter.getKeYJavaType(Expression e,
ExecutionContext ec)
retrieves the type of the expression e with respect to
the context in which it is evaluated
|
KeYJavaType |
Expression.getKeYJavaType(Services javaServ,
ExecutionContext ec)
returns the
KeYJavaType of an expression |
boolean |
TypeConverter.isAssignableTo(Expression expr,
Type to,
ExecutionContext ec) |
void |
PrettyPrinter.printExecutionContext(ExecutionContext x) |
java.lang.String |
JavaProgramElement.reuseSignature(Services services,
ExecutionContext ec)
this is the default implementation of the signature, which is
used to determine program similarity.
|
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
Assignment.getKeYJavaType(Services javaServ,
ExecutionContext ec)
retrieves the type of the assignment expression
|
KeYJavaType |
ArrayInitializer.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
Literal.getKeYJavaType(Services javaServ,
ExecutionContext ec)
retrieves the literal's type (as it is independant of the
execution context, it is same as using
Literal.getKeYJavaType(Services) ) |
abstract KeYJavaType |
Operator.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
ParenthesizedExpression.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
java.lang.String |
Assignment.reuseSignature(Services services,
ExecutionContext ec)
overriden from Operator
|
java.lang.String |
Operator.reuseSignature(Services services,
ExecutionContext ec)
overriden from JavaProgramElement.
|
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
SeqIndexOf.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
SeqSingleton.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
SeqReverse.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
SeqGet.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
AllFields.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
AllObjects.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
SeqLength.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
SeqSub.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
Singleton.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
MethodReference.determineStaticPrefixType(Services services,
ExecutionContext ec)
returns the static KeYJavaType of the methods prefix
|
KeYJavaType |
ArrayLengthReference.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
MetaClassReference.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
MethodReference.getKeYJavaType(Services services,
ExecutionContext ec) |
KeYJavaType |
ArrayReference.getKeYJavaType(Services services,
ExecutionContext ec) |
KeYJavaType |
SuperReference.getKeYJavaType(Services javaServ,
ExecutionContext ec)
returns the KeYJavaType
|
KeYJavaType |
ThisReference.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
VariableReference.getKeYJavaType(Services javaServ,
ExecutionContext ec)
Gets the KeY java type.
|
ImmutableList<KeYJavaType> |
MethodReference.getMethodSignature(Services services,
ExecutionContext ec)
determines the arguments types and constructs a signature of the current
method
|
IProgramMethod |
MethodReference.method(Services services,
KeYJavaType refPrefixType,
ExecutionContext ec) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
MethodBodyStatement.reuseSignature(Services services,
ExecutionContext ec) |
Modifier and Type | Method and Description |
---|---|
void |
Visitor.performActionOnExecutionContext(ExecutionContext x) |
void |
CreatingASTVisitor.performActionOnExecutionContext(ExecutionContext x) |
void |
JavaASTVisitor.performActionOnExecutionContext(ExecutionContext x) |
void |
UndeclaredProgramVariableCollector.performActionOnExecutionContext(ExecutionContext x) |
Modifier and Type | Method and Description |
---|---|
Function |
DoubleLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
CharListLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
Function |
FreeLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
MapLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
Function |
RealLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
BooleanLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
PermissionLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
LocSetLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
Function |
IntegerLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec)
returns the function symbol for the given operation
null if no function is found for the given operator
|
Function |
HeapLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
Function |
FloatLDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec) |
Function |
SeqLDT.getFunctionFor(Operator op,
Services serv,
ExecutionContext ec) |
abstract Function |
LDT.getFunctionFor(Operator op,
Services services,
ExecutionContext ec)
returns the function symbol for the given operation
|
boolean |
DoubleLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
CharListLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
FreeLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
MapLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
RealLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
BooleanLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
PermissionLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
LocSetLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
IntegerLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
HeapLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
FloatLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
boolean |
SeqLDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
abstract boolean |
LDT.isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given java
operator and the logic subterms
|
boolean |
DoubleLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
CharListLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
FreeLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
MapLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
RealLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
BooleanLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
PermissionLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
LocSetLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
IntegerLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
HeapLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
FloatLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
SeqLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
abstract boolean |
LDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given
unary java operator and the logic subterms
|
boolean |
DoubleLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
CharListLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
FreeLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
MapLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
RealLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
BooleanLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
PermissionLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
LocSetLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
IntegerLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
HeapLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
FloatLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
boolean |
SeqLDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec) |
abstract boolean |
LDT.isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given
binary java operator and the logic subterms
|
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
ProgramVariable.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
IProgramVariable.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
ProgramSV.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
Modifier and Type | Method and Description |
---|---|
boolean |
ProgramSVSort.canStandFor(ProgramElement check,
ExecutionContext ec,
Services services) |
boolean |
ProgramSVSort.SimpleExpressionStringSort.canStandFor(ProgramElement check,
ExecutionContext ec,
Services services) |
boolean |
ProgramSVSort.SimpleExpressionNonStringObjectSort.canStandFor(ProgramElement check,
ExecutionContext ec,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected ExecutionContext |
MethodCallProofReferencesAnalyst.extractContext(Node node,
Services services)
Extracts the
ExecutionContext . |
Modifier and Type | Method and Description |
---|---|
protected IProofReference<IProgramMethod> |
MethodCallProofReferencesAnalyst.createReference(Node node,
Services services,
ExecutionContext context,
MethodReference mr)
Creates an
IProofReference to the called IProgramMethod . |
Modifier and Type | Field and Description |
---|---|
ExecutionContext |
AbstractAuxiliaryContractRule.Instantiation.context
The execution context in which the block occurs.
|
protected ExecutionContext |
AbstractAuxiliaryContractBuiltInRuleApp.context |
ExecutionContext |
AbstractLoopInvariantRule.Instantiation.innermostExecutionContext |
Modifier and Type | Method and Description |
---|---|
ExecutionContext |
LoopInvariantBuiltInRuleApp.getExecutionContext() |
ExecutionContext |
AbstractAuxiliaryContractBuiltInRuleApp.getExecutionContext() |
Modifier and Type | Method and Description |
---|---|
void |
LoopInvariantBuiltInRuleApp.setExecutionContext(ExecutionContext context) |
void |
AbstractAuxiliaryContractBuiltInRuleApp.update(IFProofObligationVars vars,
ExecutionContext context)
Sets the proof obligation variables and execution context to new values.
|
Constructor and Description |
---|
Instantiation(Term update,
Term formula,
Modality modality,
Term self,
JavaStatement statement,
ExecutionContext context) |
Instantiation(Term u,
Term progPost,
While loop,
LoopSpecification inv,
Term selfTerm,
ExecutionContext innermostExecutionContext) |
Modifier and Type | Method and Description |
---|---|
ExecutionContext |
ContextStatementBlockInstantiation.activeStatementContext()
returns the execution context of the first active statement or
null if match is performed outer most
|
ExecutionContext |
ContextInstantiationEntry.activeStatementContext()
returns the execution context of the first active statement or
null if match is performed outer most
|
ExecutionContext |
SVInstantiations.getExecutionContext() |
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.
|
Term |
SVInstantiations.getTermInstantiation(SchemaVariable sv,
ExecutionContext ec,
Services services)
returns the instantiation of the given SchemaVariable as Term.
|
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
|
Modifier and Type | Method and Description |
---|---|
static ProgramVariable |
EvaluateArgs.evaluate(Expression e,
java.util.List<? super LocalVariableDeclaration> l,
Services services,
ExecutionContext ec)
TODO Comment.
|
KeYJavaType |
ProgramTransformer.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
Constructor and Description |
---|
EnhancedForElimination(ExecutionContext execContext,
EnhancedFor forStatement)
Creates a new enhaced for-loop elimination.
|
Modifier and Type | Method and Description |
---|---|
protected boolean |
ThrownExceptionFeature.filter(Term term,
Services services,
ExecutionContext ec) |
Modifier and Type | Method and Description |
---|---|
ExecutionContext |
AbstractSlicer.SequentInfo.getExecutionContext()
Returns the current
ExecutionContext . |
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractSlicer.analyzeUpdate(Term term,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext ec,
ReferencePrefix thisReference)
Recursive utility method used by
#analyzeUpdates(ImmutableList, Services, HeapLDT, Map) to analyze a given update. |
protected void |
AbstractSlicer.analyzeUpdates(ImmutableList<Term> updates,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext ec,
ReferencePrefix thisReference)
Utility method used by
#analyzeSequent(Node) to analyze the given updates. |
protected void |
AbstractSlicer.listModifiedLocations(Term term,
Services services,
HeapLDT heapLDT,
java.util.List<Location> listToFill,
ExecutionContext ec,
ReferencePrefix thisReference,
java.util.Set<Location> relevantLocations,
Node node)
|
protected Location |
AbstractSlicer.toLocation(Services services,
ReferencePrefix prefix,
ExecutionContext ec,
ReferencePrefix thisReference)
Converts the given
ReferencePrefix into a Location . |
protected ImmutableList<Access> |
AbstractSlicer.toLocationRecursive(Services services,
ReferencePrefix prefix,
ExecutionContext ec,
ReferencePrefix thisReference,
ImmutableList<Access> children)
Utility method used by
#toLocation(Services, ReferencePrefix, ReferencePrefix)
to recursively extract the Access instances. |
static Term |
AbstractSlicer.toTerm(Services services,
Expression expression,
ExecutionContext ec)
Converts the given
Expression into a Term . |
static ImmutableArray<Term> |
AbstractSlicer.toTerm(Services services,
ImmutableArray<Expression> expressions,
ExecutionContext ec)
Converts the given
Expression s into Term s. |
Constructor and Description |
---|
SequentInfo(java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext executionContext,
ReferencePrefix thisReference)
Constructor.
|
Copyright © 2003-2019 The KeY-Project.