public class CutHeapObjectsTermGenerator extends java.lang.Object implements TermGenerator
TermGenerator
is used by the SymbolicExecutionStrategy
to add early alias checks of used objects as target of store operations
on heaps. To achieve this, this TermGenerator
generates equality
Term
s for each possible combination of objects.Constructor and Description |
---|
CutHeapObjectsTermGenerator() |
Modifier and Type | Method and Description |
---|---|
protected void |
collectEqualityTerms(SequentFormula sf,
java.util.Set<Term> equalityTerms,
java.util.Set<Term> topTerms,
HeapLDT heapLDT,
Services services)
Computes all possible equality terms between objects in the given
SequentFormula . |
protected void |
collectStoreLocations(Term term,
java.util.Set<Term> storeLocations,
HeapLDT heapLDT)
Collects recursive all possible targets of store operations on a heap.
|
java.util.Iterator<Term> |
generate(RuleApp app,
PosInOccurrence pos,
Goal goal) |
public java.util.Iterator<Term> generate(RuleApp app, PosInOccurrence pos, Goal goal)
generate
in interface TermGenerator
protected void collectEqualityTerms(SequentFormula sf, java.util.Set<Term> equalityTerms, java.util.Set<Term> topTerms, HeapLDT heapLDT, Services services)
SequentFormula
.sf
- The SequentFormula
to work with.equalityTerms
- The result Set
with the equality Term
s to fill.topTerms
- The terms of all sequent formulasheapLDT
- The HeapLDT
to use.services
- TODO