| BasicBlockExecutionSnippet |
|
| BasicBlockExecutionWithPreconditionSnippet |
|
| BasicDependsSnippet |
Generate term "self !
|
| BasicFreeInvSnippet |
|
| BasicFreePreSnippet |
Generate term "self !
|
| BasicLoopExecutionSnippet |
|
| BasicLoopExecutionWithInvariantSnippet |
|
| BasicLoopInvariantSnippet |
|
| BasicMbyAtPreDefSnippet |
Generate term "self !
|
| BasicModifiesSnippet |
Generate term "self !
|
| BasicParamsOkSnippet |
Generate conjunction of
|
| BasicPOSnippetFactoryImpl |
|
| BasicPostconditionSnippet |
Generate term "self !
|
| BasicPreconditionSnippet |
Generate term "self !
|
| BasicSelfCreatedSnippet |
Generate term "self.created".
|
| BasicSelfExactTypeSnippet |
Generate term "MyClass::exactInstance(self) = TRUE".
|
| BasicSelfNotNullSnippet |
Generate term "self !
|
| BasicSnippetData |
Immutable class.
|
| BasicSymbolicExecutionSnippet |
|
| BasicSymbolicExecutionWithPreconditionSnippet |
|
| BlockCallPredicateSnippet |
Generate term "self !
|
| BlockCallWithPreconditionPredicateSnippet |
Generate term "self !
|
| InfFlowContractAppInOutRelationSnippet |
|
| InfFlowContractAppSnippet |
|
| InfFlowInputOutputRelationSnippet |
Generate term "self !
|
| InfFlowInputOutputRelationSnippet.SearchVisitor |
|
| InfFlowLoopInvAppSnippet |
|
| InfFlowPOSnippetFactoryImpl |
|
| LoopCallPredicateSnippet |
|
| LoopCallWithInvariantPredicateSnippet |
|
| MethodCallPredicateSnippet |
Generate term "self !
|
| POSnippetFactory |
|
| ReplaceAndRegisterMethod |
Generate term "self !
|
| ReplaceAndRegisterMethod.QuantifiableVariableVisitor |
|
| SelfcomposedBlockSnippet |
|
| SelfcomposedExecutionSnippet |
|
| SelfcomposedLoopSnippet |
|
| TwoStateMethodPredicateSnippet |
Generate term "self !
|