Mercurial > hg > Members > kono > jpf-core
comparison doc/install/build.md @ 0:61d41facf527
initial v8 import (history reset)
author | Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> |
---|---|
date | Fri, 23 Jan 2015 10:14:01 -0800 |
parents | |
children |
comparison
equal
deleted
inserted
replaced
-1:000000000000 | 0:61d41facf527 |
---|---|
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. |