public class InfFlowProgVarRenamer extends TermBuilder
Modifier and Type | Field and Description |
---|---|
private Goal |
goalForVariableRegistration
Goal on which newly created program variables are registered in.
|
private java.lang.String |
postfix
The postfix used for renaming, if a program variable / skolem constant
is found which is not yet in the replaceMap.
|
private java.util.Map<Term,Term> |
replaceMap
Link between program variables / skolem constants and their renamed
counterparts.
|
private Term[] |
terms
The set of terms on which the renaming should be applied.
|
services, WD_ANY, WD_FORMULA
Constructor and Description |
---|
InfFlowProgVarRenamer(Term[] terms,
java.util.Map<Term,Term> preInitialisedReplaceMap,
java.lang.String postfix,
Goal goalForVariableRegistration,
Services services) |
InfFlowProgVarRenamer(Term[] terms,
java.lang.String postfix,
Goal goalForVariableRegistration,
Services services) |
Modifier and Type | Method and Description |
---|---|
private Term[] |
applyProgramRenamingsToSubs(Term term,
java.util.Map<ProgramVariable,ProgramVariable> progVarReplaceMap) |
private void |
applyRenamingsOnSubterms(Term term) |
private void |
applyRenamingsOnUpdate(Term term) |
private Term |
applyRenamingsToPrograms(Term term,
java.util.Map<ProgramVariable,ProgramVariable> progVarReplaceMap) |
private void |
renameAndAddToReplaceMap(Term term) |
private Term |
renameFormulasWithoutPrograms(Term term) |
private JavaBlock |
renameJavaBlock(java.util.Map<ProgramVariable,ProgramVariable> progVarReplaceMap,
Term term,
Services services) |
private void |
renameProgramVariable(Term term) |
private void |
renameSkolemConstant(Term term) |
private Term[] |
renameSubs(Term term) |
Term[] |
renameVariablesAndSkolemConstants() |
private Term |
renameVariablesAndSkolemConstants(Term term) |
private java.util.Map<ProgramVariable,ProgramVariable> |
restrictToProgramVariables(java.util.Map<Term,Term> replaceMap) |
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 final Term[] terms
private final java.util.Map<Term,Term> replaceMap
private final java.lang.String postfix
private final Goal goalForVariableRegistration
public InfFlowProgVarRenamer(Term[] terms, java.util.Map<Term,Term> preInitialisedReplaceMap, java.lang.String postfix, Goal goalForVariableRegistration, Services services)
public Term[] renameVariablesAndSkolemConstants()
private void renameAndAddToReplaceMap(Term term)
private void renameProgramVariable(Term term)
private void renameSkolemConstant(Term term)
private void applyRenamingsOnUpdate(Term term)
private void applyRenamingsOnSubterms(Term term)
private Term applyRenamingsToPrograms(Term term, java.util.Map<ProgramVariable,ProgramVariable> progVarReplaceMap)
private Term[] applyProgramRenamingsToSubs(Term term, java.util.Map<ProgramVariable,ProgramVariable> progVarReplaceMap)
private JavaBlock renameJavaBlock(java.util.Map<ProgramVariable,ProgramVariable> progVarReplaceMap, Term term, Services services)
private java.util.Map<ProgramVariable,ProgramVariable> restrictToProgramVariables(java.util.Map<Term,Term> replaceMap)