All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type |
Method and Description |
ImmutableList<Goal> |
apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
private static void |
applyInfFlow(Goal goal,
FunctionalOperationContract contract,
UseOperationContractRule.Instantiation inst,
Term self,
ImmutableList<Term> params,
Term result,
Term exception,
Term mby,
Term atPreUpdates,
Term finalPreTerm,
ImmutableList<UseOperationContractRule.AnonUpdateData> anonUpdateDatas,
Services services) |
static java.util.Map<LocationVariable,LocationVariable> |
computeAtPreVars(java.util.List<LocationVariable> heapContext,
TermServices services,
UseOperationContractRule.Instantiation inst) |
static UseOperationContractRule.Instantiation |
computeInstantiation(Term focusTerm,
Services services)
Computes instantiation for contract rule on passed focus term.
|
static ImmutableList<Term> |
computeParams(Term baseHeapTerm,
java.util.Map<LocationVariable,Term> atPres,
LocationVariable baseHeap,
UseOperationContractRule.Instantiation inst,
TermFactory tf) |
static ProgramVariable |
computeResultVar(UseOperationContractRule.Instantiation inst,
TermServices services) |
static Term |
computeSelf(Term baseHeapTerm,
java.util.Map<LocationVariable,Term> atPres,
LocationVariable baseHeap,
UseOperationContractRule.Instantiation inst,
Term resultTerm,
TermFactory tf) |
private static UseOperationContractRule.AnonUpdateData |
createAnonUpdate(LocationVariable heap,
IProgramMethod pm,
Term mod,
Services services) |
ContractRuleApp |
createApp(PosInOccurrence pos) |
ContractRuleApp |
createApp(PosInOccurrence pos,
TermServices services) |
java.lang.String |
displayName()
returns the display name of the rule
|
private static ImmutableList<Term> |
getActualParams(MethodOrConstructorReference mr,
ExecutionContext ec,
Services services) |
private static Term |
getActualSelf(MethodOrConstructorReference mr,
IProgramMethod pm,
ExecutionContext ec,
Services services) |
private static ImmutableSet<FunctionalOperationContract> |
getApplicableContracts(Services services,
IProgramMethod pm,
KeYJavaType kjt,
Modality modality)
Returns the operation contracts which are applicable for the passed
operation and the passed modality
|
static ImmutableSet<FunctionalOperationContract> |
getApplicableContracts(UseOperationContractRule.Instantiation inst,
Services services) |
private static Term |
getFreePost(java.util.List<LocationVariable> heapContext,
IProgramMethod pm,
KeYJavaType kjt,
Term resultTerm,
Term selfTerm,
java.util.Map<LocationVariable,Term> heapAtPres,
Term freeSpecPost,
Services services)
Construct a free postcondition for the given method,
i.e., a postcondition that is always true as guaranteed by the Java language
and is not required to be checked by the callee.
|
private static Pair<Expression,MethodOrConstructorReference> |
getMethodCall(JavaBlock jb,
Services services) |
private static PosInProgram |
getPosInProgram(JavaBlock jb) |
private static IProgramMethod |
getProgramMethod(MethodOrConstructorReference mr,
KeYJavaType staticType,
ExecutionContext ec,
Services services) |
private static KeYJavaType |
getStaticPrefixType(MethodOrConstructorReference mr,
Services services,
ExecutionContext ec) |
private static UseOperationContractRule.Instantiation |
instantiate(Term focusTerm,
Services services) |
boolean |
isApplicable(Goal goal,
PosInOccurrence pio)
returns true iff a rule is applicable at the given
position.
|
boolean |
isApplicableOnSubTerms() |
Name |
name()
the name of the rule
|
private static StatementBlock |
replaceStatement(JavaBlock jb,
StatementBlock replacement) |
java.lang.String |
toString() |