public static class AuxiliaryContract.VariablesCreator extends TermBuilder
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
BREAK_FLAG_BASE_NAME
Base name for all break flags.
|
private java.util.Map<Label,ProgramVariable> |
breakFlags |
static java.lang.String |
CONTINUE_FLAG_BASE_NAME
Base name for all continue flags.
|
private java.util.Map<Label,ProgramVariable> |
continueFlags |
static java.lang.String |
FLAG_INFIX
Infix used between a flag's base name and the label name.
|
private java.util.List<Label> |
labels |
private IProgramMethod |
method |
static java.lang.String |
OUTER_REMEMBRANCE_SUFFIX
Suffix for all outer remembrance variables.
|
static java.lang.String |
REMEMBRANCE_SUFFIX
Suffix for all remembrance variables.
|
static java.lang.String |
RETURN_FLAG_NAME
Name for the return flag.
|
private ProgramVariable |
returnFlag |
private JavaStatement |
statement |
services, WD_ANY, WD_FORMULA
Constructor and Description |
---|
VariablesCreator(JavaStatement statement,
java.util.List<Label> labels,
IProgramMethod method,
Services services)
Constructor.
|
acc, add, addLabel, addLabel, all, all, allClose, allFields, allLocs, allObjects, and, and, and, andPreserveLabels, andPreserveLabels, andSC, andSC, andSC, anon, anonUpd, apply, apply, apply, applyElementary, applyElementary, applyElementary, applyParallel, applyParallel, applyParallel, applySequential, applySequential, applyUpdatePairsSequential, arr, arrayRange, arrayStore, box, bprod, bsum, cast, classErroneous, classInitializationInProgress, classInitialized, classPrepared, convertToBoolean, convertToFormula, create, created, created, createdInHeap, createdLocs, cTerm, deepNonNull, dia, disjoint, dot, dot, dot, dotArr, dotLength, elementary, elementary, elementOf, empty, equals, ex, ex, exactInstance, excVar, excVar, FALSE, ff, fieldStore, forallHeaps, frame, frameStrictlyEmpty, freshLocs, func, func, func, func, func, func, geq, getBaseHeap, getMeasuredByEmpty, getSorts, goBelowUpdates, goBelowUpdates2, gt, heapAtPreVar, heapAtPreVar, ife, ifEx, ifEx, imp, imp, impPreserveLabels, inByte, inChar, index, indexOf, infiniteUnion, infiniteUnion, inInt, initialized, inLong, inShort, instance, intersect, intersect, intersect, inv, inv, label, label, leq, lt, max, measuredBy, measuredByCheck, measuredByEmpty, min, newName, newName, newName, not, notPreserveLabels, NULL, one, open, or, or, or, orPreserveLabels, orPreserveLabels, orSC, orSC, orSC, pair, parallel, parallel, parallel, parallel, parallel, paramVars, paramVars, parseTerm, parseTerm, permissionsFor, permissionsFor, prec, prod, prog, prog, reach, reachableValue, reachableValue, reachableValue, resultVar, resultVar, select, select, selfVar, selfVar, selfVar, selfVar, seq, seq, seqConcat, seqDef, seqEmpty, seqGet, seqLen, seqReverse, seqSingleton, seqSub, sequential, sequential, sequential, setComprehension, setComprehension, setMinus, shortBaseName, shortcut, singleton, skip, staticDot, staticDot, staticFieldStore, staticInv, staticInv, store, strictlyNothing, subset, subst, subst, sum, tf, TRUE, tt, union, union, union, unionToSet, unlabel, unlabelRecursive, values, var, var, var, var, var, var, wd, wd, wd, wellFormed, wellFormed, zero, zTerm, zTerm
public static final java.lang.String BREAK_FLAG_BASE_NAME
public static final java.lang.String CONTINUE_FLAG_BASE_NAME
public static final java.lang.String RETURN_FLAG_NAME
public static final java.lang.String FLAG_INFIX
public static final java.lang.String REMEMBRANCE_SUFFIX
public static final java.lang.String OUTER_REMEMBRANCE_SUFFIX
private final JavaStatement statement
private final java.util.List<Label> labels
AuxiliaryContract.getLabels()
private final IProgramMethod method
AuxiliaryContract.getMethod()
private java.util.Map<Label,ProgramVariable> breakFlags
AuxiliaryContract.Variables.breakFlags
private java.util.Map<Label,ProgramVariable> continueFlags
private ProgramVariable returnFlag
AuxiliaryContract.Variables.returnFlag
public VariablesCreator(JavaStatement statement, java.util.List<Label> labels, IProgramMethod method, Services services)
statement
- the block or loop the contract belongs to.labels
- all labels belonging to the block.method
- the method containing the block.services
- services.public AuxiliaryContract.Variables create()
Variables
object.private void createAndStoreFlags()
breakFlags
,
continueFlags
,
returnFlag
private java.util.Set<Label> collectLabels(java.util.List<? extends LabelJumpStatement> jumps)
jumps
- a list of jump statements.private java.util.Map<Label,ProgramVariable> createFlags(java.util.Set<Label> labels, java.lang.String baseName)
labels
- the labels.baseName
- the base name for the flags.private ProgramVariable createFlag(java.lang.String name)
name
- a name.private java.util.Map<LocationVariable,LocationVariable> createRemembranceHeaps()
AuxiliaryContract.Variables.remembranceHeaps
private java.util.Map<LocationVariable,LocationVariable> createRemembranceHeaps(java.lang.String suffix)
suffix
- the suffix to use for the remembrance heaps.AuxiliaryContract.Variables.remembranceHeaps
,
AuxiliaryContract.Variables.outerRemembranceHeaps
private java.util.Map<LocationVariable,LocationVariable> createRemembranceLocalVariables()
AuxiliaryContract.Variables.remembranceLocalVariables
private java.util.Map<LocationVariable,LocationVariable> createOuterRemembranceHeaps()
AuxiliaryContract.Variables.outerRemembranceHeaps
private java.util.Map<LocationVariable,LocationVariable> createOuterRemembranceLocalVariables()
AuxiliaryContract.Variables.outerRemembranceVariables
private LocationVariable createVariable(java.lang.String name, KeYJavaType type)
name
- a base name.type
- a type.