public class BlockContractExternalBuiltInRuleApp extends AbstractBlockContractBuiltInRuleApp
BlockContractExternalRule
.contract
context, heaps, infFlowVars
builtInRule, ifInsts, pio
Constructor and Description |
---|
BlockContractExternalBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence) |
BlockContractExternalBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence,
ImmutableList<PosInOccurrence> ifInstantiations,
JavaStatement statement,
BlockContract contract,
java.util.List<LocationVariable> heaps) |
Modifier and Type | Method and Description |
---|---|
BlockContractExternalBuiltInRuleApp |
replacePos(PosInOccurrence newOccurrence) |
BlockContractExternalBuiltInRuleApp |
setIfInsts(ImmutableList<PosInOccurrence> ifInstantiations) |
BlockContractExternalBuiltInRuleApp |
tryToInstantiate(Goal goal)
Tries to complete the rule application from the available information.
|
getContract, tryToInstantiate, update
cannotComplete, complete, getExecutionContext, getHeapContext, getInformationFlowProofObligationVars, getStatement, isSufficientlyComplete, setStatement, update
execute, forceInstantiate, ifInsts, posInOccurrence, rule, setMutable, toString
public BlockContractExternalBuiltInRuleApp(BuiltInRule rule, PosInOccurrence occurrence)
rule
- the rule being applied.occurrence
- the position at which the rule is applied.public BlockContractExternalBuiltInRuleApp(BuiltInRule rule, PosInOccurrence occurrence, ImmutableList<PosInOccurrence> ifInstantiations, JavaStatement statement, BlockContract contract, java.util.List<LocationVariable> heaps)
rule
- the rule being applied.occurrence
- the position at which the rule is applied.ifInstantiations
- if instantiations.statement
- the statement which the applied contract belongs to.contract
- the contract being applied.heaps
- the heap context.public BlockContractExternalBuiltInRuleApp replacePos(PosInOccurrence newOccurrence)
replacePos
in interface IBuiltInRuleApp
replacePos
in class AbstractBuiltInRuleApp
public BlockContractExternalBuiltInRuleApp setIfInsts(ImmutableList<PosInOccurrence> ifInstantiations)
setIfInsts
in interface IBuiltInRuleApp
setIfInsts
in class AbstractBuiltInRuleApp
public BlockContractExternalBuiltInRuleApp tryToInstantiate(Goal goal)
IBuiltInRuleApp
UserInterfaceControl
to complete a built-in rule.
Returns a complete app only if there is exactly one contract.
If you want a complete app for combined contracts, use forceInstantiate
instead.
For an example implementation see e.g. UseOperationContractRule
or UseDependencyContractRule
.tryToInstantiate
in interface IBuiltInRuleApp
tryToInstantiate
in class AbstractBuiltInRuleApp