Need help in using Javapathfiner

[XINGYU ZHU]

Dear all,

I'm currently using Symbolic Pathfinder and Jpf-core. They are powerful tools to do some symbolic execution, but I've noticed that Jpf need a static entry to do some code analysis.

For example, if I comment the main entry below, an exception will be thrown. If I set "target.entry" to "foo", an exception will be thrown because foo is not a static method.

So I wonder:

1. what if I just want to analyze an non-static method directly?

2. Besides, what if the parameter is a self-defined class instead of an integer? How Could I symbolicly represent this parameter?

3. Is there any predecessor where integrate jpf with symbolic resolver (like z3 https://github.com/Z3Prover/z3)?

Thanks in advance.

Sincerely,

Xingyu ZHU.

[Cyrille Artho]

I'm not an SPF expert (others on this list can help) but regarding Point 1, it is impossible to call a non-static Java function as the entry point.

The object instance to call does not exist yet! So this is a language design issue, not a limitation in JPF or SPF.

You can always write a wrapper function as per your example.

[XINGYU ZHU]

Could you be more specific about the wrapper function please?

Thanks.

[Cyrille Artho]

What I meant was that the main function is the wrapper function that constructs an instance of "Example" and calls "foo" on that instance.