[Javapathfinder-user] Specifying properties using "Property" scheme

[Eric P. <pl...@ni...>]

Hi everyone,

This question echoes the one from M=EDrian Bruckschen about Specifying
properties using "Listener" scheme.

Since June, our group has started using JPF and we are about writing =
custom
properties. I am trying to figure out how to configure my own properties
according to the documentation, but for the moment my trials are not
conclusive. The first way to implement properties =
(gov.nasa.jpf.Property)
seems sufficient for our current needs, so I have only tried to =
configure
this one.

My question targets the check(VM,Object) method: Is it possible to =
extract
the variable we need to check from the arguments? If yes, I have not =
find
how for the moment. For example, I tried to observe step-by-step with =
jdb
the behavior of JPF on a simple toy program (to check some assertions on
variable values). Setting a breakpoint on the check(VM,Object) method of
NoAssertionViolatedProperty, it turns out that the local variables vm =
and
arg are null and throw a NullPointerException when accessed.

My group suggested other ideas to test out, but if anyone has experience =
on
that or encounters the same issue, let's get in touch.

Eric Platon