pietrobraione / jbse

A symbolic Java virtual machine for program analysis, verification and test generation
http://pietrobraione.github.io/jbse/
GNU General Public License v3.0
101 stars 29 forks source link

Error while running RunIf.java after all build. #52

Closed sjoon2455 closed 2 years ago

sjoon2455 commented 3 years ago

Hi, I followed complete tutorial on https://jbse-manual.readthedocs.io/en/latest/text/getting.html#a-basic-example. All I need to do is run the RunIf.java file, which yields the following error:

Could not open the dump file. The session will be displayed on console only.
This is the Java Bytecode Symbolic Executor's Run Tool (null v.null).
Connecting to Z3 at /Library/Frameworks/Python.framework/Versions/3.7/bin/z3.
Cannot find item in the classpath.
jbse.common.exc.ClasspathException: jbse.bc.exc.ClassFileNotFoundException: Did not find any class jbse/base/Base in the classpath.
    at jbse.algo.Action_START.loadCreateEssentialClasses(Action_START.java:331)
    at jbse.algo.Action_START.createStateStart(Action_START.java:158)
    at jbse.algo.Action_START.exec(Action_START.java:138)
    at jbse.jvm.Engine.init(Engine.java:167)
    at jbse.jvm.EngineBuilder.build(EngineBuilder.java:71)
    at jbse.jvm.RunnerBuilder.build(RunnerBuilder.java:56)
    at jbse.apps.run.Run.build(Run.java:708)
    at jbse.apps.run.Run.run(Run.java:588)
    at example.RunIf.main(RunIf.java:14)
Caused by: jbse.bc.exc.ClassFileNotFoundException: Did not find any class jbse/base/Base in the classpath.
    at jbse.bc.ClassHierarchy.loadCreateClass(ClassHierarchy.java:662)
    at jbse.algo.Action_START.loadCreateEssentialClasses(Action_START.java:325)
    ... 8 more

It seems like example project does not perfectly include jbse project...? How should I include it? The current way is to click on properties, Java Build Path, Projects, and then add jbse to the classpath within Projects. Let me attach the current configuration screen as well.

image

I hope you could help me out with this. Thanks for advance.

sjoon2455 commented 2 years ago

Resolved! It was just a path setting problem.

samirkelekar commented 2 years ago

Can you please post how exactly you solved the problem in a bit more detail ? I am facing the same issue.

sjoon2455 commented 2 years ago

Can you please post how exactly you solved the problem in a bit more detail ? I am facing the same issue.

@samirkelekar, you should be aware of path setting in RunIf.java file. Inside the main(String[] args), do System.out.println("Working Directory = " + System.getProperty("user.dir")); to find out current working directory. Then, collect the correct relative paths from the current working directory for

p.addUserClasspath("./bin");
p.setJBSELibPath("../jbse/build/libs/jbse-0.10.0-SNAPSHOT.jar");
p.setMethodSignature("example/IfExample", "(I)V", "func");
p.setExternalDecisionProcedurePath("/Library/Frameworks/Python.framework/Versions/3.7/bin/z3");

. In my case a path input to p.setJBSELibPath() was a problem. Better check those out!

samirkelekar commented 2 years ago

It worked. Thanks.