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

Class BlockCallWithPreconditionPredicateSnippet

java.lang.Object

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

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

All Implemented Interfaces:

FactoryMethod

class BlockCallWithPreconditionPredicateSnippet
extends TwoStateMethodPredicateSnippet

Generate term "self != null".

Author:

christoph

Constructor Summary

Constructors

Constructor and Description
BlockCallWithPreconditionPredicateSnippet()

Method Summary

Modifier and Type	Method and Description
(package private) java.lang.String	generatePredicateName(IProgramMethod pm, StatementBlock block, LoopSpecification loopInv)

Methods inherited from class de.uka.ilkd.key.informationflow.po.snippet.TwoStateMethodPredicateSnippet

generateContApplArgumentSorts, produce

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

BlockCallWithPreconditionPredicateSnippet

BlockCallWithPreconditionPredicateSnippet()

Method Detail

generatePredicateName

java.lang.String generatePredicateName(IProgramMethod pm,
                                       StatementBlock block,
                                       LoopSpecification loopInv)

Specified by:

generatePredicateName in class TwoStateMethodPredicateSnippet