public abstract class AbstractBlockContractBuiltInRuleApp extends AbstractAuxiliaryContractBuiltInRuleApp
AbstractBlockContractRule
.Modifier and Type | Field and Description |
---|---|
protected BlockContract |
contract |
context, heaps, infFlowVars
builtInRule, ifInsts, pio
Constructor and Description |
---|
AbstractBlockContractBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence,
ImmutableList<PosInOccurrence> ifInstantiations) |
Modifier and Type | Method and Description |
---|---|
BlockContract |
getContract() |
AbstractBlockContractBuiltInRuleApp |
tryToInstantiate(Goal goal,
AbstractBlockContractRule rule) |
void |
update(JavaStatement statement,
BlockContract contract,
java.util.List<LocationVariable> heaps) |
cannotComplete, complete, getExecutionContext, getHeapContext, getInformationFlowProofObligationVars, getStatement, isSufficientlyComplete, setStatement, update
execute, forceInstantiate, ifInsts, posInOccurrence, replacePos, rule, setIfInsts, setMutable, toString, tryToInstantiate
protected BlockContract contract
getContract()
public AbstractBlockContractBuiltInRuleApp(BuiltInRule rule, PosInOccurrence occurrence, ImmutableList<PosInOccurrence> ifInstantiations)
rule
- the rule being applied.occurrence
- the position at which the rule is applied.ifInstantiations
- if instantiations.public BlockContract getContract()
getContract
in class AbstractAuxiliaryContractBuiltInRuleApp
public AbstractBlockContractBuiltInRuleApp tryToInstantiate(Goal goal, AbstractBlockContractRule rule)
goal
- the current goal.rule
- the rule being applied.public void update(JavaStatement statement, BlockContract contract, java.util.List<LocationVariable> heaps)
statement
- the new statement.contract
- the new contract.heaps
- the new heap context.