javapathfinder-user

[Jenny c. <je...@gm...>]

Hi,
I'm having trouble with the ArrayIndexOutOfBoundsException. I'm not sure if
it's a problem of my application or not. Did anyone have this problem
before?

Thanks,
Jenny

Java Pathfinder Model Checker v3.1.2 - (C) 1999-2005 RIACS/NASA Ames
Research Center
JPF exception, terminating: class java.lang.ArrayIndexOutOfBoundsException:
9

java.lang.ArrayIndexOutOfBoundsException: 9
    at gov.nasa.jpf.jvm.StackFrame.push(StackFrame.java:862)
    at gov.nasa.jpf.jvm.ThreadInfo.push(ThreadInfo.java:1853)
    at gov.nasa.jpf.jvm.ThreadInfo.finish(ThreadInfo.java:1584)
    at gov.nasa.jpf.jvm.ThreadInfo.popFrame(ThreadInfo.java:1808)
    at gov.nasa.jpf.jvm.ThreadInfo.throwException(ThreadInfo.java:1961)
    at gov.nasa.jpf.jvm.bytecode.ATHROW.execute(ATHROW.java:43)
    at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1508)
    at gov.nasa.jpf.jvm.ThreadInfo.executePorStep(ThreadInfo.java:2104)
    at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1568)
    at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:285)
    at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1120)
    at gov.nasa.jpf.search.AbstractSearch.forward(AbstractSearch.java:340)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:92)
    at gov.nasa.jpf.JPF.run(JPF.java:311)
    at gov.nasa.jpf.JPF.main(JPF.java:238)
java.lang.ArrayIndexOutOfBoundsException: 9
    at gov.nasa.jpf.jvm.StackFrame.push(StackFrame.java:862)
    at gov.nasa.jpf.jvm.ThreadInfo.push(ThreadInfo.java:1853)
    at gov.nasa.jpf.jvm.ThreadInfo.finish(ThreadInfo.java:1584)
    at gov.nasa.jpf.jvm.ThreadInfo.popFrame(ThreadInfo.java:1808)
    at gov.nasa.jpf.jvm.ThreadInfo.throwException(ThreadInfo.java:1961)
    at gov.nasa.jpf.jvm.bytecode.ATHROW.execute(ATHROW.java:43)
    at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1508)
    at gov.nasa.jpf.jvm.ThreadInfo.executePorStep(ThreadInfo.java:2104)
    at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:1568)
    at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:285)
    at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1120)
    at gov.nasa.jpf.search.AbstractSearch.forward(AbstractSearch.java:340)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:92)
    at gov.nasa.jpf.JPF.run(JPF.java:311)
    at gov.nasa.jpf.JPF.main(JPF.java:238)
gov.nasa.jpf.JPFException: class java.lang.ArrayIndexOutOfBoundsException: =
9
    at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1163)
    at gov.nasa.jpf.search.AbstractSearch.forward(AbstractSearch.java:340)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:92)
    at gov.nasa.jpf.JPF.run(JPF.java:311)
    at gov.nasa.jpf.JPF.main(JPF.java:238)