abstract class AbstractInfFlowContractAppTacletBuilder extends AbstractInfFlowTacletBuilder
| Modifier and Type | Class and Description |
|---|---|
private class |
AbstractInfFlowContractAppTacletBuilder.InfFlowContractAppRewriteTacletBuilder
A normal RewriteTacletBuilder except that an InfFlowContractAppTaclet is
returned instead of a normal RewriteTaclet.
|
AbstractInfFlowTacletBuilder.QuantifiableVariableVisitor| Modifier and Type | Field and Description |
|---|---|
private Term[] |
contextUpdates |
private static java.lang.String |
IF_CONTRACT_APPLICATION |
private ProofObligationVars |
poVars |
(package private) static java.lang.String |
USE_IF |
services, WD_ANY, WD_FORMULA| Constructor and Description |
|---|
AbstractInfFlowContractAppTacletBuilder(Services services) |
addVarconds, 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 Term[] contextUpdates
private ProofObligationVars poVars
static final java.lang.String USE_IF
private static final java.lang.String IF_CONTRACT_APPLICATION
public AbstractInfFlowContractAppTacletBuilder(Services services)
public void setContextUpdate(Term... contextUpdates)
public void setProofObligationVars(ProofObligationVars poVars)
public Term buildContractApplPredTerm()
public Taclet buildTaclet()
abstract Name generateName()
abstract Term generateSchemaAssumes(ProofObligationVars schemaDataAssumes, Services services)
abstract Term generateSchemaFind(ProofObligationVars schemaDataFind, Services services)
abstract Term getContractApplPred(ProofObligationVars appData)
ProofObligationVars generateApplicationDataSVs(java.lang.String schemaPrefix, ProofObligationVars appData, Services services)
private Taclet genInfFlowContractApplTaclet(ProofObligationVars appData, Services services)
abstract Term buildContractApplications(ProofObligationVars contAppData, ProofObligationVars contAppData2, Services services)