jpf-symbc JPF configuration error: class not found gov.nasa.jpf.symbc.SymbolicInstructionFactory

[Lannan Luo]

Hi, all,

I am new to jpf-symbc. I want to test an example in the jpf-symbc. I use eclipse to test the example. I can successfully test and verify the examples in jpf-core repo. But I cannot test any examples in jpf-symbc.

What I got is as follows. Anyone know how to solve it?

Thanks so much!

Executing command: java -jar /home/program/jpf/jpf-core/build/RunJPF.jar +site=/home/program/jpf/site.properties +shell.port=4242 /home/program/jpf/jpf-symbc/src/examples/Assume.jpf
[WARNING] unknown classpath element: /home/program/jpf/jpf-symbc/build/jpf-symbc-classes.jar
[SEVERE] JPF configuration error: class not found gov.nasa.jpf.symbc.SymbolicInstructionFactory by classloader: gov.nasa.jpf.JPFClassLoader@5caf905d
> used within "vm.classloader.class" instantiation of class gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo
> used within "vm.class" instantiation of class gov.nasa.jpf.vm.SingleProcessVM
[SEVERE] JPF terminated

[Kasper Søe Luckow]

Hi,

I note that:

[WARNING] unknown classpath element: /home/program/jpf/jpf-symbc/build/jpf-symbc-classes.jar

It should be there if you build jpf-symbc correctly (assuming that the site.properties file is also correctly set up).

Did you run the ant build?

Kasper

--

---
You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Lannan Luo]

Thanks for your reply.

Yes. The problem is solved.