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

Class MethodCallPredicateSnippet

java.lang.Object

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

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

All Implemented Interfaces:

FactoryMethod

class MethodCallPredicateSnippet
extends TwoStateMethodPredicateSnippet

Generate term "self != null".

Author:

christoph

Constructor Summary

Constructors

Constructor and Description
MethodCallPredicateSnippet()

Method Summary

Modifier and Type	Method and Description
protected Sort[]	generateContApplArgumentSorts(ImmutableList<Term> termList, IProgramMethod pm)
(package private) java.lang.String	generatePredicateName(IProgramMethod pm, StatementBlock block, LoopSpecification loopInv)

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

produce

Methods inherited from class java.lang.Object

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

Constructor Detail

MethodCallPredicateSnippet

MethodCallPredicateSnippet()

Method Detail

generatePredicateName

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

Specified by:

generatePredicateName in class TwoStateMethodPredicateSnippet

generateContApplArgumentSorts

protected Sort[] generateContApplArgumentSorts(ImmutableList<Term> termList,
                                               IProgramMethod pm)

Overrides:

generateContApplArgumentSorts in class TwoStateMethodPredicateSnippet