How to run jbse on java project?

[cparadox]

Hi,
I'm a new starter of jbse. I have succeeded in running jbse-examplse and getting result. Now I want to run jbse on other java project and analyze some method.
I tried to add the project's bin path to the CLASSPATH in Defs.java, and modify the METHOD_CLASS, METHOD_DESCRIPTOR, METHOD_NAME and OUT_FILE in RunIf.java:

public class RunExample {
    public static void main(String[] args) {
        final RunParameters p = new RunParameters();
        set(p);
        final Run r = new Run(p);
        r.run();
    }
	
    private static final String METHOD_CLASS      = "java/awt/Event"; 
    private static final String METHOD_DESCRIPTOR = "()Ljava/lang/String"; 
    private static final String METHOD_NAME       = "paramString"; 
    private static final Path   OUT_FILE          = EXAMPLES_HOME.resolve("out/runExample.txt");
    
    private static void set(RunParameters p) {
        p.setJBSELibPath(JBSE_CLASSPATH);
        p.addUserClasspath(CLASSPATH);
        p.addSourcePath(SOURCEPATH);
        p.setMethodSignature(METHOD_CLASS, METHOD_DESCRIPTOR, METHOD_NAME);
        p.setOutputFilePath(OUT_FILE);
        p.setDecisionProcedureType(DecisionProcedureType.Z3);
        p.setExternalDecisionProcedurePath(Z3_PATH);
        p.setStateFormatMode(StateFormatMode.TEXT);
        p.setStepShowMode(StepShowMode.LEAVES);
    }
}

but get error:

This is the Java Bytecode Symbolic Executor's Run Tool (null v.null).
Connecting to Z3 at E:\MyDownloads\z3-4.8.10-x64-win\bin\z3.exe.
Starting symbolic execution of method java/awt/Event:()Ljava/lang/String:paramString at Sat Mar 06 23:25:54 CST 2021.
Unexpected internal error.
jbse.common.exc.UnexpectedInternalException: jbse.common.exc.InvalidInputException: Tried to get a jzentry for an unknown zip file entry.
	at jbse.algo.Util.failExecution(Util.java:299)
	at jbse.algo.Algorithm.onInvalidInputException(Algorithm.java:181)
	at jbse.algo.Algorithm.exec(Algorithm.java:220)
	at jbse.jvm.Engine.step(Engine.java:312)
	at jbse.jvm.Runner.doRun(Runner.java:550)
	at jbse.jvm.Runner.run(Runner.java:520)
	at jbse.apps.run.Run.run(Run.java:597)
	at runthirdpartyprograms.RunExample.main(RunExample.java:22)
Caused by: jbse.common.exc.InvalidInputException: Tried to get a jzentry for an unknown zip file entry.
	at jbse.mem.State.getZipFileEntryJz(State.java:1757)
	at jbse.algo.meta.Algo_JAVA_ZIPFILE_GETENTRY_STARTS.cookMore(Algo_JAVA_ZIPFILE_GETENTRY_STARTS.java:63)
	at jbse.algo.Algo_INVOKEMETA_Nonbranching.lambda$0(Algo_INVOKEMETA_Nonbranching.java:41)
	at jbse.algo.Algorithm.doExec(Algorithm.java:236)
	at jbse.algo.Algorithm.exec(Algorithm.java:218)
	... 5 more
Symbolic execution finished at Sat Mar 06 23:26:00 CST 2021.

Could you please tell me where I have to modify?

[pietrobraione]

The methods that manipulate zip files are native in the Oracle classes (OpenJDK and derived). JBSE implements them metacitcularly - i.e., invokes the corresponding native methods of the JVM on which it runs. It is possible that you have spotted a bug (UnexpectedInternalExceptions are usually thrown when something that should never happen happens).