public final class InfFlowBlockContractTacletBuilder extends AbstractInfFlowContractAppTacletBuilder
AbstractInfFlowTacletBuilder.QuantifiableVariableVisitor| Modifier and Type | Field and Description |
|---|---|
private BlockContract |
blockContract |
private ExecutionContext |
executionContext |
USE_IFservices, WD_ANY, WD_FORMULA| Constructor and Description |
|---|
InfFlowBlockContractTacletBuilder(Services services) |
| Modifier and Type | Method and Description |
|---|---|
(package private) Term |
buildContractApplications(ProofObligationVars contAppData,
ProofObligationVars contAppData2,
Services services) |
(package private) ImmutableSet<BlockContract> |
filterContracts(ImmutableSet<BlockContract> ifContracts) |
(package private) Name |
generateName() |
(package private) Term |
generateSchemaAssumes(ProofObligationVars schemaDataAssumes,
Services services) |
(package private) Term |
generateSchemaFind(ProofObligationVars schemaDataFind,
Services services) |
(package private) Term |
getContractApplPred(ProofObligationVars appData) |
void |
setContract(BlockContract contract) |
void |
setExecutionContext(ExecutionContext context) |
buildContractApplPredTerm, buildTaclet, generateApplicationDataSVs, setContextUpdate, setProofObligationVarsaddVarconds, collectQuantifiableVariables, createTermSV, createTermSV, createVariableSV, eqAtLocs, eqAtLocsPostacc, 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, zTermprivate BlockContract blockContract
private ExecutionContext executionContext
public InfFlowBlockContractTacletBuilder(Services services)
public void setContract(BlockContract contract)
public void setExecutionContext(ExecutionContext context)
Name generateName()
generateName in class AbstractInfFlowContractAppTacletBuilderTerm generateSchemaAssumes(ProofObligationVars schemaDataAssumes, Services services)
generateSchemaAssumes in class AbstractInfFlowContractAppTacletBuilderTerm generateSchemaFind(ProofObligationVars schemaDataFind, Services services)
generateSchemaFind in class AbstractInfFlowContractAppTacletBuilderTerm getContractApplPred(ProofObligationVars appData)
getContractApplPred in class AbstractInfFlowContractAppTacletBuilderTerm buildContractApplications(ProofObligationVars contAppData, ProofObligationVars contAppData2, Services services)
buildContractApplications in class AbstractInfFlowContractAppTacletBuilderImmutableSet<BlockContract> filterContracts(ImmutableSet<BlockContract> ifContracts)