| Interface | Description |
|---|---|
| InfFlowCompositePO | |
| InfFlowLeafPO | |
| InfFlowPO |
| Class | Description |
|---|---|
| AbstractInfFlowPO |
Abstract to customize
AbstractPO and AbstractOperationPO. |
| BlockExecutionPO | |
| IFProofObligationVars |
This class contains the set of four sets of ProofObligationVars necessary for
information flow proofs.
|
| InfFlowContractPO | |
| InfFlowProofSymbols | |
| LoopInvExecutionPO | |
| SymbolicExecutionPO |