#54 ArrayIndexOutOfBoundsException

[ispir]

When I run JPF with a simple concurrent AspectJ code, JPF throws below exception:

relase: trunk (30.01.2008)
java: 1.5.0_13
java compiler and version: jdk1.5.0_13/liba/tools.jar
JPF runs with default options and with argument "den.BufferClass".
eclipse: 3.3
I attached the related classfiles and sources

java.lang.ArrayIndexOutOfBoundsException
at java.lang.System.arraycopy(Native Method)
at gov.nasa.jpf.util.ObjVector.append(ObjVector.java:109)
at gov.nasa.jpf.jvm.CollapsingRestorer.updateThreadCache(CollapsingRestorer.java:109)
at gov.nasa.jpf.jvm.CollapsingRestorer.updateThreadListCache(CollapsingRestorer.java:79)
at gov.nasa.jpf.jvm.CollapsingRestorer.computeRestorableData(CollapsingRestorer.java:63)
at gov.nasa.jpf.jvm.CollapsingRestorer.computeRestorableData(CollapsingRestorer.java:1)
at gov.nasa.jpf.jvm.AbstractRestorer.getRestorableData(AbstractRestorer.java:35)
at gov.nasa.jpf.jvm.DefaultBacktracker.pushKernelState(DefaultBacktracker.java:82)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1246)
at gov.nasa.jpf.search.Search.forward(Search.java:357)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:86)
at gov.nasa.jpf.JPF.run(JPF.java:392)
at gov.nasa.jpf.JPF.main(JPF.java:319)
[SEVERE] JPF exception, terminating: class java.lang.ArrayIndexOutOfBoundsException: null
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFException: class java.lang.ArrayIndexOutOfBoundsException: null
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1293)
at gov.nasa.jpf.search.Search.forward(Search.java:357)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:86)
at gov.nasa.jpf.JPF.run(JPF.java:392)
at gov.nasa.jpf.JPF.main(JPF.java:319)

[ispir]

classfiles and sources