docs/install/build.md

   1 # Building, Testing, and Running #
   2
   3 If you downloaded binary snapshots, you don't have anything to build (except of creating/updating you [site.properties](./site-properties) file).
   4
   5 ## Building JPF ##
   6
   7 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).
   8
   9
  10 ### Using the command line ###
  11
  12 ~~~~~~~~ {.bash}
  13 > cd jpf-core
  14 > ant test
  15
  16 ... lots of output, at the end you should see something like:
  17 BUILD SUCCESSFUL
  18 Total time: 2 minutes 31 seconds
  19 ~~~~~~~~
  20
  21 ### Within NetBeans ###
  22
  23  1. run **File/Open Project..** from the application menu, entering the JPF project you just downloaded (e.g. "jpf-core")
  24  1. select the project that appears in our project pane (e.g. "jpf-core")
  25  1. run **Build** from the project context menu
  26
  27 ### Within Eclipse ###
  28
  29 * 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.
  30
  31 * If you eclipse settings are set to **Build Automatically** then the project after being cloned will be built.
  32
  33 * To build a particular project in the Project menu select **Build Project**. All the dependencies for the project will be built automatically.
  34
  35 #### Project Specific JDK settings within Eclipse ####
  36 1. In Eclipse go to **Project** -> **Properties**
  37
  38 2. Select **Builders**
  39
  40 3. Pick **Ant_Builder** -> click **Edit**
  41
  42 4. Click on the **JRE** tab
  43
  44 5. Select **Separate JRE** -> **Installed JREs**
  45
  46 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.
  47
  48
  49 ## Running JPF ##
  50
  51 ### Using the command line ###
  52
  53
  54 ~~~~~~~~ {.bash}
  55 > cd jpf-core
  56 > java -jar build/RunJPF.jar src/examples/Racer.jpf
  57 JavaPathfinder v5.0 - (C) 1999-2007 RIACS/NASA Ames Research Center
  58 .....
  59 ====================================================== statistics
  60 elapsed time:       0:00:00
  61 states:             new=9, visited=1, backtracked=4, end=2
  62 search:             maxDepth=5, constraints=0
  63 choice generators:  thread=8, data=0
  64 heap:               gc=8, new=291, free=32
  65 instructions:       3112
  66 max memory:         79MB
  67 loaded code:        classes=73, methods=1010
  68
  69 ====================================================== search finished: 1/12/10 2:30 PM
  70 ~~~~~~~~
  71
  72 ### Using eclipse plugin ###
  73
  74  1. Right click on a .jpf file. Examples can be found in the src\examples directory in jpf-core
  75  1. If the eclipse plugin is correctly installed, a Verify option will appear.
  76  1. Select the Verify option and the verification process of the system specified in the .jpf file begins
  77
  78 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`.
  79
  80 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:
  81
  82 ~~~~~~~~ {.bash}
  83 target=mutex.DekkerTestMain
  84 report.console.property_violation=error,trace,snapshot
  85 listener=gov.nasa.jpf.listener.EndlessLoopDetector
  86 classpath=C:\\Users\\fred\\Documents\\ch02-mutex\\bin
  87 sourcepath=C:\\Users\\fred\\Documents\\ch02-mutex\\src,C:\\Users\\Fred\\Documents\\ch02-mutex\\src-test
  88 ~~~~~~~~
  89
  90 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.
  91
  92 ### Using eclipse Run Configuration ###
  93
  94  1. Select a .jpf file by clicking on it in the Package Explorer
  95  1. Click **Run** -> **Run Configurations** -> **run-JPF-core**. It is important the correct .jpf file is selected when the configuration is run.
  96
  97 #### Windows users ####
  98 After a fresh install of jpf-core you may see the following when trying to use the Eclipse Run-jpf-core configuration:
  99
 100 ~~~~~~~~
 101 java.lang.NoClassDefFoundError: gov/nasa/jpf/Main
 102 Caused by: java.lang.ClassNotFoundException: gov.nasa.jpf.Main
 103     at java.net.URLClassLoader$1.run(Unknown Source)
 104     at java.security.AccessController.doPrivileged(Native Method)
 105     at java.net.URLClassLoader.findClass(Unknown Source)
 106     at java.lang.ClassLoader.loadClass(Unknown Source)
 107     at sun.misc.Launcher$AppClassLoader.loadClass(Unknown Source)
 108     at java.lang.ClassLoader.loadClass(Unknown Source)
 109 Exception in thread "main"
 110 ~~~~~~~~
 111
 112 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.