Directory Structure

The JPF directory tree is divided into two categories: sources and binaries. Sources do not only contain the core JPF classes, but also standard library abstractions used by JPF, this HTML documentation, and a regression test suite. Binaries include the JPF class files, and (optionally) required 3rd party libraries and build-tools.

Figure 1: JPF directory structure

Sources are divided into two major categories: core (jpf/src/*) and extension (jpf/extensions/*). While extension classes can belong to packages that are in the core (i.e. add or even override classes in core packages), care has to be taken that no core class (i.e. classes under javapathfinder-trunk/src) depends on a particular extension - dependencies are only allowed from extension to core. Since exensions can even replace core classes, it is obvious that not all extensions have to be compatible with each other. While compatibility is preferable, it does not have to hold for all extensions. As a consequence, extensions have to be built separately, by providing and explicitly invoking their build.xml Ant scripts. This also takes care of extensions that make use of native libraries and/or other special resources. Please note that not all JPF distributions have to include all extensions, as those can also be proprietary or refer to non-public applications.

Potential dependency on extensions that are incompatible or require non-standard build procedures is also the reason why example subdirectories have to be built explicitly.

Each extension directory is modeled after the toplevel JPF structure, i.e. can have src, env, test, examples and doc subdirectories. To keep the classpath simple, we still compile all extension classes into the same build/... target directory.

Classes under .../env/* refer to MJI based library abstractions, further divided into model classes (env/jpf, to be executed by JPF) and NativePeer classes (env/jvm, to be executed by the host VM). Due to their different use (JPF and host VM), env/jpf and env/jvm classes are compiled into different directories/jar archives. Since libary abstractions should be configurable, core (.../src/*) classes should not depend on env/jvm/* classes, to avoid cyclic depencies between core and env (for everything but the most basic classes like java.lang.Thread etc,)

To enable builds of JPF outside an integrated development environment, the JPF distribution contains an optional directory tree that contains everything that is required to compile JPF sources from a command line. Using these tools, a build directory is created that holds the class files for the three major source directories.

The lib directory contents are required to run JPF, and need to be in the CLASSPATH if JPF is started directly, i.e. without the provided scripts.

To ease JPF execution, the bin directory contains scripts to automatically set the CLASSPATH. The script bin/jpf can be used to start JPF from the command line like a normal Java VM (i.e. is a java drop-in replacement).