no libz3java in java.library.path

[muhammad irfan]

Hello, can someone help me?  i want to try verify a class in jpf-symbc modul , i verify the Assume.jpf but its error. (other jpf is too). what should i do? thanks

Executing command: java -jar D:\Irfan\Kuliah\Semester7\Skripsi\Aplikasi\jpf-core\build\RunJPF.jar +shell.port=4242 D:\Irfan\Kuliah\Semester7\Skripsi\Aplikasi\jpf-symbc\src\examples\Assume.jpf 

symbolic.min_int=-100

symbolic.min_long=-9223372036854775808

symbolic.min_short=-32768

symbolic.min_byte=-128

symbolic.min_char=0

symbolic.max_int=100

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

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

====================================================== system under test

Assume.main()

====================================================== search started: 05/03/18 0:47

java.lang.UnsatisfiedLinkError: no libz3java in java.library.path

at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1867)

at java.lang.Runtime.loadLibrary0(Runtime.java:870)

at java.lang.System.loadLibrary(System.java:1122)

at com.microsoft.z3.Native.<clinit>(Native.java:14)

at com.microsoft.z3.Context.<init>(Context.java:62)

at gov.nasa.jpf.symbc.numeric.solvers.ProblemZ3$Z3Wrapper.<init>(ProblemZ3.java:74)

at gov.nasa.jpf.symbc.numeric.solvers.ProblemZ3$Z3Wrapper.getInstance(ProblemZ3.java:68)

at gov.nasa.jpf.symbc.numeric.solvers.ProblemZ3.<init>(ProblemZ3.java:94)

at gov.nasa.jpf.symbc.numeric.SymbolicConstraintsGeneral.isSatisfiable(SymbolicConstraintsGeneral.java:110)

at gov.nasa.jpf.symbc.numeric.PathCondition.simplifyOld(PathCondition.java:454)

at gov.nasa.jpf.symbc.numeric.PathCondition.simplify(PathCondition.java:331)

at gov.nasa.jpf.symbc.bytecode.optimization.util.IFInstrSymbHelper.getNextInstructionAndSetPCChoice(IFInstrSymbHelper.java:574)

at gov.nasa.jpf.symbc.bytecode.optimization.IF_ICMPLE.execute(IF_ICMPLE.java:63)

at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)

at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)

at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)

at gov.nasa.jpf.vm.VM.forward(VM.java:1722)

at gov.nasa.jpf.search.Search.forward(Search.java:579)

at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)

at gov.nasa.jpf.JPF.run(JPF.java:613)

at gov.nasa.jpf.JPF.start(JPF.java:189)

at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)

at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)

at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)

at java.lang.reflect.Method.invoke(Method.java:498)

at gov.nasa.jpf.tool.Run.call(Run.java:80)

at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)

[Quoc-Sang Phan]

You should run jpf using the script jpf under jpf-core/bin

[muhammad irfan]

can you explain more detail? because i don't know how to use it, thank's ;)

[muhammad irfan]

On Monday, March 5, 2018 at 12:50:15 AM UTC+7, muhammad irfan wrote:

Like this? (look attach file)

[Quoc-Sang Phan]

Instead of: 

java -jar D:\Irfan\Kuliah\Semester7\Skripsi\Aplikasi\jpf-core\build\RunJPF.jar +shell.port=4242 D:\Irfan\Kuliah\Semester7\Skripsi\Aplikasi\jpf-symbc\src\examples\Assume.jpf 

You run: jpf-core/bin/jpf /path/to/Assume.jpf

Please read the wiki for more details.

[muhammad irfan]

Thank you for help me and answer the question. but sorry i will ask you a quetion. I has tried your "instead of" but its still eror and cmd reply "no libz3java" what should I do?

[Quoc-Sang Phan]

I see. You need to add the library path to the environment variable.

In Ubuntu you should include the path to libz3java (under jpf-symbc/lib) to the LD_LIBRARY_PATH variable.

It seems you are using Windows. You may try the solution in here:

https://stackoverflow.com/questions/7148036/what-is-ld-library-path-and-how-to-use-it

(I haven't used Windows for 10 years)

[muhammad irfan]

java -Djava.library.path=/path/to/my/dll -cp /my/classpath/goes/here MainClass

that the command, but i dont know what classpath should i do ? and which class??

like the picture ? its right?

On Monday, March 5, 2018 at 12:50:15 AM UTC+7, muhammad irfan wrote:

[Quoc-Sang Phan]

I do not see libz3.dll under jpf-symbc/lib, so perhaps z3 has not been set up for windows.

You can try cvc3, which is another SMT solver.

Did you try choco?, it is pure Java, and does not need any library.

[muhammad irfan]

Thanks for the help  now I can use the symbc.I create the new project and its work.  Thanks veryy muchhhh!!!

[ma wei]

Hi,

I encounter the same problem. How do you solve it? I use eclipse.

[Quoc-Sang Phan]

Add environment variable LD_LIBRARY_PATH to the configuration.