[Javapathfinder-user] BUG: Too rigorously POR on array operations (Test model included)

[Viet Y. N. <v.y...@al...>]

Hi,

While testing our own model checker 
(http://www.cs.utwente.nl/~ruys/mmc/), I discovered, what I believe, is 
a bug in yours. The attached model has assertion violations, but JPF 
does not find them.

It is a POR bug in JPF, as JPF considers array operations as scheduling 
irrelevant on the assumption that an array operation is always preceded 
by a getfield/getstatic, which is scheduling relevant. This is not true.

Below is a trace to the undetected assertion violation.

Could you please verify this bug?

With regards,

Viet Yen



Trace to assertion violation:

t1: getfield arr 	(gets reference to arr)
t2: getfield arr	(gets reference to arr)	
t1: iaload  		(loads 0 from arr)
t1: iadd		(adds 1, result is 1 on t1's stack)		
t2: iaload		(loads 0 from arr)
t2: iadd		(adds 1, result is 1 on t2's stack)		
t1: iastore		(stores 1 to arr)
t2: iastore		(stores 1 to arr)
t0: check assertion