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

Class BasicSymbolicExecutionSnippet

java.lang.Object

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

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

All Implemented Interfaces:

FactoryMethod

class BasicSymbolicExecutionSnippet
extends ReplaceAndRegisterMethod
implements FactoryMethod

Author:

christoph

Constructor Summary

Constructors

Constructor and Description
BasicSymbolicExecutionSnippet()

Method Summary

Modifier and Type	Method and Description
private JavaBlock	buildJavaBlock(BasicSnippetData d, ImmutableList<Term> formalPars, ProgramVariable selfVar, ProgramVariable resultVar, ProgramVariable exceptionVar, LocationVariable eVar)
private Term	buildProgramTerm(BasicSnippetData d, ProofObligationVars vs, Term postTerm, TermBuilder tb)
private ProgramVariable[]	extractProgramVariables(ImmutableList<Term> formalPars)
Term	produce(BasicSnippetData d, ProofObligationVars poVars)

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

collectQuantifiableVariables, register, register, register, replace, replace, replace, replace, replace, replace, replaceQuantifiableVariables

Methods inherited from class java.lang.Object

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

Constructor Detail

BasicSymbolicExecutionSnippet

BasicSymbolicExecutionSnippet()

Method Detail

produce

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

Specified by:

produce in interface FactoryMethod

Throws:

java.lang.UnsupportedOperationException

buildProgramTerm

private Term buildProgramTerm(BasicSnippetData d,
                              ProofObligationVars vs,
                              Term postTerm,
                              TermBuilder tb)

buildJavaBlock

private JavaBlock buildJavaBlock(BasicSnippetData d,
                                 ImmutableList<Term> formalPars,
                                 ProgramVariable selfVar,
                                 ProgramVariable resultVar,
                                 ProgramVariable exceptionVar,
                                 LocationVariable eVar)

extractProgramVariables

private ProgramVariable[] extractProgramVariables(ImmutableList<Term> formalPars)
                                           throws java.lang.IllegalArgumentException

Throws:

java.lang.IllegalArgumentException