NoClassDefFoundError

[Shane Xu]

HI All:
  I am currently learning how to utilize JPF to analyze java programs, especially Symbolic Path Finder module. I have finished environment set up, and I am able to run provided symbolic .jpf tests. However, I get "NoClassDefFoundError" when I try to analyze a lejos EV3 program, which utilizes some lejos EV3 libraries.

The error message says that "lejos.hardware.sensor" is not found. And I try to include lejos EV3 libraries on jpf-symbc/jp.properties within jpf-symbc.native_classpath, and it turns out that this doesn't work at all. I guess I need to module function calls used from lejos EV3 libraries. Is this right? If this is the case, how can I start to module these function calls? Thanks.

[Petr Hudeček]

Hello.

I'm not familiar with leJOS specifically, but in general, if the code you're trying to analyze using Java Pathfinder is using a library, the library must be in the classpath of the system under test, not the native classpath. The native classpath contains classes that contain the code of JPF and jpf-symbc and potentially other extensions. The system that's being tested (your leJOS program, in this case) uses a different classpath.

To add to this classpath, try to use the properties "jpf-symbc.classpath" or "jpf-core.classpath", without the "native_" prefix. You may just add "jpf-core.classpath+=./lejos.jar", for example, to your project's .jpf file.

The libraries you link to in this classpath will be run by JPF much like your program. Their dependencies, if any, must also be in the simple classpath.

Best regards,
Petr

--

---
You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfinder+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Shane Xu]

HI Ptr:
  Thanks for replying. However, this issue still occurs after I apply changes you proposed.

1. Add included jar file to my applications' .jpf file as jpf-symbc.classpath.

 2. Add included jar file to my applications' .jpf file as jpf-core.classpath.

However, in both cases, the same error message arises:

I guess this error happens because JPF can't locate class definition when it reads the first line of code from my lejos program:
   
3. I also try to modify my application's .jpf file as following (${jpf-symbc}/build/examples contains compiled application classes):

This time, a different error arises:


I do know this must be a issue related to classpath set up. Since I am new to JPF, I am confused about how to get it work. Please provide any suggestion. Thx.

Chengcheng

To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.

[Petr Hudeček]

Hello,

I agree that the error probably means that JPF's class loader cannot find the sensor class in its classpath. There are a few ways to debug that - there is a commandline option that prints classpath in RunJPF, I believe. You can try that and see if the classpath is indeed being correctly loaded. You can also try posting your project here, I could try to to get it to run at my computer.

However, your screenshot is from an older version of JPF. The classes and packages mentioned in your error trace are from JPF 6, which is several years old and, among other things, is not super compatible with Java 8, I believe, and at any rate is not supported. 

I don't think upgrading to the current version of JPF will solve your problem but if it's an option for you, it's probably a good idea to upgrade.

Best regards,

Petr

To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfinder+unsubscribe@googlegroups.com.

[Quoc-Sang Phan]

JPF/SPF can only handle Java bytecode.

In order to manipulate hardware  (which is in your case) the library invokes some native methods, i.e. dynamically loaded library written in, e.g. C/C++, which JPF can't handle.

Try running with jpf-nhandler to see if the problem persists.

--Sang

[Shane Xu]

HI Petr:
  Within the attachment I upload, you can find a simple lejos program under /src, and you can use the build.xml to build the program and run. In this case, an error still arises if you run the program using ant (without plugin any EV3 device for testing):
 
At the end of this error message, you can find that the error happens because an EV3 brick doesn't exist which is the actual case when I try to run the lejos program without plugin any EV3 device. But, the included .jar file is correctly located, since I put location of included .jar file(ev3classes.jar) within build.xml, and the error is not caused by missing included .jar file. I understand that I couldn't test lejos program using JPF-core & JPF-symbc directly, but I really want to know how to make JPF correctly locate included .jar file utilized by lejos program. Could you try this on your computer? If JPF gives error message like "No brick found", instead of "Class not defined", this probably mean that the .jar file used by lejos program is located correctly. Thanks.

[Petr Hudeček]

 Could you please attach also the Lejos jar file?

To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfinder+unsubscribe@googlegroups.com.

[Shane Xu]

HI Petr:
  I have some trouble of attaching the .jar file here. Please download lejos package(leJOS_EV3_0.9.0-beta.tar.gz) from following link:
  https://sourceforge.net/projects/ev3.lejos.p/files/0.9.0-beta/
  After unzipping the file, you will find the .jar ev3classes.jar under /lib/ev3.
  Than you.

Best regards,
Chengcheng

[Qian Feng]

Hi Petr:

     My friend has the trouble to upload file. Here is the .jar file you may need 

https://drive.google.com/file/d/0BwdxGXEQpH_9UWJkSjVRM0lKRUE/view?usp=sharing 

Thanks for help.

Have a nice day!

Qian