public class LoopInfFlowUnfoldTacletBuilder extends TermBuilder
services, WD_ANY, WD_FORMULA
Constructor and Description |
---|
LoopInfFlowUnfoldTacletBuilder(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 |
setExecutionContext(ExecutionContext context) |
void |
setGuard(Term guard) |
void |
setInfFlowVars(IFProofObligationVars ifVars) |
void |
setLoopInv(LoopSpecification loopInv) |
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 LoopInfFlowUnfoldTacletBuilder(Services services)
public void setLoopInv(LoopSpecification loopInv)
public void setExecutionContext(ExecutionContext context)
public void setGuard(Term guard)
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.