Package | Description |
---|---|
gov.nasa.jpf | |
gov.nasa.jpf.listener | |
gov.nasa.jpf.report | |
gov.nasa.jpf.search | |
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 |
ListenerAdapter
Adapter class that dummy implements both VMListener and SearchListener interfaces
Used to ease implementation of listeners that only process a few notifications
|
class |
PropertyListenerAdapter
abstract base class that dummy implements Property, Search- and VMListener methods
convenient for creating listeners that act as properties, just having to override
the methods they need
the only local functionality is that instances register themselves automatically
as property when the search is started
<2do> rewrite once GenericProperty is an interface
|
Modifier and Type | Method and Description |
---|---|
protected void |
JPF.addPendingSearchListener(SearchListener l) |
void |
JPF.addSearchListener(SearchListener l) |
Modifier and Type | Class and Description |
---|---|
class |
AssertionProperty
this is a property listener that turns thrown AssertionErrors into
property violations before they are caught (i.e.
|
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 |
EndlessLoopDetector
little listener that tries to detect endless while() loops by counting
backjumps, breaking transitions if the count exceeds a threshold, and
then checking if program states match.
|
class |
ErrorTraceGenerator
A lightweight listener to generate the error trace by printing
the program instructions at transition boundaries.
|
class |
ExceptionInjector
listener to inject exceptions according to user specifications.
|
class |
ExecTracker
Listener tool to monitor JPF execution.
|
class |
HeapTracker
HeapTracker - property-listener class to check heap utilization along all
execution paths (e.g.
|
class |
IdleFilter
simple combined listener that checks if a thread seems to do idle loops that
might starve other threads or JPF.
|
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 |
NoStateCycles
If there is a cycle in the states of the program, JPF doesn't execute the
already visited states.
|
class |
NumericValueChecker
little listener that checks value ranges of specified numeric fields and local vars
configuration examples:
range.fields=speed,..
|
class |
ObjectTracker
listener that keeps track of all allocations, method calls, field updates
and deallocations of instances of a set of types
we don't need a StateExtensionClient/Listener here because we only
keep live, typed object data.
|
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 |
PathOutputMonitor
listener that monitors path output, matching it against specifications
supplied as text files.
|
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 |
PreciseRaceDetector
This is a Race Detection Algorithm that is precise in its calculation of races, i.e.
|
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 |
Reporter
this is our default report generator, which is heavily configurable
via our standard properties.
|
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 |
SearchListenerAdapter
a no-action SearchListener which we can use to override only the
notifications we are interested in
|
Modifier and Type | Field and Description |
---|---|
protected SearchListener[] |
Search.listeners
search listeners.
|
Modifier and Type | Method and Description |
---|---|
void |
Search.addListener(SearchListener newListener) |
void |
Search.removeListener(SearchListener removeListener) |
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 |