[JPF] JPF from terminal

[Dascalu Laurentiu]

Hello,

I want to use the JPF over my clasess in a shell script. I started
with this tutorial: http://javapathfinder.sourceforge.net/Running_JPF.html

I have the following configuration:
1. javapathfinder-trunk (cloned from mercurial repo)
2. my_project
src/my_classes

I want to test my classes:
../javapathfinder-trunk/bin/jpf \
+jpf.basedir=../SymbolicExecutor \

+vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory \
'+symbolic.method=myMethod1()' \
+search.multiple_errors=true \
+jpf.report.console.finished= \
Dummy

The error is:
[WARNING] orphant NativePeer method: java.lang.ClassLoader.init0()V
[...]
[WARNING] orphant NativePeer method:
java.lang.System.getKeyValuePairs()[Ljava/lang/String;
[SEVERE] error during VM runtime initialization: wrong model classes
(check vm.[boot]classpath)

If I run the application in Eclipse, everything is fine. Do I miss
something?

Thanks,


--
Subscription settings: http://groups.google.com/group/java-pathfinder/subscribe?hl=en

[Muhammad Yousaf]

I think it would be best for you if you refer to the new website

babelfish.arc.nasa.gov/trac/jpf

It has almost all the details how to install and run JPF. The information over there is somewhat scattered. Soon, I will be making a document soon that will list all the steps to install and run JPF on Eclipse. I sure will share that document over here.

[Flavio Lerda]

Hello Dascalu,

From the error you reported, it seems you are not adding
jpf-classes.jar to your invocation of JPF.
This jar file contains all the MJI implementation of native classes
and methods (like java.lang.ClassLoader.init0()V).

I would suggest running jpf using the .jpf file you use in Eclipse as
an argument or replication all the options in it and in the
jpf.properties file.

-Flavio

--
Flavio Lerda

[Laurențiu Dascălu]

> I would suggest running jpf using the .jpf file you use in Eclipse as
> an argument or replication all the options in it and in the
> jpf.properties file.

Ok, I copied jpf.properties into my the SUT directory.

Now I receive:
Exception in thread "main" java.lang.RuntimeException: ERROR: you need
to turn debug option on

I've found that in the code:
//if debug option was not used when compiling the class,
//then we do not have names of the locals

throw new RuntimeException("ERROR: you need to turn debug option on");

How should I compile my java classes to be JPF compliant? In order to
compile, I just included some jars into the classpath.

> On 23 April 2010 18:04, Muhammad Yousaf<muhammd...@gmail.com> wrote:
>> I think it would be best for you if you refer to the new website
>> babelfish.arc.nasa.gov/trac/jpf
>> It has almost all the details how to install and run JPF. The information
>> over there is somewhat scattered. Soon, I will be making a document soon
>> that will list all the steps to install and run JPF on Eclipse. I sure will
>> share that document over here.

I've had no problems running JPF on Eclipse.

--
Laurențiu Dascălu

[Laurențiu Dascălu]

Looks like the solution was simple; just compile with -g.

I use ant to compile the sources, so I added debug="on" to the javac tag.

--
Laurențiu Dascălu