Package | Description |
---|---|
de.uka.ilkd.key.informationflow.po | |
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
Modifier and Type | Method and Description |
---|---|
IFProofObligationVars |
InfFlowContractPO.getIFVars() |
IFProofObligationVars |
LoopInvExecutionPO.getLeafIFVars() |
IFProofObligationVars |
InfFlowPO.getLeafIFVars()
Get the information flow proof obligation variables (set of four sets of
proof obligation variables necessary for information flow proofs) for
the "leaf" (i.e., child of child of ..) information flow proof
obligation.
|
IFProofObligationVars |
InfFlowContractPO.getLeafIFVars() |
IFProofObligationVars |
BlockExecutionPO.getLeafIFVars() |
IFProofObligationVars |
SymbolicExecutionPO.getLeafIFVars() |
IFProofObligationVars |
IFProofObligationVars.labelHeapAtPreAsAnonHeapFunc() |
Modifier and Type | Field and Description |
---|---|
protected IFProofObligationVars |
AbstractAuxiliaryContractBuiltInRuleApp.infFlowVars |
Modifier and Type | Method and Description |
---|---|
IFProofObligationVars |
LoopInvariantBuiltInRuleApp.getInformationFlowProofObligationVars() |
IFProofObligationVars |
AbstractAuxiliaryContractBuiltInRuleApp.getInformationFlowProofObligationVars() |
Modifier and Type | Method and Description |
---|---|
void |
LoopInvariantBuiltInRuleApp.setInformationFlowProofObligationVars(IFProofObligationVars vars) |
void |
AbstractAuxiliaryContractBuiltInRuleApp.update(IFProofObligationVars vars,
ExecutionContext context)
Sets the proof obligation variables and execution context to new values.
|
Copyright © 2003-2019 The KeY-Project.