de.uka.ilkd.key.symbolic_execution.strategy

Class CutHeapObjectsTermGenerator

java.lang.Object

de.uka.ilkd.key.symbolic_execution.strategy.CutHeapObjectsTermGenerator

All Implemented Interfaces:

TermGenerator

public class CutHeapObjectsTermGenerator
extends java.lang.Object
implements TermGenerator

This 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 Terms for each possible combination of objects.

Author:

Martin Hentschel

Constructor Summary

Constructors

Constructor and Description
CutHeapObjectsTermGenerator()

Method Summary

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)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

CutHeapObjectsTermGenerator

public CutHeapObjectsTermGenerator()

Method Detail

generate

public java.util.Iterator<Term> generate(RuleApp app,
                                         PosInOccurrence pos,
                                         Goal goal)

Specified by:

generate in interface TermGenerator

collectEqualityTerms

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.

Parameters:

sf - The SequentFormula to work with.

equalityTerms - The result Set with the equality Terms to fill.

topTerms - The terms of all sequent formulas

heapLDT - The HeapLDT to use.

services - TODO

collectStoreLocations

protected void collectStoreLocations(Term term,
                                     java.util.Set<Term> storeLocations,
                                     HeapLDT heapLDT)

Collects recursive all possible targets of store operations on a heap.

Parameters:

term - The Term to start search in.

storeLocations - The result Set to fill.

heapLDT - The HeapLDT to use (it provides the store and create Function).