public abstract class AbstractOperationPO extends AbstractPO
This abstract implementation of ProofOblInput
extends the
functionality of AbstractPO
to execute some code within a try catch
block.
The generated Sequent
has the following form:
==>
<generalAssumptions> &
<preconditions>
->
<updatesToStoreInitialValues>
<modalityStart>
exc=null;try {<customCode>}catch(java.lang.Throwable e) {exc = e}
<modalityEnd>
(exc = null & <postconditions > & <optionalUninterpretedPredicate>)
If isAddUninterpretedPredicate()
an uninterpreted predicate is
added to the postcondition which contains the heap and all parameters as
argument. This predicate can be used to filter out invalid execution paths
because its branches are closed while still open branches contains valid
execution paths.
AbstractPO.Vertex
IPersistablePO.LoadedPOContainer
Modifier and Type | Field and Description |
---|---|
private java.util.Set<Term> |
additionalUninterpretedPredicates
Additional uninterpreted predicates, e.g. used in the validity branch of
applied block contracts.
|
private boolean |
addSymbolicExecutionLabel
If this is
true the SymbolicExecutionTermLabel will be added
to the initial modality which is proven. |
private boolean |
addUninterpretedPredicate
If this is
true an uninterpreted predicate is added to the
postconditions which contains the heap and all parameters as arguments. |
private static java.lang.String |
JAVA_LANG_THROWABLE |
protected InitConfig |
proofConfig |
private Term |
uninterpretedPredicate
The used uninterpreted predicate created via
#buildUninterpretedPredicate(ImmutableList, ProgramVariable, String)
and available via getUninterpretedPredicate() . |
environmentConfig, environmentServices, heapLDT, javaInfo, name, poNames, poTerms, specRepos, taclets, tb
PROPERTY_ADD_SYMBOLIC_EXECUTION_LABEL, PROPERTY_ADD_UNINTERPRETED_PREDICATE, PROPERTY_CLASS, PROPERTY_FILENAME, PROPERTY_NAME
Constructor and Description |
---|
AbstractOperationPO(InitConfig initConfig,
java.lang.String name)
Constructor.
|
AbstractOperationPO(InitConfig initConfig,
java.lang.String name,
boolean addUninterpretedPredicate,
boolean addSymbolicExecutionLabel)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
static Term |
addAdditionalUninterpretedPredicateIfRequired(Services services,
Term term,
ImmutableList<LocationVariable> variablesToProtect,
Term exceptionVar)
This method adds the uninterpreted predicate to the given
Term
if the used ProofOblInput is an instance of AbstractOperationPO
and isAddUninterpretedPredicate() is true . |
private static java.util.List<LocationVariable> |
addPreHeaps(IObserverFunction target,
java.util.List<LocationVariable> modHeaps,
java.util.Map<LocationVariable,LocationVariable> atPreVars) |
private static Term |
addTransactionPrecondition(Term pre,
boolean transactionFlag,
boolean isTransactionApplicable,
Services proofServices,
TermBuilder tb) |
static Term |
addUninterpretedPredicateIfRequired(Services services,
Term term)
This method adds the uninterpreted predicate to the given
Term
if the used ProofOblInput is an instance of AbstractOperationPO
and isAddUninterpretedPredicate() is true . |
protected abstract Term |
buildFrameClause(java.util.List<LocationVariable> modHeaps,
java.util.Map<Term,Term> heapToAtPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Builds the frame clause including the modifies clause.
|
protected Term |
buildFreePre(ProgramVariable selfVar,
KeYJavaType selfKJT,
ImmutableList<ProgramVariable> paramVars,
java.util.List<LocationVariable> heaps,
Services services)
Builds the "general assumption".
|
protected JavaBlock |
buildJavaBlock(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
boolean transaction,
ImmutableList<StatementBlock> sb)
Creates the try catch block to execute.
|
protected abstract ImmutableList<StatementBlock> |
buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Builds the code to execute in different statement blocks.
1. code to execute before the try block
2. code to execute in the try block
3. code to execute in the catch block
4. code to execute in the finally block
|
protected abstract java.lang.String |
buildPOName(boolean transactionFlag)
Returns the name of the
Proof based on the given transaction flag. |
protected Term |
buildProgramTerm(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Term postTerm,
ImmutableList<StatementBlock> sb,
Services services)
Creates the
Term which contains the modality including
the complete program to execute. |
protected Term |
buildUpdate(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Builds the initial updates.
|
private static void |
collectHeapAtPres(java.util.List<LocationVariable> modHeaps,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
TermBuilder tb) |
private ImmutableList<FunctionalOperationContract> |
collectLookupContracts(IProgramMethod pm,
Services proofServices) |
private Term |
createApplyGlobalUpdateTerm(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Term preImpliesProgPost,
Services proofServices) |
private ImmutableList<LocationVariable> |
createFormalParamVars(ImmutableList<ProgramVariable> paramVars,
Services proofServices) |
private static java.util.Map<Term,Term> |
createHeapToAtPres(java.util.List<LocationVariable> modHeaps,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
TermBuilder tb) |
private Term |
createModelPOTerm(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
java.util.List<LocationVariable> modHeaps,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services proofServices) |
private Term |
createNonModelPOTerm(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
boolean transactionFlag,
java.util.List<LocationVariable> modHeaps,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services proofServices) |
private static Term |
createPermsFor(IProgramMethod pm,
java.util.List<LocationVariable> heaps,
Services proofServices,
TermBuilder tb) |
private Term |
createPost(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.List<LocationVariable> modHeaps,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
java.util.List<LocationVariable> heaps,
java.util.Map<Term,Term> heapToBefore,
Services proofServices) |
private static Term |
createProgPost(IObserverFunction target,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
java.util.List<LocationVariable> modHeaps,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Term saveBeforeHeaps,
Term representsFromContract,
Term post,
TermBuilder tb) |
protected Term |
createUninterpretedPredicate(ImmutableList<LocationVariable> formalParamVars,
Term exceptionVar,
java.lang.String name,
Services services)
|
private static Term[] |
createUpdateSubs(IObserverFunction target,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.List<LocationVariable> modHeaps,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
TermBuilder tb) |
protected Term |
ensureUninterpretedPredicateExists(ImmutableList<ProgramVariable> paramVars,
ImmutableList<LocationVariable> formalParamVars,
ProgramVariable exceptionVar,
java.lang.String name,
Services services)
Creates
uninterpretedPredicate . |
void |
fillSaveProperties(java.util.Properties properties)
This method is called by a
ProofSaver to store the proof
specific settings in the given Properties . |
protected abstract Term |
generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services) |
protected Term |
generateParamsOK(ImmutableList<ProgramVariable> paramVars)
Generates the general assumption that all parameter arguments are valid.
|
protected Term |
generateParamsOK2(ImmutableList<Term> paramVars)
Generates the general assumption that all parameter arguments are valid.
|
java.util.Set<Term> |
getAdditionalUninterpretedPredicates()
Returns the available additional uninterpreted predicates.
|
static java.util.Set<Term> |
getAdditionalUninterpretedPredicates(Proof proof)
Returns the uninterpreted predicate used in the given
Proof if available. |
protected LocationVariable |
getBaseHeap(Services services)
Returns the base heap.
|
protected abstract KeYJavaType |
getCalleeKeYJavaType()
Returns the
KeYJavaType which contains getProgramMethod() . |
protected InitConfig |
getCreatedInitConfigForSingleProof() |
protected abstract Term |
getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
ImmutableSet<NoPosTacletApp> |
getInitialTaclets() |
protected abstract Term |
getPost(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the postcondition.
|
protected abstract Term |
getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Creates the precondition.
|
protected abstract IProgramMethod |
getProgramMethod()
Returns the
IProgramMethod to call. |
private Term |
getRepresentsFromContract(IProgramMethod pm,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
java.util.List<LocationVariable> heaps,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services proofServices) |
protected LocationVariable |
getSavedHeap(Services services)
Returns the saved heap.
|
protected abstract Modality |
getTerminationMarker()
Returns the
Modality to use as termination marker. |
Term |
getUninterpretedPredicate()
Returns the used uninterpreted predicate.
|
static Term |
getUninterpretedPredicate(Proof proof)
Returns the uninterpreted predicate used in the given
Proof if available. |
protected java.lang.String |
getUninterpretedPredicateName()
Returns the name used for the uninterpreted predicate.
|
boolean |
isAddSymbolicExecutionLabel()
Checks if the modality is labeled with the
SymbolicExecutionTermLabel . |
protected static boolean |
isAddSymbolicExecutionLabel(java.util.Properties properties)
Checks if the "addSymbolicExecutionLabel" value is set in the given
Properties . |
boolean |
isAddUninterpretedPredicate()
Checks if an uninterpreted predicate is added to the postcondition or not.
|
protected static boolean |
isAddUninterpretedPredicate(java.util.Properties properties)
Checks if the "addUninterpretedPredicate" value is set in the given
Properties . |
protected boolean |
isCopyOfMethodArgumentsUsed()
Checks if a copy of the method call arguments are used instead
of the original method arguments.
|
protected boolean |
isMakeNamesUnique()
Checks if self variable, exception variable, result variable
and method call arguments should be renamed to make sure that their
names are unique in the whole KeY application.
|
protected abstract boolean |
isTransactionApplicable()
Checks if transactions are applicable.
|
protected Term |
modifyPostTerm(Services proofServices,
Term post)
Modifies the post condition with help of
POExtension.modifyPostTerm(InitConfig, Services, Term) . |
protected Term |
newAdditionalUninterpretedPredicate(ImmutableList<LocationVariable> formalParamVars,
Term exceptionVar,
java.lang.String name,
Services services)
Creates a new uninterpreted predicate which is added to
additionalUninterpretedPredicates . |
protected Services |
postInit() |
void |
readProblem() |
private void |
register(ImmutableList<ProgramVariable> paramVars,
ProgramVariable[] vars,
java.util.Collection<LocationVariable> atPreVars,
Services proofServices) |
private static Term |
saveBeforeHeaps(java.util.Map<Term,Term> heapToBefore,
TermBuilder tb) |
private boolean[] |
setTransactionFlags() |
assignPOTerms, collectClassAxioms, createProof, createProofObject, generateSelfCreated, generateSelfExactType, generateSelfExactType, generateSelfNotNull, generateWdTaclets, getContainerType, getName, getPO, implies, name, register, register, register, selectClassAxioms
private static final java.lang.String JAVA_LANG_THROWABLE
protected InitConfig proofConfig
private boolean addUninterpretedPredicate
true
an uninterpreted predicate is added to the
postconditions which contains the heap and all parameters as arguments.#buildUninterpretedPredicate(ImmutableList, String)
,
getUninterpretedPredicateName()
private boolean addSymbolicExecutionLabel
true
the SymbolicExecutionTermLabel
will be added
to the initial modality which is proven.private Term uninterpretedPredicate
#buildUninterpretedPredicate(ImmutableList, ProgramVariable, String)
and available via getUninterpretedPredicate()
.private final java.util.Set<Term> additionalUninterpretedPredicates
public AbstractOperationPO(InitConfig initConfig, java.lang.String name)
initConfig
- The InitConfig
to use.name
- The name to use.public AbstractOperationPO(InitConfig initConfig, java.lang.String name, boolean addUninterpretedPredicate, boolean addSymbolicExecutionLabel)
initConfig
- The InitConfig
to use.name
- he name to use.addUninterpretedPredicate
- true
postcondition contains
uninterpreted predicate, false
uninterpreted predicate
is not contained in postcondition.addSymbolicExecutionLabel
- true
to add the
SymbolicExecutionTermLabel
to the modality, false
to not label the modality.public static Term getUninterpretedPredicate(Proof proof)
Proof
if available.proof
- The Proof
to get its uninterpreted predicate.null
if not used.public static java.util.Set<Term> getAdditionalUninterpretedPredicates(Proof proof)
Proof
if available.proof
- The Proof
to get its uninterpreted predicate.null
if not used.public static Term addUninterpretedPredicateIfRequired(Services services, Term term)
Term
if the used ProofOblInput
is an instance of AbstractOperationPO
and isAddUninterpretedPredicate()
is true
.
Otherwise the given Term
is returned.services
- The Services
which provides the Proof
and its ProofOblInput
.term
- The Term
to modify.Term
.public static Term addAdditionalUninterpretedPredicateIfRequired(Services services, Term term, ImmutableList<LocationVariable> variablesToProtect, Term exceptionVar)
Term
if the used ProofOblInput
is an instance of AbstractOperationPO
and isAddUninterpretedPredicate()
is true
.
Otherwise the given Term
is returned.services
- The Services
which provides the Proof
and its ProofOblInput
.term
- The Term
to modify.variablesToProtect
- LocationVariable
s to protect.exceptionVar
- The exception variable to protect.Term
.protected static boolean isAddUninterpretedPredicate(java.util.Properties properties)
Properties
.properties
- The Properties
to read value from.true
is set, false
is not set.protected static boolean isAddSymbolicExecutionLabel(java.util.Properties properties)
Properties
.properties
- The Properties
to read value from.true
is set, false
is not set.private static void collectHeapAtPres(java.util.List<LocationVariable> modHeaps, java.util.Map<LocationVariable,LocationVariable> atPreVars, TermBuilder tb)
private static Term[] createUpdateSubs(IObserverFunction target, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.List<LocationVariable> modHeaps, java.util.Map<LocationVariable,LocationVariable> atPreVars, TermBuilder tb)
private static Term createPermsFor(IProgramMethod pm, java.util.List<LocationVariable> heaps, Services proofServices, TermBuilder tb)
private static java.util.List<LocationVariable> addPreHeaps(IObserverFunction target, java.util.List<LocationVariable> modHeaps, java.util.Map<LocationVariable,LocationVariable> atPreVars)
private static Term saveBeforeHeaps(java.util.Map<Term,Term> heapToBefore, TermBuilder tb)
private static java.util.Map<Term,Term> createHeapToAtPres(java.util.List<LocationVariable> modHeaps, java.util.Map<LocationVariable,LocationVariable> atPreVars, TermBuilder tb)
private static Term addTransactionPrecondition(Term pre, boolean transactionFlag, boolean isTransactionApplicable, Services proofServices, TermBuilder tb)
private static Term createProgPost(IObserverFunction target, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, java.util.List<LocationVariable> modHeaps, java.util.Map<LocationVariable,LocationVariable> atPreVars, Term saveBeforeHeaps, Term representsFromContract, Term post, TermBuilder tb)
public void readProblem() throws ProofInputException
ProofInputException
public boolean isAddUninterpretedPredicate()
true
postcondition contains uninterpreted predicate,
false
uninterpreted predicate is not contained in postcondition.public boolean isAddSymbolicExecutionLabel()
SymbolicExecutionTermLabel
.true
modality is labled, false
modality is not labled.public Term getUninterpretedPredicate()
public java.util.Set<Term> getAdditionalUninterpretedPredicates()
public void fillSaveProperties(java.util.Properties properties) throws java.io.IOException
ProofSaver
to store the proof
specific settings in the given Properties
. The stored settings
have to contain all information required to instantiate the proof
obligation again and this instance should create the same Sequent
(if code and specifications are unchanged).fillSaveProperties
in interface IPersistablePO
fillSaveProperties
in class AbstractPO
properties
- The Properties
to fill with the proof obligation specific settings.java.io.IOException
- Occurred Exception.public ImmutableSet<NoPosTacletApp> getInitialTaclets()
protected InitConfig getCreatedInitConfigForSingleProof()
getCreatedInitConfigForSingleProof
in class AbstractPO
protected Services postInit()
protected Term modifyPostTerm(Services proofServices, Term post)
POExtension.modifyPostTerm(InitConfig, Services, Term)
.proofServices
- The Services
to use.post
- The post condition to modify.protected boolean isMakeNamesUnique()
true
use unique names, false
use original
names even if they are not unique in whole KeY application.protected abstract IProgramMethod getProgramMethod()
IProgramMethod
to call.IProgramMethod
to call.protected abstract boolean isTransactionApplicable()
protected abstract KeYJavaType getCalleeKeYJavaType()
KeYJavaType
which contains getProgramMethod()
.KeYJavaType
which contains getProgramMethod()
.protected abstract ImmutableList<StatementBlock> buildOperationBlocks(ImmutableList<LocationVariable> formalParVars, ProgramVariable selfVar, ProgramVariable resultVar, Services services)
formalParVars
- Arguments from formal parameters for method call.selfVar
- The self variable.resultVar
- The result variable.services
- services instanceprotected Term buildFreePre(ProgramVariable selfVar, KeYJavaType selfKJT, ImmutableList<ProgramVariable> paramVars, java.util.List<LocationVariable> heaps, Services services)
selfVar
- The self variable.selfKJT
- The KeYJavaType
of the self variable.paramVars
- The parameters ProgramVariable
s.heaps
- The heaps.services
- The services instance.Term
containing the general assumptions.protected Term generateParamsOK(ImmutableList<ProgramVariable> paramVars)
paramVars
- The parameters ProgramVariable
s.protected Term generateParamsOK2(ImmutableList<Term> paramVars)
paramVars
- The parameters ProgramVariable
s.protected abstract Term generateMbyAtPreDef(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
protected abstract Term getPre(java.util.List<LocationVariable> modHeaps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,LocationVariable> atPreVars, Services services)
modHeaps
- The heaps.selfVar
- The self variable.paramVars
- The parameters ProgramVariable
s.atPreVars
- Mapping of LocationVariable
to the
LocationVariable
which contains the initial value.services
- The Services
to use.Term
representing the precondition.protected abstract Term getPost(java.util.List<LocationVariable> modHeaps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable exceptionVar, java.util.Map<LocationVariable,LocationVariable> atPreVars, Services services)
modHeaps
- The heaps.selfVar
- The self variable.paramVars
- The parameters ProgramVariable
s.resultVar
- The result variable.exceptionVar
- The exception variable.atPreVars
- Mapping of LocationVariable
to the
LocationVariable
which contains the initial value.services
- The Services
to use.Term
representing the postcondition.protected abstract Term getGlobalDefs(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
protected java.lang.String getUninterpretedPredicateName()
protected Term ensureUninterpretedPredicateExists(ImmutableList<ProgramVariable> paramVars, ImmutableList<LocationVariable> formalParamVars, ProgramVariable exceptionVar, java.lang.String name, Services services)
uninterpretedPredicate
.paramVars
- The parameters ProgramVariable
s.formalParamVars
- The formal parameters LocationVariable
s.exceptionVar
- The exception variable.name
- The name of the uninterpreted predicate.services
- services instance.protected Term newAdditionalUninterpretedPredicate(ImmutableList<LocationVariable> formalParamVars, Term exceptionVar, java.lang.String name, Services services)
additionalUninterpretedPredicates
.formalParamVars
- The formal parameters LocationVariable
s.exceptionVar
- The exception variable.name
- The name of the uninterpreted predicate.services
- services instance.protected Term createUninterpretedPredicate(ImmutableList<LocationVariable> formalParamVars, Term exceptionVar, java.lang.String name, Services services)
Term
to use in the postcondition of the generated
Sequent
which represents the uninterpreted predicate.formalParamVars
- The formal parameters LocationVariable
s.exceptionVar
- The exception variable.name
- The name of the uninterpreted predicate.services
- services instance.protected abstract Term buildFrameClause(java.util.List<LocationVariable> modHeaps, java.util.Map<Term,Term> heapToAtPre, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
modHeaps
- The heaps.heapToAtPre
- The previous heap before execution.selfVar
- The self variable.paramVars
- The parameters ProgramVariable
s.services
- services instanceTerm
representing the frame clause.protected Term buildProgramTerm(ImmutableList<ProgramVariable> paramVars, ImmutableList<LocationVariable> formalParamVars, ProgramVariable selfVar, ProgramVariable resultVar, ProgramVariable exceptionVar, java.util.Map<LocationVariable,LocationVariable> atPreVars, Term postTerm, ImmutableList<StatementBlock> sb, Services services)
Term
which contains the modality including
the complete program to execute.paramVars
- Formal parameters of method call.formalParamVars
- Arguments from formal parameters for method call.selfVar
- The self variable.resultVar
- The result variable.exceptionVar
- The ProgramVariable
used to store caught exceptions.atPreVars
- Mapping of LocationVariable
to the
LocationVariable
which contains the initial value.postTerm
- The post condition.sb
- The StatementBlock
to execute in try block.services
- services instance.Term
.protected LocationVariable getBaseHeap(Services services)
services
- services instance.LocationVariable
of the base heap.protected LocationVariable getSavedHeap(Services services)
services
- services instance.LocationVariable
of the saved heap.protected JavaBlock buildJavaBlock(ImmutableList<LocationVariable> formalParVars, ProgramVariable selfVar, ProgramVariable resultVar, ProgramVariable exceptionVar, boolean transaction, ImmutableList<StatementBlock> sb)
formalParVars
- Arguments from formal parameters for method call.selfVar
- The self variable.resultVar
- The result variable.exceptionVar
- The ProgramVariable
used to store caught exceptions.transaction
- Transaction flag.sb
- The StatementBlock
s to execute.JavaBlock
which contains the try catch block.protected abstract Modality getTerminationMarker()
Modality
to use as termination marker.Modality
to use as termination marker.protected Term buildUpdate(ImmutableList<ProgramVariable> paramVars, ImmutableList<LocationVariable> formalParamVars, java.util.Map<LocationVariable,LocationVariable> atPreVars, Services services)
paramVars
- Formal parameters of method call.formalParamVars
- Arguments from formal parameters for method call.atPreVars
- Mapping of LocationVariable
to the
LocationVariable
which contains the initial value.services
- The services instance.Term
representing the initial updates.protected boolean isCopyOfMethodArgumentsUsed()
true
use copy of method call arguments,
false
use original method call arguments.protected abstract java.lang.String buildPOName(boolean transactionFlag)
Proof
based on the given transaction flag.transactionFlag
- The transaction flag.private ImmutableList<LocationVariable> createFormalParamVars(ImmutableList<ProgramVariable> paramVars, Services proofServices)
private ImmutableList<FunctionalOperationContract> collectLookupContracts(IProgramMethod pm, Services proofServices)
private Term getRepresentsFromContract(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, java.util.List<LocationVariable> heaps, java.util.Map<LocationVariable,LocationVariable> atPreVars, Services proofServices)
private void register(ImmutableList<ProgramVariable> paramVars, ProgramVariable[] vars, java.util.Collection<LocationVariable> atPreVars, Services proofServices)
private Term createApplyGlobalUpdateTerm(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Term preImpliesProgPost, Services proofServices)
private Term createPost(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ImmutableList<LocationVariable> formalParamVars, ProgramVariable resultVar, ProgramVariable exceptionVar, java.util.List<LocationVariable> modHeaps, java.util.Map<LocationVariable,LocationVariable> atPreVars, java.util.List<LocationVariable> heaps, java.util.Map<Term,Term> heapToBefore, Services proofServices)
private Term createNonModelPOTerm(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable exceptionVar, boolean transactionFlag, java.util.List<LocationVariable> modHeaps, java.util.Map<LocationVariable,LocationVariable> atPreVars, Services proofServices)
private Term createModelPOTerm(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, java.util.List<LocationVariable> modHeaps, java.util.Map<LocationVariable,LocationVariable> atPreVars, Services proofServices)
private boolean[] setTransactionFlags()