public static final class SimpleBlockContract.Creator extends TermBuilder
Modifier and Type | Field and Description |
---|---|
private Map<LocationVariable,Term> |
assignables |
private Behavior |
behavior |
private StatementBlock |
block |
private Map<Label,Term> |
breaks |
private Map<Label,Term> |
continues |
private Term |
diverges |
private Map<LocationVariable,Term> |
ensures |
private Map<LocationVariable,Boolean> |
hasMod |
private ImmutableList<LocationVariable> |
heaps |
private ImmutableList<InfFlowSpec> |
infFlowSpecs |
private JoinProcedure |
joinProcedure |
private List<Label> |
labels |
private IProgramMethod |
method |
private Map<LocationVariable,Term> |
requires |
private Term |
returns |
private Term |
signals |
private Term |
signalsOnly |
private BlockContract.Variables |
variables |
services, WD_ANY, WD_FORMULA
Constructor and Description |
---|
SimpleBlockContract.Creator(StatementBlock block,
List<Label> labels,
IProgramMethod method,
Behavior behavior,
BlockContract.Variables variables,
Map<LocationVariable,Term> requires,
Map<LocationVariable,Term> ensures,
ImmutableList<InfFlowSpec> infFlowSpecs,
JoinProcedure joinProcedure,
Map<Label,Term> breaks,
Map<Label,Term> continues,
Term returns,
Term signals,
Term signalsOnly,
Term diverges,
Map<LocationVariable,Term> assignables,
Map<LocationVariable,Boolean> hasMod,
Services services) |
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 StatementBlock block
private final IProgramMethod method
private final Behavior behavior
private final BlockContract.Variables variables
private final Map<LocationVariable,Term> requires
private final Map<LocationVariable,Term> ensures
private final ImmutableList<InfFlowSpec> infFlowSpecs
private final JoinProcedure joinProcedure
private final Term returns
private final Term signals
private final Term signalsOnly
private final Term diverges
private final Map<LocationVariable,Term> assignables
private final ImmutableList<LocationVariable> heaps
private final Map<LocationVariable,Boolean> hasMod
public SimpleBlockContract.Creator(StatementBlock block, List<Label> labels, IProgramMethod method, Behavior behavior, BlockContract.Variables variables, Map<LocationVariable,Term> requires, Map<LocationVariable,Term> ensures, ImmutableList<InfFlowSpec> infFlowSpecs, JoinProcedure joinProcedure, Map<Label,Term> breaks, Map<Label,Term> continues, Term returns, Term signals, Term signalsOnly, Term diverges, Map<LocationVariable,Term> assignables, Map<LocationVariable,Boolean> hasMod, Services services)
public ImmutableSet<BlockContract> create()
private Map<LocationVariable,Term> buildPreconditions()
private Map<LocationVariable,Term> buildPostconditions()
private Term buildPostcondition(LocationVariable heap)
private Term conditionPostconditions(Map<Label,ProgramVariable> flags, Map<Label,Term> postconditions)
private Term conditionPostcondition(ProgramVariable flag, Term postcondition)
private Term buildThrowPostcondition()
private Term buildNormalTerminationCondition()
private Term buildBreakTerminationCondition()
private Term buildContinueTerminationCondition()
private Term buildReturnTerminationCondition()
private Term buildThrowTerminationCondition()
private Term buildNormalTerminationCondition(Map<Label,ProgramVariable> flags)
private Term buildAbruptTerminationCondition(Map<Label,ProgramVariable> flags)
private Term buildFlagIsCondition(ProgramVariable flag, Term truth)
private Term buildExceptionIsNullCondition()
private Map<LocationVariable,Term> buildModifiesClauses()
private ImmutableSet<BlockContract> create(Map<LocationVariable,Term> preconditions, Map<LocationVariable,Term> postconditions, Map<LocationVariable,Term> modifiesClauses, ImmutableList<InfFlowSpec> infFlowSpecs, JoinProcedure joinProcedure)
private boolean ifDivergesConditionCannotBeExpressedByAModality()
private Map<LocationVariable,Term> addNegatedDivergesConditionToPreconditions(Map<LocationVariable,Term> preconditions)