+++ /dev/null
-# Building, Testing, and Running #
-
-If you downloaded binary snapshots, you don't have anything to build (except of creating/updating you [site.properties](./site-properties) file).
-
-## Building JPF ##
-
-If you have cloned the project repositories you are interested in (which at least includes [jpf-core](../jpf-core/index)), you can build and test each of them by means of their included [Ant](http://ant.apache.org) `build.xml` scripts. Note that you have to install Ant and JUnit separately, e.g. following directions [here](../install/requirements).
-
-
-### Using the command line ###
-
-~~~~~~~~ {.bash}
-> cd jpf-core
-> ant test
-
-... lots of output, at the end you should see something like:
-BUILD SUCCESSFUL
-Total time: 2 minutes 31 seconds
-~~~~~~~~
-
-### Within NetBeans ###
-
- 1. run **File/Open Project..** from the application menu, entering the JPF project you just downloaded (e.g. "jpf-core")
- 1. select the project that appears in our project pane (e.g. "jpf-core")
- 1. run **Build** from the project context menu
-
-### Within Eclipse ###
-
-* Ensure that the `JAVA_HOME` environment variable points to the jdk1.6xxx directory. If it is empty or points to a JRE then errors such as **javac not found** maybe seen. If you do not want the system Java settings to point to jdk1.6xxx, you can also set project specific settings in eclipse.
-
-* If you eclipse settings are set to **Build Automatically** then the project after being cloned will be built.
-
-* To build a particular project in the Project menu select **Build Project**. All the dependencies for the project will be built automatically.
-
-#### Project Specific JDK settings within Eclipse ####
-1. In Eclipse go to **Project** -> **Properties**
-
-2. Select **Builders**
-
-3. Pick **Ant_Builder** -> click **Edit**
-
-4. Click on the **JRE** tab
-
-5. Select **Separate JRE** -> **Installed JREs**
-
-6. On Windows and Unix-based systems pick JDK1.6xxx. If it is not listed under the installed JREs, click on **Add**, browse your file system to where JDK1.6xxx resides and select. On OSx systems pick the JVM 1.6.0.
-
-
-## Running JPF ##
-
-### Using the command line ###
-
-
-~~~~~~~~ {.bash}
-> cd jpf-core
-> java -jar build/RunJPF.jar src/examples/Racer.jpf
-JavaPathfinder v5.0 - (C) 1999-2007 RIACS/NASA Ames Research Center
-.....
-====================================================== statistics
-elapsed time: 0:00:00
-states: new=9, visited=1, backtracked=4, end=2
-search: maxDepth=5, constraints=0
-choice generators: thread=8, data=0
-heap: gc=8, new=291, free=32
-instructions: 3112
-max memory: 79MB
-loaded code: classes=73, methods=1010
-
-====================================================== search finished: 1/12/10 2:30 PM
-~~~~~~~~
-
-### Using eclipse plugin ###
-
- 1. Right click on a .jpf file. Examples can be found in the src\examples directory in jpf-core
- 1. If the eclipse plugin is correctly installed, a Verify option will appear.
- 1. Select the Verify option and the verification process of the system specified in the .jpf file begins
-
-Note that the Application.jpf file essentially replaces previous uses of eclipse launch configurations. The required element of a .jpf file is the `target=MAIN_CLASS` where `MAIN_CLASS` is the class containing main method of the system under test. Any other configurations that need to be specified can be added here. for example `listener=gov.nasa.jpf.tools.SearchMonitor`.
-
-Specify `classpath=PATH_TO_BIN_DIRECTORY` to add the class files for the program under test to JPF's class path. Windows users will need to use the double-backslash notation in specifying paths in the .jpf file. An example .jpf file for the Windows platform is included below for convenience:
-
-~~~~~~~~ {.bash}
-target=mutex.DekkerTestMain
-report.console.property_violation=error,trace,snapshot
-listener=gov.nasa.jpf.listener.EndlessLoopDetector
-classpath=C:\\Users\\fred\\Documents\\ch02-mutex\\bin
-sourcepath=C:\\Users\\fred\\Documents\\ch02-mutex\\src,C:\\Users\\Fred\\Documents\\ch02-mutex\\src-test
-~~~~~~~~
-
-The .jpf file not only indicates the `target` and `classpath`, but it also turns on error reporting with trace generation (`report.console.property_violation`) and configures the source path (`sourcepath`). Note that multiple source directories are specified using the comma separator.
-
-### Using eclipse Run Configuration ###
-
- 1. Select a .jpf file by clicking on it in the Package Explorer
- 1. Click **Run** -> **Run Configurations** -> **run-JPF-core**. It is important the correct .jpf file is selected when the configuration is run.
-
-#### Windows users ####
-After a fresh install of jpf-core you may see the following when trying to use the Eclipse Run-jpf-core configuration:
-
-~~~~~~~~
-java.lang.NoClassDefFoundError: gov/nasa/jpf/Main
-Caused by: java.lang.ClassNotFoundException: gov.nasa.jpf.Main
- at java.net.URLClassLoader$1.run(Unknown Source)
- at java.security.AccessController.doPrivileged(Native Method)
- at java.net.URLClassLoader.findClass(Unknown Source)
- at java.lang.ClassLoader.loadClass(Unknown Source)
- at sun.misc.Launcher$AppClassLoader.loadClass(Unknown Source)
- at java.lang.ClassLoader.loadClass(Unknown Source)
-Exception in thread "main"
-~~~~~~~~
-
-In this particular case, the error was generated after the initial build after the clone had completed. To resolve the issue, **refresh the Eclipse workspace** (F5 or right click Refresh). After the refresh, the Run-jpf-core configuration should work as described above.
projects / jpf-core.git / blobdiff