Mercurial > hg > Members > kono > jpf-core

annotate doc/user/run.md @ 0:61d41facf527

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial v8 import (history reset)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 23 Jan 2015 10:14:01 -0800
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
1 # Running JPF #
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
2 There are five general ways to run JPF, depending on your execution environment (command prompt or IDE) and desired level of configuration support. This page has to cover quite some ground, so bear with us
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
3
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
4 1. [from a command prompt (operating system shell)](#command-line)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
5 2. [from an IDE (NetBeans, Eclipse) without using JPF plugins](#running-jpf-from-within-ide-without-plugins)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
6 3. [from an IDE with JPF plugins installed](#running-jpf-from-within-ide-with-plugins)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
7 4. [from within a JUnit test class](#launching-jpf-from-junit-tests)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
8 5. [single tests from command line](#explicitly-running-tests-from-the-command-line)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
9 6. [explicitly from an arbitrary Java program](#explicitly-launching-jpf-from-a-java-program)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
10
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
11 ## Command Line ##
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
12
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
13 There are several ways to run JPF from the command line, using varying degrees of its runtime infrastructure. The most simple way is to use the provided `bin/jpf` script of the jpf-core distribution. Go to the directory where your system under test (SUT) classes reside, and do a
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
14
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
15 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
16 > <jpf-core-dir>/bin/jpf +classpath=. <application-main-class>
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
17 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
18
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
19 or preferably
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
20
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
21 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
22 > <jpf-core-dir>/bin/jpf <application-property-file>.jpf
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
23 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
24
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
25 (see target specification below). If you want to avoid platform specific scripts, you only have to slightly expand this to
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
26
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
27 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
28 > java -jar <jpf-core-dir>/build/RunJPF.jar +classpath=. <application-main-class>
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
29 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
30
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
31 This makes use of the small RunJPF.jar startup jar that is part of the jpf-core distribution, which only includes the classes that are required to start the JPF bootstrapping process (esp. the JPF classloader). These classes automatically process the various [JPF configuration files](config). If your SUT is not trivial, it is also recommended to add a "-Xmx1024m" host VM option, to avoid running out of memory.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
32
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
33 Last (and probably most rarely), you can directly start JPF and give it an explicit classpath. This amounts to something like
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
34
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
35 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
36 > java -classpath <jpf-core-dir>/build/jpf.jar gov.nasa.jpf.JPF +classpath=. <application-main-class>
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
37 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
38
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
39 Of course, this gets quickly more complicated if you use JPF extensions, which require to add to both the host VM and the JPF classpath, which is completely automated if you use the RunJPF.jar method. Explicitly setting paths is only for rare occasions if you develop JPF components yourself.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
40
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
41 There are three different argument groups that are processed by JPF:
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
42
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
43 #### (1) JPF command line options ####
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
44
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
45 These options should come first (after RunJPF.jar), and all start with a hyphen ("-"). The set of currently supported options is:
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
46
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
47 * -help : show usage information and exit
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
48 * -log : print the configuration steps
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
49 * -show : print the configuration dictionary after configuration is complete
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
50
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
51 The last two options are mostly used to debug if the JPF configuration does not work as expected. Usually you start with `-show`, and if you don't see the values you expect, continue with `-log` to find out how the values got set.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
52
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
53
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
54 #### (2) JPF properties ####
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
55
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
56 This is the second group of options, which all start with a plus ("+") marker, and consist of "`+<key>=<value>`" pairs like
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
57
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
58 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
59 .. +cg.enumerate_random=true
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
60 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
61
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
62 All properties from the various JPF properties [configuration files](config) can be overridden from the command-line, which means there is no limit regarding number and values of options. If you want to extend an existing value, you can use any of the following notations
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
63
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
64 * `+<key>+=<value>` - which appends <value>
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
65 * `++<key>=<value>` - which prepends <value>
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
66 * `+<key>=..${<key>}..` - which gives explicit control over extension positions
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
67
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
68 Normal JPF properties `${<key>}` expansion is supported.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
69
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
70 If the `=<value>` part is omitted, a default value of `true` is assumed. If you want to set a value to null (i.e. remove a key), just skip the `<value>` part, as in `+<key>=`
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
71
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
72 #### (3) target specification ####
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
73
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
74 There are two ways to specify what application JPF should analyze
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
75
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
76 * explicit classname and arguments
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
77
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
78 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
79 > jpf ... x.y.MyApplication arg1 arg2 ..
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
80 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
81
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
82 * application property file (*.jpf)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
83
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
84 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
85 > jpf ... MyApplication.jpf
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
86 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
87
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
88 We recommend using the second way, since it enables you to store all required settings in a text file that can be kept together with the SUT sources, and also allows you to start JPF from within !NetBeans or Eclipse just by selecting the *.jpf file (this is mainly what the IDE plugins are for). Please note that application property files require a "`target`" entry, as in
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
89
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
90 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
91 # JPF application property file to verify x.y.MyApplication
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
92 target = x.y.MyApplication
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
93 target.args = arg1,arg2
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
94 # Note that target_args in JPF 6 changed to target.args in JPF 7.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
95 ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
96 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
97
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
98 ## Running JPF from within IDE without plugins ##
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
99
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
100 You can start JPF from within !NetBeans or Eclipse without having the IDE specific JPF plugins installed. In this case, JPF uses the standard IDE consoles to report verification results. For details, please refer to the following pages:
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
101
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
102 * [Running JPF from within NetBeans without plugin](run_nb)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
103 * [Running JPF from Eclipse without plugin](run_eclipse)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
104
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
105 Note that this is **not** the recommended way to run JPF from within an IDE, unless you want to debug JPF or your classes.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
106
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
107 ## Running JPF from within IDE with plugins ##
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
108
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
109 You can simplify launching JPF from within !NetBeans or Eclipse by using the respective plugins that are available from this server. In this case, you just have to create/select an application property (*.jpf) file within your test project, and use the IDE context menu to start a graphical JPF user interface. These so called "JPF shells" are separate applications (that can be configured through normal JPF properties), i.e. appear in a separate window, but can still communicate with the IDE, e.g. to position editor windows. You can find more details on
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
110
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
111 * [Running JPF from within NetBeans with netbeans-jpf plugin](run_nb_plugin)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
112 * [Running JPF from Eclipse with eclipse-jpf plugin](run_eclipse_plugin)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
113
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
114 This is becoming the primary method of running JPF. The benefits are twofold: (1) this is executed outside of the IDE process, i.e. it doesn't crash the IDE if JPF runs out of memory, and (2) it makes use of all your standard JPF configuration (site.properties and jpf.properties), in the same way like running JPF from a command-line.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
115
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
116 ## Launching JPF from JUnit tests ##
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
117
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
118 JPF comes with [JUnit](http://www.junit.org) based testing infrastructure that is used for its own regression test suite. This mechanism can also be used to create your own test drivers that are executed by JUnit, e.g. through an [Ant](http://ant.apache.org) build script. The source structure of your tests is quite simple
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
119
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
120 ~~~~~~~~ {.java}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
121 import gov.nasa.jpf.util.test.JPFTestSuite;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
122 import org.junit.Test;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
123
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
124 public class MyTest extends TestJPF {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
125
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
126 @Test
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
127 public void testSomeFunction() {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
128 if (verifyNoPropertyViolation(jpfOptions)) { // specifies the test goal, "jpfOptions" are optional
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
129 someFuntction(); .. // this section is verified by JPF
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
130 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
131 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
132
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
133 //.. more @Test methods
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
134 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
135
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
136 From a JUnit perspective, this is a completely normal test class. You can therefore execute such a test with the standard `<junit>` [Ant](http://ant.apache.org) task, like
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
137
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
138 ~~~~~~~~ {.xml}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
139 <property file="${user.home}/.jpf/site.properties"/>
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
140 <property file="${jpf-core}/jpf.properties"/>
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
141 ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
142 <junit printsummary="on" showoutput="off" haltonfailure="yes"
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
143 fork="yes" forkmode="perTest" maxmemory="1024m">
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
144 ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
145 <classpath>
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
146 ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
147 <pathelement location="${jpf-core}/build/jpf.jar"/>
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
148 </classpath>
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
149
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
150 <batchtest todir="build/tests">
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
151 <fileset dir="build/tests">
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
152 ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
153 <include name="**/*Test.class"/>
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
154 </fileset>
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
155 </batchtest>
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
156 </junit>
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
157 ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
158 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
159
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
160 Only jpf.jar needs to be in the host VM classpath when compiling and running the test, since `gov.nasa.jpf.util.test.TestJPF` will use the normal JPF configuration (site.properties and configured jpf.properties) to set up the required `native_classpath`, `classpath`, 'test_classpath` and `sourcepath` settings at runtime. Please refer to the [JPF configuration](config) page for details.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
161
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
162 If you don't have control over the build.xml because of the IDE specific project type (e.g. if your SUT is configured as a NetBeans "Class Library Project"), you have to add jpf.jar as an external jar to your IDE project configuration.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
163
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
164 In addition to adding jpf.jar to your build.xml or your IDE project configuration, you might want to add a jpf.properties file to the root directory of your project, to set up things like where JPF finds classes and sources it should analyze (i.e. settings that should be common for all your tests). A generic example could be
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
165
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
166 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
167 # example of JPF project properties file to set project specific paths
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
168
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
169 # no native classpath required if this is not a JPF project itself
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
170 myproject.native_classpath=...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
171
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
172 # where does JPF find the classfiles to execute
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
173 myproject.classpath=build/classes
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
174
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
175 # where do test classes reside
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
176 myproject.test_classpath=build/test/classes
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
177
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
178 # other project common JPF settings like autoloaders etc.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
179 listener.autoload+=,javax.annotation.Nonnull
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
180 listener.javax.annotation.Nonnull=.aprop.listener.NonnullChecker
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
181 ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
182 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
183
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
184 You can find project examples here
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
185
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
186 * [standard NetBeans project](../projects/standardnbproject) ("Java Class Library" or "Java Application")
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
187 * Freeform NetBeans project (with user supplied build.xml)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
188 * standard Eclipse project (with user supplied build.xml)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
189
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
190 Please refer to the [Verify API](api) and the [JPF tests](../devel/jpf_tests) pages for details about JPF APIs (like `verifyNoPropertyViolation(..)` or `Verify.getInt(min,max)`) you can use within your test classes.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
191
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
192 Since JPF projects use the same infrastructure for their regression tests, you can find a wealth of examples under the `src/tests` directories of your installed JPF projects.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
193
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
194 ## Explicitly Running Tests from the command line ##
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
195
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
196 You can also run your `TestJPF` derived test drivers by using the `bin/test` script (which in turn just a short for "`java -jar tools/RunTest.jar`", i.e. is platform independent):
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
197
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
198 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
199 bin/test <test-class> [<test-method>]
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
200 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
201
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
202 Note that each `verify..(jpfArgs)` uses its own `Config` instance in this case. If you want to specify temporary JPF options from the command-line when running `RunTest`, prefix them with `test` like in the following example
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
203
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
204 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
205 bin/test +test.listener=.listener.ExecTracker gov.nasa.jpf.test.mc.basic.AttrsTest
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
206 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
207
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
208 ## Explicitly Launching JPF from a Java Program ##
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
209 Since JPF is a pure Java application, you can also run it from your own application. The corresponding pattern looks like this:
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
210
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
211 ~~~~~~~~ {.java}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
212 public class MyJPFLauncher {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
213 ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
214 public static void main(String[] args){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
215 ..
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
216 try {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
217
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
218 // this initializes the JPF configuration from default.properties, site.properties
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
219 // configured extensions (jpf.properties), current directory (jpf.properies) and
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
220 // command line args ("+<key>=<value>" options and *.jpf)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
221 Config conf = JPF.createConfig(args);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
222
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
223 // ... modify config according to your needs
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
224 conf.setProperty("my.property", "whatever");
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
225
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
226 // ... explicitly create listeners (could be reused over multiple JPF runs)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
227 MyListener myListener = ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
228
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
229 JPF jpf = new JPF(conf);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
230
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
231 // ... set your listeners
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
232 jpf.addListener(myListener);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
233
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
234 jpf.run();
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
235 if (jpf.foundErrors()){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
236 // ... process property violations discovered by JPF
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
237 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
238 } catch (JPFConfigException cx){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
239 // ... handle configuration exception
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
240 // ... can happen before running JPF and indicates inconsistent configuration data
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
241 } catch (JPFException jx){
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
242 // ... handle exception while executing JPF, can be further differentiated into
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
243 // ... JPFListenerException - occurred from within configured listener
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
244 // ... JPFNativePeerException - occurred from within MJI method/native peer
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
245 // ... all others indicate JPF internal errors
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
246 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
247 ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
248 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
249
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
250 Please refer to the [Embedding JPF](../devel/embedded) developers documentation for details. If you start JPF through your own launcher application, you have to take care of setting up the required `CLASSPATH` entries so that it finds your (and JPFs) classes, or you can use the generic `gov.nasa.jpf.Main` to load and start your launcher class, which makes use of all the path settings you have in your [site.properties](../install/site-properties) and the directories holding project properties (jpf.properties) referenced therein (details on [how to configure JPF](../user/config). This brings us back to the command line at the top of this page, only that you specify which class should be loaded through `Main`:
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
251
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
252 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
253 > java -jar .../RunJPF.jar -a MyJPFLauncher ...
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
254 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
255
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
256 (note that `gov.nasa.jpf.Main` is the `Main-Class` entry of the executable RunJPF.jar, which also holds the `JPFClassLoader`).
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
257
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
258 Just for the sake of completeness, there is another way to start JPF explicitly through a `gov.nasa.jpf.JPFShell` implementation, which is using the normal `JPF.main()` to load your shell, which in turn instantiates and runs a `JPF` object. This is specified in your application property (*.jpf) file with the `shell=<your-shell-class>` option. Use this if your way to start JPF is optional, i.e. JPF could also be run normally with your *.jpf.