public final class InfFlowMethodContractTacletBuilder extends AbstractInfFlowContractAppTacletBuilder
AbstractInfFlowTacletBuilder.QuantifiableVariableVisitor| Modifier and Type | Field and Description |
|---|---|
private FunctionalOperationContract |
methodContract |
USE_IFservices, WD_ANY, WD_FORMULA| Constructor and Description |
|---|
InfFlowMethodContractTacletBuilder(Services services) |
| Modifier and Type | Method and Description |
|---|---|
(package private) Term |
buildContractApplications(ProofObligationVars contAppData,
ProofObligationVars contAppData2,
Services services) |
(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) |
private ImmutableSet<InformationFlowContract> |
getInformFlowContracts(IProgramMethod pm,
Services services) |
void |
setContract(FunctionalOperationContract contract) |
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 FunctionalOperationContract methodContract
public InfFlowMethodContractTacletBuilder(Services services)
public void setContract(FunctionalOperationContract contract)
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 AbstractInfFlowContractAppTacletBuilderprivate ImmutableSet<InformationFlowContract> getInformFlowContracts(IProgramMethod pm, Services services)