Re: [Javapathfinder-user] Running JPF

[Peter C. M. <pcm...@em...>]

You have to start jpf like a normal VM, i.e. you give it a class  
name, NOT the classfile. That means, this class has to be either in  
the classpath, or in the path that's used only by JPF to load classes  
(+vm.classpath), i.e. which are not seen by the host VM.

In you first example, the problem is simply that you have to specify  
the classname (the ./examples dir is already set in the classpath by  
the bin/jpf script):

   > bin/jpf HelloWorld

In your second example, the problem is that jpf - before it would not  
have found HelloWorld - doesn't find it's native peer model classes  
anymore (the MJI stuff in build/env/jpf), like java.lang.Thread and  
others. Please read the MJI docu section for that - model classes  
have to be ONLY in the vm.classpath (the host VM shouldn't see them  
because it needs the real java.lang.Thread etc.), the native peers  
have to be in the CLASSPATH (to make sure the host VM finds them). A  
bit confusing, but think of jpf as a JVM that is running on top of a  
JVM.

-- Peter 

On Aug 5, 2005, at 2:49 AM, Martijn Hendriks wrote:

> Hi,
>
> I am new to JPF and I am trying to modelcheck the HelloWorld app in  
> the example directory. I just cannot get it to work:
>
> javapathfinder > bin/jpf examples/HelloWorld.class
> Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA  
> Ames Research Center
> JPF exception, terminating: could not load class  
> examples.HelloWorld.class
>
> examples > ../bin/jpf HelloWorld.class
> Java Pathfinder Model Checker v3.1.2 - (C) 1999-2004 RIACS/NASA  
> Ames Research Center
> error during VM runtime initialization: wrong model classes (check  
> vm.[boot]classpath)
>
> and i tried a lot more... I probably need to set some paths, but I  
> can't figure what to do exactly.
>
> The "ant run-tests" works fine: no errors are reported (I am using  
> j2sdk1.4.2_08 on Linux).
>
> It would be great if someone could help me with this.
>
> Thanks!
>
> Martijn Hendriks