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

[Peter C. M. <pcm...@em...>]

Eric,

the check 'Object' argument is a left-over, and indeed null (I should  
clean it up). Extracting JPF object values from normal Properties is  
difficult. You get the vm, and from there you can obtain the  
DynamicArea (heap), but you still have to know the object reference  
(ElementInfo index) for your object in question. The problem is that  
'check' is evaluated after executing the whole transition, i.e. many  
instructions, so you don't have the instruction context anymore. Any  
property that needs this (e.g. to monitor certain field values)  
should better be a VMListener. For this specific purpose, there is a  
generic PropertyListenerAdapter class that implements the listener  
and property interfaces (see gov.nasa.jpf.tools.RaceDetector as an  
example - note that those properties get automatically registered  
during the SearchListener.searchStarted() notification). That's  
probably the best choice if your properties depend on object values,  
and not general search or vm execution states.

-- Peter

> 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.