Package | Description |
---|---|
gov.nasa.jpf.listener | |
gov.nasa.jpf.report | |
gov.nasa.jpf.util | |
gov.nasa.jpf.util.script | |
gov.nasa.jpf.vm | |
gov.nasa.jpf.vm.serialize |
Modifier and Type | Class and Description |
---|---|
class |
BudgetChecker
Listener that implements various budget constraints
|
class |
CallMonitor
this isn't yet a useful tool, but it shows how to track method calls with
their corresponding argument values
|
class |
CGMonitor |
class |
CGRemover
listener that removes CGs for specified locations, method calls or method bodies
This is an application specific state space optimizer that should be used
carefully since it has to be aware of which CGs can be removed, and which
ones can't (e.g.
|
class |
ChoiceSelector
this is a listener that only executes single choices until it detects
that it should start to search.
|
class |
ChoiceTracker
generic choice tracker tool, to produce a list of choice values that
can be used to create readable replay scripts etc.
|
class |
CoverageAnalyzer
a listener to report coverage statistics
The idea is to collect per-class/-method/-thread information about
executed instructions, and then analyze this deeper when it comes to
report time (e.g.
|
class |
DeadlockAnalyzer
example of a listener that creates property specific traces.
|
class |
ExceptionInjector
listener to inject exceptions according to user specifications.
|
class |
ExecTracker
Listener tool to monitor JPF execution.
|
class |
InsnCounter
simple tools to gather statistics about instructions executed by JPF.
|
class |
LockedStackDepth
A listener that tracks information about the stack depth of when a lock is first acquired.
|
class |
MethodAnalyzer
analyzes call/execute sequences of methods
closely modeled after the DeadlockAnalyzer, i.e.
|
class |
MethodTracker
simple tool to log method invocations
at this point, it doesn't do fancy things yet, but gives a more high
level idea of what got executed by JPF than the ExecTracker
|
class |
OOMEInjector
simulator for OutOfMemoryErrors.
|
class |
OverlappingMethodAnalyzer
this is a specialized MethodAnalyzer that looks for overlapping method
calls on the same object from different threads.
|
class |
Perturbator
listener that perturbs GETFIELD/GETSTATIC and InvokeInstruction results
NOTE - this listener initializes in two steps: (1) during listener construction
it builds a list of classes it has to monitor, and (2) during class load
time it further analyzes classes from this list to get the actual target
objects (FieldInfos and MethodInfos) so that instruction monitoring is
efficient enough.
|
class |
ReferenceLocator
tiny utility listener that can be used to find out where a certain
object (specified by reference) gets allocated or accessed (call or field),
and when it gets gc'ed
|
class |
SearchMonitor
SearchListener class to collect and report statistical
data during JPF execution.
|
class |
SearchStats
An alternative to SearchMonitor that just reports statistics at the end.
|
class |
SimpleDot
an alternative Graphviz dot-file generator for simple,educational state graphs
except of creating funny wallpapers, it doesn't help much in real life if the
state count gets > 50, but for the small ones it's actually quite readable.
|
class |
SimpleIdleFilter
This is the simple version of IdleFilter.
|
class |
StackDepthChecker
listener that throws a java.lang.StackOverflowError in case a thread
exceeds a configured max stack depth
<2do> - maybe we should only count visible stackframes, i.e.
|
class |
StackTracker
simple tool to log stack invocations
at this point, it doesn't do fancy things yet, but gives a more high
level idea of what got executed by JPF than the ExecTracker
|
class |
StateCountEstimator
From already visited states, estimates the total number of states by the branching factor.
|
class |
StateSpaceAnalyzer
a listener that collects information about ChoiceGenerators, choices and
where they are used.
|
class |
StateSpaceDot |
class |
StateTracker
simple tool to log state changes
|
class |
StopWatchFuzzer
a listener that is used to explore all paths from a time-value comparison.
|
class |
TraceStorer
tool to save traces upon various conditions like
- property violation
- call of a certain method
- reaching a certain search depth
- creating a certain thread
|
class |
VarRecorder
Simple listener tool to record the values of variables as they are accessed.
|
class |
VarTracker
simple listener tool to find out which variables (locals and fields) are
changed how often and from where.
|
Modifier and Type | Class and Description |
---|---|
class |
Statistics
simple structure to hold statistics info created by Reporters/Publishers
this is kind of a second tier SearchListener, which does not
explicitly have to be registered
<2do> this should get generic and accessible enough to replace all the
other statistics collectors, otherwise there is too much redundancy.
|
Modifier and Type | Class and Description |
---|---|
class |
StateExtensionListener<T>
generic listener that keeps track of state extensions, using
state ids as index values into a dynamic array of T objects
the purpose of this utility class is to make state extensions
backtrackable, so that clients don't have to care about this
|
class |
Trace<T>
a generic, listener- created trace over property specific operations
we could register this as a listener itself, but since it usually is used from
a listener, we might as well just delegate from there
|
Modifier and Type | Class and Description |
---|---|
class |
EventGeneratorFactory
abstract root for backtrackable event generator factories
<2do> - we don't support backtracking for sections yet! needs to be implemented for
state charts
|
Modifier and Type | Class and Description |
---|---|
class |
ConstInsnPathTime
time model that uses instruction count along current path to deduce
the execution time.
|
Modifier and Type | Class and Description |
---|---|
class |
DynamicAbstractionSerializer.Attributor |