class BasicSymbolicExecutionSnippet extends ReplaceAndRegisterMethod implements FactoryMethod
Constructor and Description |
---|
BasicSymbolicExecutionSnippet() |
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) |
collectQuantifiableVariables, register, register, register, replace, replace, replace, replace, replace, replace, replaceQuantifiableVariables
public Term produce(BasicSnippetData d, ProofObligationVars poVars) throws java.lang.UnsupportedOperationException
produce
in interface FactoryMethod
java.lang.UnsupportedOperationException
private Term buildProgramTerm(BasicSnippetData d, ProofObligationVars vs, Term postTerm, TermBuilder tb)
private JavaBlock buildJavaBlock(BasicSnippetData d, ImmutableList<Term> formalPars, ProgramVariable selfVar, ProgramVariable resultVar, ProgramVariable exceptionVar, LocationVariable eVar)
private ProgramVariable[] extractProgramVariables(ImmutableList<Term> formalPars) throws java.lang.IllegalArgumentException
java.lang.IllegalArgumentException