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

Class TwoStateMethodPredicateSnippet

java.lang.Object

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

All Implemented Interfaces:

FactoryMethod

Direct Known Subclasses:

BlockCallPredicateSnippet, BlockCallWithPreconditionPredicateSnippet, LoopCallPredicateSnippet, LoopCallWithInvariantPredicateSnippet, MethodCallPredicateSnippet

abstract class TwoStateMethodPredicateSnippet
extends java.lang.Object
implements FactoryMethod

Generate term "self != null".

Author:

christoph

Constructor Summary

Constructors

Constructor and Description
TwoStateMethodPredicateSnippet()

Method Summary

Modifier and Type	Method and Description
private ImmutableList<Term>	extractTermListForPredicate(IProgramMethod pm, ProofObligationVars poVars, boolean hasMby) Parameters and the result of a method only have to appear once in the predicate.
protected Sort[]	generateContApplArgumentSorts(ImmutableList<Term> termList, IProgramMethod pm)
private Function	generateContApplPredicate(java.lang.String nameString, Sort[] argSorts, TermBuilder tb, Services services)
(package private) abstract java.lang.String	generatePredicateName(IProgramMethod pm, StatementBlock block, LoopSpecification loopInv)
private Term	instantiateContApplPredicate(Function pred, ImmutableList<Term> termList, TermBuilder tb)
Term	produce(BasicSnippetData d, ProofObligationVars poVars)

Methods inherited from class java.lang.Object

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

Constructor Detail

TwoStateMethodPredicateSnippet

TwoStateMethodPredicateSnippet()

Method Detail

produce

public Term produce(BasicSnippetData d,
                    ProofObligationVars poVars)
             throws java.lang.UnsupportedOperationException

Specified by:

produce in interface FactoryMethod

Throws:

java.lang.UnsupportedOperationException

generateContApplArgumentSorts

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

generateContApplPredicate

private Function generateContApplPredicate(java.lang.String nameString,
                                           Sort[] argSorts,
                                           TermBuilder tb,
                                           Services services)

instantiateContApplPredicate

private Term instantiateContApplPredicate(Function pred,
                                          ImmutableList<Term> termList,
                                          TermBuilder tb)

generatePredicateName

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

extractTermListForPredicate

private ImmutableList<Term> extractTermListForPredicate(IProgramMethod pm,
                                                        ProofObligationVars poVars,
                                                        boolean hasMby)

Parameters and the result of a method only have to appear once in the predicate. This method chooses the right variables out of the poVars.

Parameters:

poVars - The proof obligation variables.

Returns: