de.uka.ilkd.key.informationflow.po.snippet

Interfaces

• BasicPOSnippetFactory
• FactoryMethod
• InfFlowFactoryMethod
• InfFlowPOSnippetFactory

Classes

• BasicBlockExecutionSnippet
• BasicBlockExecutionWithPreconditionSnippet
• BasicDependsSnippet
• BasicFreeInvSnippet
• BasicFreePreSnippet
• BasicLoopExecutionSnippet
• BasicLoopExecutionWithInvariantSnippet
• BasicLoopInvariantSnippet
• BasicMbyAtPreDefSnippet
• BasicModifiesSnippet
• BasicParamsOkSnippet
• BasicPOSnippetFactoryImpl
• BasicPostconditionSnippet
• BasicPreconditionSnippet
• BasicSelfCreatedSnippet
• BasicSelfExactTypeSnippet
• BasicSelfNotNullSnippet
• BasicSnippetData
• BasicSymbolicExecutionSnippet
• BasicSymbolicExecutionWithPreconditionSnippet
• BlockCallPredicateSnippet
• BlockCallWithPreconditionPredicateSnippet
• InfFlowContractAppInOutRelationSnippet
• InfFlowContractAppSnippet
• InfFlowInputOutputRelationSnippet
• InfFlowInputOutputRelationSnippet.SearchVisitor
• InfFlowLoopInvAppSnippet
• InfFlowPOSnippetFactoryImpl
• LoopCallPredicateSnippet
• LoopCallWithInvariantPredicateSnippet
• MethodCallPredicateSnippet
• POSnippetFactory
• ReplaceAndRegisterMethod
• ReplaceAndRegisterMethod.QuantifiableVariableVisitor
• SelfcomposedBlockSnippet
• SelfcomposedExecutionSnippet
• SelfcomposedLoopSnippet
• TwoStateMethodPredicateSnippet

Enums

• BasicPOSnippetFactory.Snippet
• BasicSnippetData.Key
• InfFlowPOSnippetFactory.Snippet