Short update:
I found the cause of my NullPointerException. Turns out that
MJIEnv.getClassInfo() returns null sometimes, which is not handled
properly. Actually, INVOKEVIRTUAL.execute() wants to notify me that some
method could not be found (INVOKEVIRTUAL.getInvokedMethod() returns
null). The method in question is evaluate() on the predicate I wrote.
This happens after JPF verified the first couple of states of my
program. Before, it is able to execute evaluate(). I guess I am missing
out on something essential here. If I remove the ContractVerifier from
my listeners, everything works find (obviously).
Here is my configuration, maybe I messed up here?
@using=jpf-symbc
@using=jpf-aprop
# Taken directly from jpf-aprop examples
listener.autoload=\
javax.annotation.Nonnull,\
javax.annotation.concurrent.GuardedBy,\
gov.nasa.jpf.annotation.Const,\
gov.nasa.jpf.annotation.NonShared,\
gov.nasa.jpf.annotation.Invariant,\
gov.nasa.jpf.annotation.Ensures,\
gov.nasa.jpf.annotation.Requires
listener.javax.annotation.Nonnull=gov.nasa.jpf.aprop.listener.NonnullChecker
listener.javax.annotation.concurrent.GuardedBy=gov.nasa.jpf.aprop.listener.LockChecker
listener.gov.nasa.jpf.annotation.Const=gov.nasa.jpf.aprop.listener.ConstChecker
listener.gov.nasa.jpf.annotation.NonShared=gov.nasa.jpf.aprop.listener.NonSharedChecker
listener.gov.nasa.jpf.annotation.Invariant=gov.nasa.jpf.aprop.listener.ContractVerifier@pbc
listener.gov.nasa.jpf.annotation.Ensures=gov.nasa.jpf.aprop.listener.ContractVerifier@pbc
listener.gov.nasa.jpf.annotation.Requires=gov.nasa.jpf.aprop.listener.ContractVerifier@pbc
# Link to binaries and libraries
classpath =
${config_path}/../bin:${config_path}/../lib/multiverse-core-0.7.0.jar
sourcepath = ${config_path}/src:${config_path}/verify
native_classpath+=:${config_path}/../bin:${config_path}/verify
type_classpath+=:${config_path}/../bin:${config_path}/verify
# Specify driver
target = dk.itu.parallel.morphology.verify.FilterDriver
vm.insn_factory.class = gov.nasa.jpf.symbc.SymbolicInstructionFactory
vm.storage.class = nil
vm.por = true
# Configure symbolic execution
symbolic.min_int = 0
symbolic.max_int = 9
symbolic.debug = true
# Constraint solvers
symbolic.dp = omega.native
#symbolic.dp = coral
symbolic.lazy = true
symbolic.lazy.subtypes = true
#search.class = gov.nasa.jpf.search.heuristic.BFSHeuristic
#search.class = gov.nasa.jpf.search.heuristic.Interleaving
search.class = gov.nasa.jpf.search.heuristic.DFSHeuristic
search.depth_limit = 9
#listener = gov.nasa.jpf.aprop.listener.ContractVerifier
listener+=,gov.nasa.jpf.symbc.SymbolicListener
listener+=,gov.nasa.jpf.symbc.heap.HeapSymbolicListener
listener+=,gov.nasa.jpf.listener.PreciseRaceDetector
search.multiple_errors = true
log.info = gov.nasa.jpf.vm.ClassInfo
log.info+=,gov.nasa.jpf.aprop
cg.max_processors = 3
Any help is much appreciated!
Florian