Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/javapathfinder/jpf-core/wiki/JPF-core below:

JPF core · javapathfinder/jpf-core Wiki · GitHub

This is the basis for all JPF projects, i.e. you need to install it to do anything with JPF. 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.

The Git repository for jpf-core is on https://github.com/javapathfinder/jpf-core

There is also a repository for the wiki, to allow third-party contributors to provide pull requests. https://github.com/javapathfinder/jpf-wiki-sync

The contents of the wiki repository automatically get merged into the JPF wiki (within minutes after each change).

jpf-core supports two rather generic properties, which are configured by default:

• gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
• gov.nasa.jpf.vm.NotDeadlockedProperty

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.

Some of the listeners (like PreciseRaceDetector) are ListenerAdapter instances, i.e. work as more specific Property implementations.

jpf-core includes a variety of listeners that fall into three major categories:

• program properties
• execution monitoring
• execution control

Some of the main listeners are

• AssertionProperty
• IdleFilter
• ExceptionInjector

jpf-core uses many JPF properties, most of which you can find in the defaults.properties file. The following ones are of interest for users

• listener - a comma separated list of class names representing listeners that should be automatically instantiated and registered during JPF startup
• 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 registers the associated listener
• listener.<annotation-type> - class name of the listener associated with <annotation-type>
• vm.insn_factory.class - class name of a BytecodeInstructionFactory, e.g. to switch to the symbolic execution mode or to use specific bytecode implementations for checking numeric properties
• 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)
• cg.randomize_choices (random|path|def) - tells JPF if it should randomize the order of choices for each ChoiceGenerator, to avoid degenerated searches (e.g. always indexing with the main thread in scheduling choices).
• report.console.property_violation - comma-separated list of topics that should be printed by JPF if it detects an error. Possible values include
  • error error description
  • snapshot thread stacks
  • trace instruction/statement trace (can be long and memory-expensive)

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4