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

Class ReplaceAndRegisterMethod

java.lang.Object

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

Direct Known Subclasses:

BasicBlockExecutionSnippet, BasicBlockExecutionWithPreconditionSnippet, BasicDependsSnippet, BasicLoopExecutionSnippet, BasicLoopExecutionWithInvariantSnippet, BasicLoopInvariantSnippet, BasicMbyAtPreDefSnippet, BasicModifiesSnippet, BasicPostconditionSnippet, BasicPreconditionSnippet, BasicSymbolicExecutionSnippet, BasicSymbolicExecutionWithPreconditionSnippet, InfFlowContractAppSnippet, InfFlowInputOutputRelationSnippet, InfFlowLoopInvAppSnippet, SelfcomposedBlockSnippet, SelfcomposedExecutionSnippet, SelfcomposedLoopSnippet

abstract class ReplaceAndRegisterMethod
extends java.lang.Object

Generate term "self != null".

Author:

christoph

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	ReplaceAndRegisterMethod.QuantifiableVariableVisitor

Constructor Summary

Constructors

Constructor and Description
ReplaceAndRegisterMethod()

Method Summary

Modifier and Type	Method and Description
(package private) static java.util.HashSet<QuantifiableVariable>	collectQuantifiableVariables(Term term)
(package private) void	register(Function f, Services services)
(package private) void	register(ImmutableList<ProgramVariable> pvs, Services services)
(package private) void	register(ProgramVariable pv, Services services)
(package private) InfFlowSpec[]	replace(ImmutableList<InfFlowSpec> termss, StateVars origVars, StateVars poVars, TermBuilder tb)
(package private) InfFlowSpec	replace(InfFlowSpec terms, StateVars origVars, StateVars poVars, TermBuilder tb)
(package private) Term[]	replace(Term[] terms, StateVars origVars, StateVars poVars, TermBuilder tb)
(package private) Term	replace(Term term, ProofObligationVars origVars, ProofObligationVars poVars, TermBuilder tb)
(package private) Term	replace(Term term, StateVars origVars, StateVars poVars, TermBuilder tb)
(package private) Term	replace(Term term, Term[] origVars, Term[] poVars, TermBuilder tb)
(package private) static Term	replaceQuantifiableVariables(Term term, java.util.HashSet<QuantifiableVariable> qvs, Services services)

Methods inherited from class java.lang.Object

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

Constructor Detail

ReplaceAndRegisterMethod

ReplaceAndRegisterMethod()

Method Detail

replace

final Term replace(Term term,
                   ProofObligationVars origVars,
                   ProofObligationVars poVars,
                   TermBuilder tb)

replace

final Term replace(Term term,
                   StateVars origVars,
                   StateVars poVars,
                   TermBuilder tb)

replace

final Term[] replace(Term[] terms,
                     StateVars origVars,
                     StateVars poVars,
                     TermBuilder tb)

replace

final InfFlowSpec replace(InfFlowSpec terms,
                          StateVars origVars,
                          StateVars poVars,
                          TermBuilder tb)

replace

final InfFlowSpec[] replace(ImmutableList<InfFlowSpec> termss,
                            StateVars origVars,
                            StateVars poVars,
                            TermBuilder tb)

replace

final Term replace(Term term,
                   Term[] origVars,
                   Term[] poVars,
                   TermBuilder tb)

register

final void register(ProgramVariable pv,
                    Services services)

register

final void register(ImmutableList<ProgramVariable> pvs,
                    Services services)

register

final void register(Function f,
                    Services services)

replaceQuantifiableVariables

static final Term replaceQuantifiableVariables(Term term,
                                               java.util.HashSet<QuantifiableVariable> qvs,
                                               Services services)

collectQuantifiableVariables

static final java.util.HashSet<QuantifiableVariable> collectQuantifiableVariables(Term term)