T
- the type of the subclass.protected abstract static class AbstractAuxiliaryContractImpl.Combinator<T extends AuxiliaryContract> extends TermBuilder
Modifier and Type | Field and Description |
---|---|
protected T[] |
contracts
The contracts to combine.
|
protected java.util.Map<LocationVariable,Term> |
modifiesClauses |
protected AuxiliaryContract.Variables |
placeholderVariables |
protected java.util.Map<LocationVariable,Term> |
postconditions |
protected java.util.Map<LocationVariable,Term> |
preconditions |
protected java.util.Map<LocationVariable,LocationVariable> |
remembranceVariables |
services, WD_ANY, WD_FORMULA
Constructor and Description |
---|
Combinator(T[] contracts,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected void |
addConditionsFrom(T contract) |
private void |
addModifiesClauseFrom(T contract,
LocationVariable heap) |
private void |
addPostconditionFrom(Term postcondition,
T contract,
LocationVariable heap) |
private Term |
addPreconditionFrom(T contract,
LocationVariable heap) |
private Term |
andPossiblyNull(Term currentCondition,
Term additionalCondition) |
protected abstract T |
combine() |
private Term |
orPossiblyNull(Term currentCondition,
Term additionalCondition) |
private Term |
preify(Term formula) |
private T[] |
sort(T[] contracts) |
private Term |
unionPossiblyNull(Term currentLocationSet,
Term additionalLocationSet) |
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
protected final T extends AuxiliaryContract[] contracts
protected AuxiliaryContract.Variables placeholderVariables
protected java.util.Map<LocationVariable,LocationVariable> remembranceVariables
Variables#remembranceLocalVariables
protected final java.util.Map<LocationVariable,Term> preconditions
protected final java.util.Map<LocationVariable,Term> postconditions
protected final java.util.Map<LocationVariable,Term> modifiesClauses
private T[] sort(T[] contracts)
contracts
- the contract's to sort.protected abstract T combine()
protected void addConditionsFrom(T contract)
contract
- the contract whose conditions to add.private Term addPreconditionFrom(T contract, LocationVariable heap)
contract
- the contract whose precondition to add.heap
- the heap to use.private void addPostconditionFrom(Term postcondition, T contract, LocationVariable heap)
postcondition
- the postcondition to add.contract
- the contract the postcondition belongs to.heap
- the heap to use.private void addModifiesClauseFrom(T contract, LocationVariable heap)
contract
- the contract whose modified clause to add.heap
- the heap to use.private Term orPossiblyNull(Term currentCondition, Term additionalCondition)
currentCondition
- a condition or null
.additionalCondition
- a condition.private Term andPossiblyNull(Term currentCondition, Term additionalCondition)
currentCondition
- a condition or null
.additionalCondition
- a condition.private Term unionPossiblyNull(Term currentLocationSet, Term additionalLocationSet)
currentLocationSet
- a location set or null
.additionalLocationSet
- a location set.