JPF 安装提示

1、JPF 安装提示1. 是关于JPF的官方网站，里面由关于JPF的相关资料。2. 下载JPF需要到Sourceforge网站上，网址为：3. 下载javapathfinder-src-libs-1.0-7-oct-05.zip文件到本地解压缩。4. 将解压缩的项目Import到eclipse workspace。5. 更改Project Properties    a. Java Build Path -> Source -> Add Folder (env/jpf 和env/jvm和examples加进来)   

2、 a. Java Build Path -> Lib -> Add JARs (将位于build-tools/lib & lib 下的所有jar包添加进来)    c. Java Compiler -> Compiler Compliance level & Generated Class. file compatibility & source file compatibility 全设为1.4（这样就允许target code中包含assert之类的信息了）6. 进入ANT View启动A

3、NT命令：compile（default）ANT脚本需要适当修改才能保证编译后的项目可以运行，修改后的脚本粘贴在下面了，覆盖原有脚本即可    项目上右键菜单Run-> Add Arguments （添加你想检查的目标代码，如 deadlock.Deadlock）     点击Wizard中的Run按钮8. 观察Console，会出现运行结果！如有不明白之处，可以发邮件向我咨询：lianggt08sei (梁广泰)附：build.xml<?xml version="1.0&

4、quot; ?><!- build.xml - the global JPF build system configuration targets: clean remove the files that have been generated by the build process compile compile JPF and its specific (modeled) environment libraries compile-env-jpf compile exclusive JPF classes for (modeled) environment compile-e

5、nv-jvm compile native method peer classes for (modeled) environment compile-examples compile all the examples compile-jpf compile all JPF classes compile-tests compile all the tests for JPF dist generate the compressed distribution tar files dist-src generate the compressed source distribution tar f

6、iles docs-javadoc create javadoc documentation init common task/target initialization jar create jar archives for JPF, its JVM and their environment models run-tests run all JPF tests-><project name="nasa-jpf" default="compile" basedir="."> <!- = COMMON SECT

7、ION = -> <!- this is where platform specific settings come in (note this has to be read first in case you want to override props) -> <property file="perties"/> <property file="$perties"/> <!- this is where we get static things like the ve

8、rsion from (but make sure they don't collide) -> <property file="perties"/> <!- our required global properties -> <property name="" value="open-jpf" /> <!- Project directories -> <property name="bin.dir" val

9、ue="bin" /> <property name="build.dir" value="build" /> <property name= value="$build.dir/dist" /> <property name= value="$build.dir" /> <property name= value= /> <property name= value= /> <property name= value=&qu

10、ot;$build.dir/jpf" /> <property name= value="$build.dir/jpf" /> <property name= value="$build.dir/lib" /> <property name= value="$build.dir/test" /> <property name="build-tools.dir" value="build-tools" /> <property

11、name= value="$build-tools.dir/bin" /> <property name= value="$build-tools.dir/lib" /> <property name="doc.dir" value="doc"/> <property name= value="$doc.dir/api"/> <property name= value="$doc.dir/images"/> <pro

12、perty name="env.dir" value="env"/> <property name= value="$env.dir/jpf"/> <property name= value="$env.dir/jvm"/> <property name="examples.dir" value="examples" /> <property name="lib.dir" value="lib&qu

13、ot; /> <property name="src.dir" value="src" /> <property name="test.dir" value="test" /> <property name="ext.dir" value="extensions" /> <property name="packages" value=/> <property name="debug&qu

14、ot; value="on"/> <property name="deprecation" value="on"/> <property name="jar" value="jar" /> <!- just more or less educated fallback guesses, use perties -> <property name="junit.jar" value=/> <!- ge

15、neric classpath settings (collecting all libs under extensions) -> <path id="lib.path"> <fileset dir="."> <include name="$lib.dir/*.jar"/> </fileset> <fileset dir="."> <include name="$lib.dir/*.zip"/> </files

16、et> <fileset dir="$ext.dir"> <include name="*/$lib.dir/*.jar"/> </fileset> </path> <!- we need to do this trick to avoid Ant recompiling all our sources (it needs to get exact srddirs) -> <path id="esd"> <pathelement location=&q

17、uot;$src.dir"/> <dirset dir="$ext.dir"> <include name="*/src"/> </dirset> </path> <property name= refid="esd"/> <!-* * init: common tasks, mainly to setup directories and check what other * tasks can be executed *-> <target

18、 name="init" description="common task/target initialization"> <tstamp/> <echo>* JPF build system *current dir: $user.diruser home dir: $user.home java version: $java.versionOS: $-$os.arch-$os.version </echo> <echo>NOTE - if property values are pr

19、inted with brackets (e.g. '$bla'), it means they are NOT defined. This is a 'echo' task itch. </echo> <available file="perties" property=/> <echo message= /> <echo message="NOTE - some targets might be skipped if you don't have a '

20、perties' file" /> <echo/> <echo message="- creating build directories."/> <mkdir dir="$build.dir"/> <mkdir dir=/> <mkdir dir=/> <mkdir dir=/> <mkdir dir=/> <mkdir dir=/> <echo/> <echo message="- ch

21、ecking for external libraries."/> <condition property=> <!- we currently don't use other test tools than junit -> <available classname=/> </condition> <available classname= property=/> <echo message=/> </target> <!-* * compile-jpf: compile JPF

22、 core classes *-> <target name="compile-jpf" depends="init" description="compile JPF core classes"> <javac srcdir="$src.dir" destdir= debug="$debug" source="1.4" listfiles="Yes" deprecation="$deprecation">

23、 <classpath> <path refid="lib.path"/> </classpath> </javac> <copy file="perties" todir=/> </target> <!-* * compile-ext: compile JPF extension classes *-> <target name="compile-ext" depends="compile-jpf" d

24、escription="compile optional extension classes"> <javac srcdir= destdir= debug="$debug" source="1.4" listfiles="Yes" deprecation="$deprecation"> <classpath> <path refid="lib.path"/> </classpath> </javac> <

25、;/target> <!-* * compile: compile MJI native peer class environment *-> <target name="compile-env-jvm" depends="compile-jpf" description="compile MJI native peer classes"> <javac srcdir= destdir= debug="$debug" source="1.4" deprecat

26、ion="$deprecation"> <classpath> <path refid="lib.path"/> <pathelement path=/> </classpath> </javac> </target> <!-* * compile: compile standard MJI model classes *-> <target name="compile-env-jpf" depends="compile-jpf&

27、quot; description="compile MJI model classes"> <javac srcdir= destdir= debug="$debug" source="1.4" deprecation="$deprecation"> <classpath> <path refid="lib.path"/> <pathelement path=/> <pathelement path=/> </classp

28、ath> </javac> </target> <!-* * compile: compile JPF and its modeled environment libraries *-> <target name="compile" depends="compile-jpf, compile-ext, compile-env-jvm, compile-env-jpf" description="compile JPF and its specific (modeled) environment l

29、ibraries"> </target> <!-= EXAMPLES SECTION =-> <!-* * compile-examples: optional Compile the examples *-> <target name="compile-examples" depends="compile" description="compile examples"> <!- Create the build/examples directory -> &

30、lt;mkdir dir=/> <javac srcdir="$examples.dir" destdir= debug="$debug" source="1.4" deprecation="$deprecation"> <classpath> <path refid="lib.path"/> <pathelement path=/> <pathelement path=/> <pathelement path=/>

31、</classpath> </javac> <!- Copy *.ltl, *.properties to the build/examples directory. -> <copy todir=> <fileset dir="$examples.dir" includes="*/*.ltl, */*.properties"/> </copy> </target> <!-= TEST SECTION =-> <!-* * compile-tests:

32、optional compile all the tests for JPF *-> <target name="compile-tests" depends="compile" description="compile all the tests for JPF"> <javac srcdir="$test.dir" destdir= debug="$debug" source="1.4" deprecation="$deprecation

33、"> <classpath> <path refid="lib.path"/> <pathelement location="$junit.jar"/> <pathelement path=/> <pathelement path=/> <pathelement path=/> </classpath> </javac> <!- Copy *.ltl, *.properties to the build/test directory. -

34、> <copy todir=> <fileset dir="$test.dir" includes="*/*.ltl, */*.properties"/> </copy> </target> <!-* * run-tests: optional run all JPF tests *-> <target name="run-tests" depends="compile-tests" if= description="run all

35、JPF tests"> <echo message= /> <junit printsummary="on" showoutput="off"> <formatter type="plain"/> <classpath id="test.path"> <!- we need to add the system classpath if we run junit forked (otherwise it won't find the ant

36、 stuff itself) -> <pathelement path=/> <path refid="lib.path"/> <pathelement location="$junit.jar"/> <pathelement path=/> <pathelement path=/> <pathelement path=/> <pathelement path=/> </classpath> <batchtest fork="yes&qu

37、ot; todir=> <fileset dir=> <!- until we have the Ant AbstractFileSet patch (#12060), we have to explicitly name the tests -> <include name="*/jvm/TestJavaLangClassJPF.class"/> <include name="*/jvm/TestAssertJPF.class"/> <include name="*/jvm/Test

38、ExceptionJPF.class"/> <include name="*/jvm/TestArrayJPF.class"/> <include name="*/jvm/TestNativePeerJPF.class"/> <include name="*/jvm/TestCastJPF.class"/> <include name="*/jvm/TestFieldJPF.class"/> <include name="*/jvm/T

39、estMethodJPF.class"/> <include name="*/jvm/TestThreadJPF.class"/> <include name="*/jvm/TestWaitJPF.class"/> <include name="*/mc/TestVMDeadlockJPF.class"/> <include name="*/mc/TestRandomJPF.class"/> <include name="*/mc/Te

40、stCrossingJPF.class"/> <include name="*/mc/TestOldClassicJPF.class"/> </fileset> </batchtest> </junit> </target> <!-= DOCUMENTATION AND FORMAT SECTION =-> <!-* * docs-javadoc: create API documentation with javadoc *-> <target name="

41、docs-javadoc" depends="init" description="create javadoc documentation"> <mkdir dir=/> <echo message="- running javadoc to create documentation."/> <javadoc packagenames="$packages" sourcepath="$src.dir" destdir= author="t

42、rue" version="true" use="true" source="1.4" windowtitle="$ API" doctitle="$"> <classpath> <path refid="lib.path"/> </classpath> </javadoc> </target> <!-= DISTRIBUTION AND ARCHIVING SE

43、CTION =-> <!-* * jar: build jars with all JPF binaries *-> <target name="jar" depends="compile" description="create jar archives for JPF, its JVM and their environment models"> <mkdir dir=/> <copy todir=> <fileset dir="$user.dir"&

44、gt; <include name="perties"/> <include name="perties"/> </fileset> </copy> <jar jarfile= basedir=/> <jar jarfile= basedir= /> <jar jarfile= basedir= /> </target> <!-* * dist: create a binary distribution *->

45、<target name="dist" description="generate the compressed distribution tar files"> <!- Create the distribution directory -> <mkdir dir=/> <!- Create the compressed distribution file in the distribution directory -> <tar destfile= compression="gzip"> <tarfileset dir="$src.dir" prefix="$-$jpf.version/$src.dir" /> <tarfileset dir="$test.dir" prefix="$-$jpf.version/$test.dir" /> <t