doc/jpf-core/index.md

   1 # jpf-core #
   2 This is the basis for all JPF projects, i.e. you always need to install it. jpf-core contains the basic VM and model checking infrastructure, and can be used to check for concurrency defects like deadlocks, and unhandled exceptions like `NullPointerExceptions` and `AssertionErrors`.
   3
   4
   5 ## Repository ##
   6 The Mercurial repository is on http://babelfish.arc.nasa.gov/hg/jpf/jpf-core
   7
   8 ## Properties ##
   9 jpf-core supports two rather generic properties, which are configured by default:
  10
  11  * `gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty`
  12  * `gov.nasa.jpf.jvm.NotDeadlockedProperty`
  13
  14 There is no need to parameterize any of them. `NoUncaughtExceptionsProperty` covers all `Throwable` objects that are not handled within the application, i.e. would terminate the process.
  15
  16 Some of the listeners (like `PreciseRaceDetector`) are `ListenerAdapter` instances, i.e. work as more specific Property implementations.
  17
  18 ## Listeners ##
  19 jpf-core includes a variety of [listeners](../devel/listener) that fall into three major categories:
  20
  21  * program properties
  22  * execution monitoring
  23  * execution control
  24
  25 Some of the main listeners are
  26
  27  * [AssertionProperty](./AssertionProperty)
  28  * [IdleFilter](./IdleFilter)
  29  * [ExceptionInjector](./ExceptionInjector)
  30
  31 ## Properties ##
  32 jpf-core uses many JPF properties, you can find most of them in the `defaults.properties` file. The following ones are of interest for users
  33
  34  * `listener` - a comma separated list of class names representing listeners that should be automatically instantiated and registered during JPF startup
  35  * `listener.autoload` - a comma separated list of annotation types. If JPF encounters such an annotation in one of the analyzed classes at runtime, it automatically loads and registered the associated listener
  36  * `listener.<annotation-type>` - class name of the listener associated with `<annotation-type>`
  37  * `vm.insn_factory.class` - class name of a [`BytecodeInstructionFactory`](../devel/bytecode_factory), e.g. to switch to the symbolic execution mode or to use specific bytecode implementations for checking numeric properties
  38  * `vm.halt_on_throw (true|false)` - tells JPF if it should try to find a handler if it encounters an exception in the analyzed program (useful to avoid masking exceptions within handlers)
  39  * [`cg.randomize_choices`](../user/config/random) `(random|path|def)` - tells JPF if it should randomize the order of choices for each [`ChoiceGenerator`](../devel/choicegenerator), to avoid degenerated searches (e.g. always indexing with the main thread in scheduling choices).
  40  * `report.console.property_violation` - comma separated list of topics that should be printed by JPF if it detects an error. Possible values include
  41     - `error` error description
  42     - `snapshot` thread stacks
  43     - `trace` instruction/statement trace (can be long and memory-expensive)