public static final class AuxiliaryContractBuilders.VariablesCreatorAndRegistrar
extends java.lang.Object
AuxiliaryContract.getPlaceholderVariables()
), and register them.Modifier and Type | Field and Description |
---|---|
private Goal |
goal
The current goal.
|
private AuxiliaryContract.Variables |
placeholderVariables |
private Services |
services
Services.
|
Constructor and Description |
---|
VariablesCreatorAndRegistrar(Goal goal,
AuxiliaryContract.Variables placeholderVariables,
Services services) |
Modifier and Type | Method and Description |
---|---|
private <K> java.util.Map<K,LocationVariable> |
appendSuffix(java.util.Map<K,LocationVariable> map,
java.lang.String suffix) |
AuxiliaryContract.Variables |
createAndRegister(Term self,
boolean existingPO) |
AuxiliaryContract.Variables |
createAndRegister(Term self,
boolean existingPO,
ProgramElement pe) |
AuxiliaryContract.Variables |
createAndRegisterCopies(java.lang.String suffix)
Creates and registers copies of the remembrance variables and heaps.
|
private java.util.Map<Label,ProgramVariable> |
createAndRegisterFlags(java.util.Map<Label,ProgramVariable> placeholderFlags) |
private java.util.Map<LocationVariable,LocationVariable> |
createAndRegisterRemembranceVariables(java.util.Map<LocationVariable,LocationVariable> remembranceVariables) |
private LocationVariable |
createAndRegisterVariable(ProgramVariable placeholderVariable) |
private void |
replaceOuterRemembranceVarsInInnerContracts(ProgramElement pe,
java.util.Map<LocationVariable,LocationVariable> outerRemembranceHeaps,
java.util.Map<LocationVariable,LocationVariable> outerRemembranceVariables)
Replace the outer remembrance variables of all contracts on blocks in
pe . |
private final Goal goal
private final AuxiliaryContract.Variables placeholderVariables
private final Services services
public VariablesCreatorAndRegistrar(Goal goal, AuxiliaryContract.Variables placeholderVariables, Services services)
goal
- If this is not null, all created variables are added to it. If it is null, the
variables are instead added to the services
' namespace.placeholderVariables
- the placeholders from which to create the variables.services
- services.public AuxiliaryContract.Variables createAndRegister(Term self, boolean existingPO)
self
- the self termexistingPO
- true
if we are applying a rule in an existing proof obligation,
false
if we are creating a new proof obligation.public AuxiliaryContract.Variables createAndRegister(Term self, boolean existingPO, ProgramElement pe)
self
- the self termexistingPO
- true
if we are applying a rule in an existing proof obligation,
false
if we are creating a new proof obligation.pe
- if existingPO == false
, all contracts on blocks in this
program element will have their remembrance variables replaced by
the one created here.public AuxiliaryContract.Variables createAndRegisterCopies(java.lang.String suffix)
suffix
- a suffix for the new variables' names.AuxiliaryContract.Variables
object containing the new ProgramVariables
.private <K> java.util.Map<K,LocationVariable> appendSuffix(java.util.Map<K,LocationVariable> map, java.lang.String suffix)
map
- a map containing variables.suffix
- a suffix.private java.util.Map<Label,ProgramVariable> createAndRegisterFlags(java.util.Map<Label,ProgramVariable> placeholderFlags)
placeholderFlags
- the placeholder flags.private java.util.Map<LocationVariable,LocationVariable> createAndRegisterRemembranceVariables(java.util.Map<LocationVariable,LocationVariable> remembranceVariables)
remembranceVariables
- the placeholder remembrance variables.private LocationVariable createAndRegisterVariable(ProgramVariable placeholderVariable)
placeholderVariable
- a placeholder variableprivate void replaceOuterRemembranceVarsInInnerContracts(ProgramElement pe, java.util.Map<LocationVariable,LocationVariable> outerRemembranceHeaps, java.util.Map<LocationVariable,LocationVariable> outerRemembranceVariables)
pe
.pe
- the program elements.outerRemembranceHeaps
- the new outer remembrance heaps.outerRemembranceVariables
- the new outer remembrance variables.createAndRegister(Term, boolean, ProgramElement)