proguard.analysis.cpa.jvm.domain.memory

Interface TraceExtractor

All Known Implementing Classes:

JvmMemoryLocationBamCpaRun, JvmTaintMemoryLocationBamCpaRun

public interface TraceExtractor

This interfaces containts helper methods for CpaRuns producing witness traces.

Method Summary

Modifier and Type	Method and Description
default java.util.Set<java.util.List<BamLocationDependentJvmMemoryLocation>>	extractLinearTraces() Returns a set of linear witness traces.
java.util.Collection<BamLocationDependentJvmMemoryLocation<?>>	getEndPoints() Returns endpoints or the extracted traces.
ProgramLocationDependentReachedSet<JvmCfaNode,JvmCfaEdge,JvmMemoryLocationAbstractState<?>,MethodSignature>	getOutputReachedSet() Returns the reached set of a trace extracting memory location CPA.
default java.util.List<BamLocationDependentJvmMemoryLocation>	removeDuplicateProgramLocations(java.util.List<BamLocationDependentJvmMemoryLocation> trace)
default void	traceExtractionIteration(java.util.Set<java.util.List<BamLocationDependentJvmMemoryLocation>> result, java.util.List<BamLocationDependentJvmMemoryLocation> currentTrace)

Method Detail

extractLinearTraces

default java.util.Set<java.util.List<BamLocationDependentJvmMemoryLocation>> extractLinearTraces()

Returns a set of linear witness traces.

getEndPoints

java.util.Collection<BamLocationDependentJvmMemoryLocation<?>> getEndPoints()

Returns endpoints or the extracted traces. Its output should be used for constructing initial states for memory location CPAs.

getOutputReachedSet

ProgramLocationDependentReachedSet<JvmCfaNode,JvmCfaEdge,JvmMemoryLocationAbstractState<?>,MethodSignature> getOutputReachedSet()

Returns the reached set of a trace extracting memory location CPA.

traceExtractionIteration

default void traceExtractionIteration(java.util.Set<java.util.List<BamLocationDependentJvmMemoryLocation>> result,
                                      java.util.List<BamLocationDependentJvmMemoryLocation> currentTrace)

removeDuplicateProgramLocations

default java.util.List<BamLocationDependentJvmMemoryLocation> removeDuplicateProgramLocations(java.util.List<BamLocationDependentJvmMemoryLocation> trace)