private static final class SimpleBlockContract.Combinator extends TermBuilder
Modifier and Type | Field and Description |
---|---|
private BlockContract[] |
contracts |
private Map<LocationVariable,Term> |
modifiesClauses |
private BlockContract.Variables |
placeholderVariables |
private Map<LocationVariable,Term> |
postconditions |
private Map<LocationVariable,Term> |
preconditions |
private Map<LocationVariable,LocationVariable> |
remembranceVariables |
services, WD_ANY, WD_FORMULA
Constructor and Description |
---|
SimpleBlockContract.Combinator(ImmutableSet<BlockContract> contracts,
Services services) |
Modifier and Type | Method and Description |
---|---|
private void |
addConditionsFrom(BlockContract contract) |
private void |
addModifiesClauseFrom(BlockContract contract,
LocationVariable heap) |
private void |
addPostconditionFrom(Term precondition,
BlockContract contract,
LocationVariable heap) |
private Term |
addPreconditionFrom(BlockContract contract,
LocationVariable heap) |
private Term |
andPossiblyNull(Term currentCondition,
Term additionalCondition) |
private BlockContract |
combine() |
private Term |
orPossiblyNull(Term currentCondition,
Term additionalCondition) |
private Term |
preify(Term formula) |
private BlockContract[] |
sort(ImmutableSet<BlockContract> 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, deepNonNull, dia, disjoint, dot, dot, dot, dotArr, dotLength, elementary, elementary, elementOf, empty, eqAtLocs, eqAtLocsPost, 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, 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
private final BlockContract[] contracts
private BlockContract.Variables placeholderVariables
private Map<LocationVariable,LocationVariable> remembranceVariables
private final Map<LocationVariable,Term> preconditions
private final Map<LocationVariable,Term> postconditions
private final Map<LocationVariable,Term> modifiesClauses
public SimpleBlockContract.Combinator(ImmutableSet<BlockContract> contracts, Services services)
private BlockContract[] sort(ImmutableSet<BlockContract> contracts)
private BlockContract combine()
private void addConditionsFrom(BlockContract contract)
private Term addPreconditionFrom(BlockContract contract, LocationVariable heap)
private void addPostconditionFrom(Term precondition, BlockContract contract, LocationVariable heap)
private void addModifiesClauseFrom(BlockContract contract, LocationVariable heap)
private Term unionPossiblyNull(Term currentLocationSet, Term additionalLocationSet)