Trying to test JPF

[Sérgio Areias]

Hi.

I am new to java pathfinder. I have done everything as described on
the documentation and I was able to build it successful. Now I am
trying to run the examples included on the source package but I am
always receiving the same message.

"[SEVERE] not a valid class name: <NAME_OF_THE_FILE>"

What would be the options I need to add when running bin/jpf for the
files under the folder "examples"?

Thanks in advance,
Sérgio

[Peter Mehlitz]

try something like

cd <your-project-dir>/jpf-core
bin/jpf src/examples/Rand.jpf

from the command line

-- Peter

[Sérgio Areias]

Thanks for the answer.

Now I have a source folder with four class files named linquedqueue:

LinkedNode.java
LinkedQueue.java
LinkedQueueDriver.java
Process.java

To use bin/jpf I have to convert them to *.jpf first with bin/javajpf?
Because everytime I try to do it I receive the following error
message:

Exception in thread "main" java.lang.NoClassDefFoundError: /Users/
Juggernaut/Desktop/linkedqueue/LinkedQueue/java
Caused by:
java.lang.ClassNotFoundException: .Users.Juggernaut.Desktop.linkedqueue.LinkedQueue.java
at java.net.URLClassLoader$1.run(URLClassLoader.java:202)
at java.security.AccessController.doPrivileged(Native Method)
at java.net.URLClassLoader.findClass(URLClassLoader.java:190)
at java.lang.ClassLoader.loadClass(ClassLoader.java:307)
at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:301)
at java.lang.ClassLoader.loadClass(ClassLoader.java:248)


I have tried to use JPF with Eclipse as explained in the documentation
but I am receiving the same error everytime I try to run it. What am I
doing wrong here (I would prefer to use it on the console instead of
using it with Eclipse)?

Thanks in advance,
Sérgio

[Ivan Mushketik]

Hello.
To run your application under JPF you should "tell" to JPF where your
application classes and sources and what class to run.
To do it you can either write *.jpf config file or set this parameters
in command line.
Here is my config that I use to run test application in JPF:
# target.jpf
target=jpftest.Main
jpf-core.classpath+=;/home/proger/Documents/Programming/Java/JPF/JPFTest/build/classes

target - name of the class with main() method
jpf.core.classpath - variable with classpath that use system under test.

To run my app I just use:
bin/jpf target.jpf
(I keep this file in jpf-core directory).

Check out [1] for more info about JPF config.

[1] - http://babelfish.arc.nasa.gov/trac/jpf/wiki/user/config

[Peter Mehlitz]

there is no tool to create *.jpf application properties files, you have to do this by hand (javajpf is just a little utility script to run java on arbitrary main classes with a classpath that includes jpf-core).

The *.jpf files are simple (Java properties formatted) text files, and they only have to include one line

target = <your-main-class>

Please see http://babelfish.arc.nasa.gov/trac/jpf/wiki/user/config for details, or look at some of the examples in jpf-core/src/examples

-- Peter

[Sérgio Areias]

Thanks for the help. After a few hours trying it is working nice right
now.

Sérgio

On Apr 15, 5:28 pm, Peter Mehlitz <pcmehl...@gmail.com> wrote:
> there is no tool to create *.jpf application properties files, you have to do this by hand (javajpf is just a little utility script to run java on arbitrary main classes with a classpath that includes jpf-core).
>
> The *.jpf files are simple (Java properties formatted) text files, and they only have to include one line
>
>   target = <your-main-class>
>

> Please seehttp://babelfish.arc.nasa.gov/trac/jpf/wiki/user/configfor details, or look at some of the examples in jpf-core/src/examples

[Pieter]

I found this link to be very helpful during installation:

http://bluegulf.wordpress.com/2011/04/20/tutorial-using-java-pathfinder-together-with-junit-in-eclipse-environment-setup/

Regards
>o{=

[Sérgio Areias]

Hi.

Now I have another doubt. Any of the extensions for JPF does JML
verifications (I could not find anything about it)? If this is not the
case, any suggestion for what files should I begin to read from the
source code in order to get jpf-symbc and use it to verify JML
annotations?

For example, if I had the method "adds(int a, int b)" I would want to
receive the jpf-symbc output about argument 'a' and 'b', and check the
JML annotation to find possible errors. Is this possible to do with
jpf even if I have to do some changes or add some code?

Thanks in advance,
Sérgio

On May 17, 2:25 pm, Pieter <superhaas...@gmail.com> wrote:
> I found this link to be very helpful during installation:
>

> http://bluegulf.wordpress.com/2011/04/20/tutorial-using-java-pathfind...
>
> Regards
>
> >o{=