public abstract class AbstractAuxiliaryContractBuiltInRuleApp extends AbstractBuiltInRuleApp
AbstractAuxiliaryContractRule
.Modifier and Type | Field and Description |
---|---|
protected ExecutionContext |
context |
protected java.util.List<LocationVariable> |
heaps |
protected IFProofObligationVars |
infFlowVars |
private JavaStatement |
statement |
builtInRule, ifInsts, pio
Constructor and Description |
---|
AbstractAuxiliaryContractBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence occurrence,
ImmutableList<PosInOccurrence> ifInstantiations) |
Modifier and Type | Method and Description |
---|---|
boolean |
cannotComplete(Goal goal) |
boolean |
complete()
returns true if all variables are instantiated
|
abstract AuxiliaryContract |
getContract() |
ExecutionContext |
getExecutionContext() |
java.util.List<LocationVariable> |
getHeapContext() |
IFProofObligationVars |
getInformationFlowProofObligationVars() |
JavaStatement |
getStatement() |
boolean |
isSufficientlyComplete()
returns true if tryToInstantiate may be able to complete the app
|
void |
setStatement(JavaStatement s) |
void |
update(IFProofObligationVars vars,
ExecutionContext context)
Sets the proof obligation variables and execution context to new values.
|
execute, forceInstantiate, ifInsts, posInOccurrence, replacePos, rule, setIfInsts, setMutable, toString, tryToInstantiate
private JavaStatement statement
getStatement()
protected java.util.List<LocationVariable> heaps
getHeapContext()
protected IFProofObligationVars infFlowVars
getInformationFlowProofObligationVars()
protected ExecutionContext context
getExecutionContext()
public AbstractAuxiliaryContractBuiltInRuleApp(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 void setStatement(JavaStatement s)
s
- the statement (block or loop) which the applied contract belongs to.public JavaStatement getStatement()
public abstract AuxiliaryContract getContract()
public IFProofObligationVars getInformationFlowProofObligationVars()
public ExecutionContext getExecutionContext()
public java.util.List<LocationVariable> getHeapContext()
getHeapContext
in interface IBuiltInRuleApp
getHeapContext
in class AbstractBuiltInRuleApp
public boolean complete()
AbstractBuiltInRuleApp
complete
in interface RuleApp
complete
in class AbstractBuiltInRuleApp
public boolean isSufficientlyComplete()
IBuiltInRuleApp
isSufficientlyComplete
in interface IBuiltInRuleApp
isSufficientlyComplete
in class AbstractBuiltInRuleApp
public boolean cannotComplete(Goal goal)
goal
- the current goal.true
iff the rule application cannot be completed for the current goal.public void update(IFProofObligationVars vars, ExecutionContext context)
vars
- new proof obligation variables.context
- new execution context.