Hello,
I want to run JPF on a project importing some .jar libraries. However, I always met ClassNotFoundException. Tracing back the exception by line number, I find it's the place that the external class appears for the first time.
So I'm wondering how can I import the .jar library? I'm using the latest version of jpf-core and jpf-symbc and I can run the example symbolic execution (SE) successfully. I have tried to put the .jar file at jpf-symbc/lib but that doesn't work. I compile the code with ant and set debug=true for javac.
Below is the error msg I got:
~/jpf/jpf-symbc$ ../jpf-core/bin/jpf /home/zzy/jpf/floodlight/src/main/java/net/floodlightcontroller/hub/Hub.jpf
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=
2147483647symbolic.max_pc_msec=0
symbolic.min_int=-1000000
symbolic.max_int=1000000
symbolic.min_double=-8.0
symbolic.max_double=7.0
JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.
====================================================== system under test
net.floodlightcontroller.hub.Hub.main()
====================================================== search started: 11/19/15 2:23 PM
====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.ClassNotFoundException: class not found: org.slf4j.LoggerFactory
at net.floodlightcontroller.hub.Hub.<clinit>(Hub.java:51)
====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
owned locks:java.lang.Class@b3
call stack:
at net.floodlightcontroller.hub.Hub.<clinit>(Hub.java:51)
====================================================== Method Summaries
====================================================== Method Summaries (HTML)
====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ClassNotFoundException: class not found:..."
====================================================== statistics
elapsed time: 00:00:01
states: new=1,visited=0,backtracked=1,end=0
search: maxDepth=1,constraints=0
choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap: new=371,released=0,maxLive=0,gcCycles=0
instructions: 3100
max memory: 30MB
loaded code: classes=67,methods=1328
Thanks in advance!
Zhenyu