Re: [Javapathfinder-user] Running JPF

[Martijn H. <M.H...@cs...>]

Hi Peter,

Thanks for your reply, it makes things more clear, and I can use jpf now!

Best wishes,

Martijn

Peter C. Mehlitz wrote:
> 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
> 
> 
> 
> -------------------------------------------------------
> SF.Net email is Sponsored by the Better Software Conference & EXPO
> September 19-22, 2005 * San Francisco, CA * Development Lifecycle Practices
> Agile & Plan-Driven Development * Managing Projects & Teams * Testing & QA
> Security * Process Improvement & Measurement * http://www.sqe.com/bsce5sf
> _______________________________________________
> Javapathfinder-user mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-user