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 !
|