Error in executing examples

[Alim9100]

hello I wanted to run some examples in the src/examples. but an error issues every time. can u help?

[Console output redirected to file:C:\Users\ASUS\Desktop\output] [WARNING] unknown classpath element: C:\Users\ASUS\Desktop\JPF\jpf-symbc\build\jpf-symbc-classes.jar [WARNING] unknown classpath element: C:\Users\ASUS\Desktop\JPF\jpf-core\build\jpf-classes.jar [WARNING] unknown classpath element: C:\Users\ASUS\Desktop\JPF\jpf-core\build\examples Running Symbolic PathFinder ... symbolic.dp=choco symbolic.string_dp_timeout_ms=0 symbolic.string_dp=none symbolic.choco_time_bound=30000 symbolic.max_pc_length=2147483647 symbolic.max_pc_msec=0 symbolic.bvlength=32 symbolic.min_int=-2147483648 symbolic.min_long=-9223372036854775808 symbolic.min_short=-32768 symbolic.min_byte=-128 symbolic.min_char=0 symbolic.max_int=2147483647 symbolic.max_long=9223372036854775807 symbolic.max_short=32767 symbolic.max_byte=127 symbolic.max_char=65535 symbolic.min_double=4.9E-324 symbolic.max_double=1.7976931348623157E308 [WARNING] orphan NativePeer method: java.lang.Class.initialize0()V [WARNING] orphan NativePeer method: java.lang.Class.getByteArrayFromResourceStream(Ljava/lang/String;)[B [WARNING] orphan NativePeer method: java.lang.Class.getResolvedName(Ljava/lang/String;)Ljava/lang/String; [WARNING] orphan NativePeer method: java.lang.ClassLoader.getResource0(Ljava/lang/String;)Ljava/lang/String; [WARNING] orphan NativePeer method: java.lang.ClassLoader.getResources0(Ljava/lang/String;)[Ljava/lang/String; [WARNING] orphan NativePeer method: java.lang.ClassLoader.defineClass0(Ljava/lang/String;[BII)Ljava/lang/Class; gov.nasa.jpf.vm.ClassInfoException: class not found: gov.nasa.jpf.BoxObjectCaches at gov.nasa.jpf.vm.ClassLoaderInfo.getResolvedClassInfo(ClassLoaderInfo.java:363) at gov.nasa.jpf.vm.SystemClassLoaderInfo.getResolvedClassInfo(SystemClassLoaderInfo.java:147) at gov.nasa.jpf.vm.VM.getStartupSystemClassInfos(VM.java:445) at gov.nasa.jpf.vm.VM.initializeMainThread(VM.java:564) at gov.nasa.jpf.vm.SingleProcessVM.initialize(SingleProcessVM.java:130) at gov.nasa.jpf.JPF.run(JPF.java:611) at gov.nasa.jpf.JPF.start(JPF.java:189) at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source) at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source) at java.lang.reflect.Method.invoke(Unknown Source) at gov.nasa.jpf.tool.Run.call(Run.java:80) at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116) [SEVERE] cannot load system class gov.nasa.jpf.BoxObjectCaches

[corinus]

Hi: There are some warnings: [WARNING] unknown classpath element: ... Did you build jpf-core and jpf-symbc correctly? Did you run ant? The site.properties file should also be set up.

[1saacYing]

Hi Alim, do you settle this problem? I have met it but i still confuse about it. Thanks

[yannicnoller]

Hi @1saacYing, can you mention some more details that allow reproducing your problem? Which java version are you using? How did you set up the site.properties?

We are currently working on updating the README file to make the setup easier. In the meantime, you may find this post here helpful: https://sudsy-spear-592.notion.site/Symbolic-PathFinder-Setup-47fe784d81614f98b4525f260618fa35

[1saacYing]

Hello, @yannicnoller ,my java version is jdk-8u121 from Oracle, and I have tried jdk-8u20 which causes "JavaObjectInputStreamAccess cannot be resolved to a type SharedSecrets.java /jpf-core/src/classes/sun/misc" but jkd-8u121 can handle this problem. I have created a site.properties in ~/jpf site.properties jpf-core/ jpf-symbc/ … and ~/.jpf has a same site.properties

the site.properties: jpf-core = ${user.home}/jpf/jpf-core jpf-symbc = ${user.home}/jpf/jpf-symbc

extensions = $ {jpf-core}, $ {jpf-symbc}

I met the problem when I imported the jpf-core as a project in eclipse, and i run a .jpf in src/examples Thanks

[yannicnoller]

Hi @1saacYing! It seems you run simply JPF instead of SPF, so you might want to raise your issue in the jpf-core repository: https://github.com/javapathfinder/jpf-core. Nevertheless, the example works on my setup:

JavaPathfinder core system v8.0 - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test
Racer.main()

====================================================== search started: 28/7/22 9:04 PM
10
10

====================================================== error 1
gov.nasa.jpf.listener.PreciseRaceDetector
race for field Racer@15b.d
  main at Racer.main(Racer.java:35)
        "int c = 420 / racer.d;               // (4)"  READ:  getfield Racer.d
  Thread-1 at Racer.run(Racer.java:26)
        "d = 0;                               // (2)"  WRITE: putfield Racer.d

====================================================== trace #1
------------------------------------------------------ transition #0 thread: 0
gov.nasa.jpf.vm.choice.ThreadChoiceFromSet {id:"ROOT" ,1/1,isCascaded:false}
      [3157 insn w/o sources]
  Racer.java:30                  : Racer racer = new Racer();
  Racer.java:19                  : public class Racer implements Runnable {
      [1 insn w/o sources]
  Racer.java:21                  : int d = 42;
  Racer.java:30                  : Racer racer = new Racer();
  Racer.java:31                  : Thread t = new Thread(racer);
      [145 insn w/o sources]
  Racer.java:31                  : Thread t = new Thread(racer);
  Racer.java:32                  : t.start();
      [1 insn w/o sources]
------------------------------------------------------ transition #1 thread: 0
gov.nasa.jpf.vm.choice.ThreadChoiceFromSet {id:"START" ,1/2,isCascaded:false}
      [2 insn w/o sources]
  Racer.java:34                  : doSomething(1000);                   // (3)
  Racer.java:41                  : try { Thread.sleep(n); } catch (InterruptedException ix) {}
      [4 insn w/o sources]
------------------------------------------------------ transition #2 thread: 1
gov.nasa.jpf.vm.choice.ThreadChoiceFromSet {id:"SLEEP" ,2/2,isCascaded:false}
      [1 insn w/o sources]
  Racer.java:1                   : /*
  Racer.java:25                  : doSomething(1001);                   // (1)
  Racer.java:41                  : try { Thread.sleep(n); } catch (InterruptedException ix) {}
      [4 insn w/o sources]
------------------------------------------------------ transition #3 thread: 1
gov.nasa.jpf.vm.choice.ThreadChoiceFromSet {id:"SLEEP" ,2/2,isCascaded:false}
      [3 insn w/o sources]
  Racer.java:41                  : try { Thread.sleep(n); } catch (InterruptedException ix) {}
  Racer.java:42                  : }
  Racer.java:26                  : d = 0;                               // (2)
------------------------------------------------------ transition #4 thread: 0
gov.nasa.jpf.vm.choice.ThreadChoiceFromSet {id:"SHARED_OBJECT" ,1/2,isCascaded:false}
      [3 insn w/o sources]
  Racer.java:41                  : try { Thread.sleep(n); } catch (InterruptedException ix) {}
  Racer.java:42                  : }
  Racer.java:35                  : int c = 420 / racer.d;               // (4)
------------------------------------------------------ transition #5 thread: 0
gov.nasa.jpf.vm.choice.ThreadChoiceFromSet {id:"SHARED_OBJECT" ,1/2,isCascaded:false}
  Racer.java:35                  : int c = 420 / racer.d;               // (4)

====================================================== results
error #1: gov.nasa.jpf.listener.PreciseRaceDetector "race for field Racer@15b.d   main at Racer.main(Ra..."

====================================================== statistics
elapsed time:       00:00:00
states:             new=9,visited=1,backtracked=4,end=2
search:             maxDepth=6,constraints=0
choice generators:  thread=8 (signal=0,lock=1,sharedRef=2,threadApi=3,reschedule=2), data=0
heap:               new=362,released=33,maxLive=357,gcCycles=7
instructions:       3424
max memory:         245MB
loaded code:        classes=62,methods=1477

====================================================== search finished: 28/7/22 9:04 PM

I am using a later Java version, you also might want to try this.

yannic@Yannics-MacBook-Pro jpf-symbc % java -version
openjdk version "1.8.0_312"
OpenJDK Runtime Environment (Temurin)(build 1.8.0_312-b07)
OpenJDK 64-Bit Server VM (Temurin)(build 25.312-b07, mixed mode)

[yannicnoller]

Sure, feel free to let me know if you need more help! I will keep the issue open for now. Eclipse+ant works; my output was produced via Eclipse. We are currently working on an update to Gradle, though.

[1saacYing]

Hi @yannicnoller , could you tell me the ant version of your setup, because this is my first time using ant, so I'm not familiar with it. And how can I display the result through Eclipse after ant build? import the project to Eclipse like the post shows in SPF part?

[yannicnoller]

yannic@Yannics-MacBook-Pro jpf-core % ant -version
Apache Ant(TM) version 1.10.12 compiled on October 13 2021

But I am not sure whether the ant version would make such a difference.

For Eclipse: yes, the post shows an example. You select a .jpf file and then run it with the JPF/SPF run-config.

Did you try to run the example from the command line? The post also shows an example. If that works, it would at least show that your general setup is working and that the error must be found in your Eclipse setup.

[1saacYing]

Hello @yannicnoller, I am working on the command line and I have built successful. May I ask you about the code to run the .jpf get the result which you showed me before?

[1saacYing]

Hi @yannicnoller I can run .jpf with the JPF/SPF run-config. But eclipse still shows some problem about java version. Could you help me?

[yannicnoller]

Hi @1saacYing! Which Java version are you using in the Eclipse project configuration? You need to make sure that you also use Java 8.

[1saacYing]

Hi @yannicnoller , I use java -8 but there are some problem about src/peers and why does error show that it needs JRE version more than 11? And eclipse shows some errors

Finally, Could you help me how to run the example in command line, if i want to run NumericExample.jpf? I tried the code on the post but I failed.

Thank you very much.

[1saacYing]

I can run a part of examples but some is not successful. For example the examples/TestArray.jpf, which shows no libz3java in java.library.path.

[yannicnoller]

I can run a part of examples but some is not successful.

That is possible. Not all examples might be functional right now. If you find examples that are not working, please open an issue and I will look into it.

For example the examples/TestArray.jpf, which shows no libz3java in java.library.path.

Please check my post for this one; I am explaining how to set the correct path.

Finally, Could you help me how to run the example in command line, if i want to run NumericExample.jpf? I tried the code on the post but I failed.

I need more info to help here! It works for me.

I use java -8 but there are some problem about src/peers and why does error show that it needs JRE version more than 11?

I cannot reproduce this error. Which branch are you using? Which git commit? It seems not the latest master because the DNNArchitectureFactory.java is not included in there, is it?

[1saacYing]

Hi @yannicnoller, Thank you very much for your reply which really helps me a lot and I'm sorry I didn't see below that you have provided a solution to the library path problem.

Yes. I am not use the latest master, i find it from another author. https://github.com/corinus/neurospf.git. I will try the official version now.

[yannicnoller]

No problem, I am happy to help!

https://github.com/corinus/neurospf.git

This repository has some additions for the efficient analysis of neural networks. Maybe you first try the latest SPF official version, and then we can figure out what does not work with NeuroSPF, but for that you probably want to open an issue in that specific repository instead of here.

[1saacYing]

Hi @yannicnoller, I have successfully run the latest SPF official version. And I will try the neuroSPF base on it. your post is amazing !! Cheers

[yannicnoller]

@1saacYing! Okay, great. Then I will close this issue here now.