public abstract class AbstractLoopContractBuiltInRuleApp extends AbstractAuxiliaryContractBuiltInRuleApp
AbstractLoopContractRule
.Modifier and Type | Field and Description |
---|---|
protected LoopContract |
contract |
context, heaps, infFlowVars
builtInRule, ifInsts, pio
Constructor and Description |
---|
AbstractLoopContractBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence,
ImmutableList<PosInOccurrence> ifInstantiations) |
Modifier and Type | Method and Description |
---|---|
LoopContract |
getContract() |
AbstractLoopContractBuiltInRuleApp |
tryToInstantiate(Goal goal,
AbstractLoopContractRule rule) |
void |
update(JavaStatement statement,
LoopContract 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 LoopContract contract
getContract()
public AbstractLoopContractBuiltInRuleApp(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 LoopContract getContract()
getContract
in class AbstractAuxiliaryContractBuiltInRuleApp
public AbstractLoopContractBuiltInRuleApp tryToInstantiate(Goal goal, AbstractLoopContractRule rule)
goal
- the current goal.rule
- the rule being applied.public void update(JavaStatement statement, LoopContract contract, java.util.List<LocationVariable> heaps)
statement
- the new statement.contract
- the new contract.heaps
- the new heap context.