=== JNuke ===

This is the 'Jnuke' framework for checking Java bytecode.  It is written
in C and entirely self-contained, although it can be linked against zlib.

JNuke contains all the necessary infrastructure to load, manipulate,
and analyze Java bytecode. It has been tested for Java bytecode generated
by compilers up to version 1.6, but does not directly support generics.
Furthermore, dynamic (scripting) languages that can be compiled to Java
bytecode using the new "invokedynamic" instruction are not supported.

--- Features ---

For an overview of the capabilities of JNuke, please see "toolpaper04"
and "thesis" in "doc".

If the class libraries for a given application are available, its analysis
capabilites are as follows:

* Static analysis: A static analysis for atomicity races has been
  implemented under "sa". Most of the analysis logics can also be
  used for dynamic analysis, and are contained in module "algo".
  See "bl-atomicity" and "toolpaper05" in "doc" for more information.

* Dynamic analysis: Multiple categories are available here.

  - Bytecode execution: Module "vm" implements bytecode execution,
    similar to a normal Java VM. Application "jnukevm" in "bin" provides
    a command line frontend.

  - Model checking, also implemented in "vm". For later analysis,
    the schedule leading to a failure can be captured using front end
    "jcapture" in "bin".

  - Replaying a given schedule: "jreplay" in "bin".

  - Run-time verification, in "rv". Implemented algorithms include
    Eraser, high-level data races, and variations of the ExitBlock
    algorithms; the latter ones are used by the model checker.

--- Compilation ---

The main compilation target is "testjnuke", a front end to all unit tests,
which run the entire functionality of JNuke. This target is built after
configuration, using

    ./configure && make

should create it. To compile, a C compiler (such as gcc 4.2) is
required. Having zlib and a Java development environment installed will
allow optional features to be included.

The system has been tested under Ubuntu Linux 9.4, and Mac OS 10.6.3.
For an overview of all configuration options, please run

    ./configure -h

--- Usage ---

Command line front ends are available as jcapture, jnukevm, and jreplay
(see above), compiled by

    make apps

The front ends all have a help function, obtained by calling the
application followed by "-h" or "--help", e.g.

    ./bin/jnukevm -h

Most uses are not covered by the front ends. In those cases, the unit
test front end has to be used; see section 8.7 in "doc/thesis" for a
detailed documentation.

--- Test data ---

In particular, it may be useful for other projects to investigate the
data of the over 1,800 test cases related to Java bytecode. Test data
is stored in directory "log", organized in a structure that mirrors the
structure of the modules and classes.

--- Further documentation ---

Please see "doc" for detailed documentation. To view the full
documentation, you will need LyX (http://www.lyx.org/), LaTeX, xfig,
gnuplot, and some utilities to convert EPS to PDF. All of these
applications are readily available on modern systems.

--- Contact ---

For specific information, or help regarding one of the modules in JNuke,
please contact Cyrille Artho <c.artho@aist.go.jp>.

--- Authors ---

Cyrille Artho
Marcel Baur
Armin Biere
Pascal Eugster
Peter Farkas
Viktor Schuppan
Boris Zweimueller