public final class InfFlowBlockContractTacletBuilder extends AbstractInfFlowContractAppTacletBuilder
AbstractInfFlowTacletBuilder.QuantifiableVariableVisitor
Modifier and Type | Field and Description |
---|---|
private BlockContract |
blockContract |
private ExecutionContext |
executionContext |
USE_IF
services, 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, setProofObligationVars
addVarconds, collectQuantifiableVariables, createTermSV, createTermSV, createVariableSV, eqAtLocs, eqAtLocsPost
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
private BlockContract blockContract
private ExecutionContext executionContext
public InfFlowBlockContractTacletBuilder(Services services)
public void setContract(BlockContract contract)
public void setExecutionContext(ExecutionContext context)
Name generateName()
generateName
in class AbstractInfFlowContractAppTacletBuilder
Term generateSchemaAssumes(ProofObligationVars schemaDataAssumes, Services services)
generateSchemaAssumes
in class AbstractInfFlowContractAppTacletBuilder
Term generateSchemaFind(ProofObligationVars schemaDataFind, Services services)
generateSchemaFind
in class AbstractInfFlowContractAppTacletBuilder
Term getContractApplPred(ProofObligationVars appData)
getContractApplPred
in class AbstractInfFlowContractAppTacletBuilder
Term buildContractApplications(ProofObligationVars contAppData, ProofObligationVars contAppData2, Services services)
buildContractApplications
in class AbstractInfFlowContractAppTacletBuilder
ImmutableSet<BlockContract> filterContracts(ImmutableSet<BlockContract> ifContracts)