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, 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 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)