abstract class AbstractInfFlowTacletBuilder extends TermBuilder
Modifier and Type | Class and Description |
---|---|
(package private) class |
AbstractInfFlowTacletBuilder.QuantifiableVariableVisitor |
Modifier and Type | Field and Description |
---|---|
private static Name |
EQUAL_LOCS
Constant name for eqAtLocs function.
|
private static Name |
EQUAL_LOCS_POST
Constant name for eqAtLocsPost function.
|
services, WD_ANY, WD_FORMULA
Constructor and Description |
---|
AbstractInfFlowTacletBuilder(Services services) |
Modifier and Type | Method and Description |
---|---|
(package private) void |
addVarconds(RewriteTacletBuilder<? extends RewriteTaclet> tacletBuilder,
java.lang.Iterable<SchemaVariable> quantifiableSVs) |
(package private) java.util.Map<QuantifiableVariable,SchemaVariable> |
collectQuantifiableVariables(Term replaceWithTerm,
Services services) |
(package private) ImmutableList<Term> |
createTermSV(ImmutableList<Term> ts,
java.lang.String schemaPrefix,
Services services) |
(package private) Term |
createTermSV(Term t,
java.lang.String schemaPrefix,
Services services) |
(package private) SchemaVariable |
createVariableSV(QuantifiableVariable v,
java.lang.String schemaPrefix,
Services services) |
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.
|
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 static final Name EQUAL_LOCS
private static final Name EQUAL_LOCS_POST
public AbstractInfFlowTacletBuilder(Services services)
ImmutableList<Term> createTermSV(ImmutableList<Term> ts, java.lang.String schemaPrefix, Services services)
SchemaVariable createVariableSV(QuantifiableVariable v, java.lang.String schemaPrefix, Services services)
void addVarconds(RewriteTacletBuilder<? extends RewriteTaclet> tacletBuilder, java.lang.Iterable<SchemaVariable> quantifiableSVs) throws java.lang.IllegalArgumentException
java.lang.IllegalArgumentException
java.util.Map<QuantifiableVariable,SchemaVariable> collectQuantifiableVariables(Term replaceWithTerm, Services services)
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.