public class MethodInfFlowUnfoldTacletBuilder extends TermBuilder
services, WD_ANY, WD_FORMULA
Constructor and Description |
---|
MethodInfFlowUnfoldTacletBuilder(Services services) |
Modifier and Type | Method and Description |
---|---|
Taclet |
buildTaclet() |
Term |
eqAtLocs(Services services,
Term heap1,
Term locset1,
Term heap2,
Term locset2)
Get eqAtLocs function as a term.
|
Term |
eqAtLocsPost(Services services,
Term heap1Pre,
Term heap1Post,
Term locset1,
Term heap2Pre,
Term heap2Post,
Term locset2)
Get eqAtLocsPost function as a term.
|
void |
setContract(InformationFlowContract c) |
void |
setInfFlowVars(IFProofObligationVars ifVars) |
void |
setReplacewith(Term replacewith) |
acc, add, addLabel, addLabel, addLabelToAllSubs, addLabelToAllSubs, 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, replace, 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
public MethodInfFlowUnfoldTacletBuilder(Services services)
public void setContract(InformationFlowContract c)
public void setInfFlowVars(IFProofObligationVars ifVars)
public void setReplacewith(Term replacewith)
public Taclet buildTaclet()
public Term eqAtLocs(Services services, Term heap1, Term locset1, Term heap2, Term locset2)
services
- the Services object.heap1
- the first heap term.locset1
- the first location set term.heap2
- the first heap term.locset2
- the first location set term.public Term eqAtLocsPost(Services services, Term heap1Pre, Term heap1Post, Term locset1, Term heap2Pre, Term heap2Post, Term locset2)
services
- the Services object.heap1Pre
- the first pre-heap term.heap1Post
- the first post-heap term.locset1
- the first location set term.heap2Pre
- the second pre-heap term.heap2Post
- the second post-heap term.locset2
- the second location set term.Copyright © 2003-2019 The KeY-Project.