I get an ArrayOutOfBoundsException when I run JPF and specify the classpath through -cp. The error occurs on in gov/nasa/jpf/Config.java on line 1314.
buf[i1] overflows when i == n - 1 and i1 == n. Since n is the length of buf, the expression reaches beyond the end of the buffer.
Here is the command that I ran to get this error.
java -cp .:/home/jwu/src/javapathfinder/trunk/lib/bcel.jar:/home/jwu/src/javapathfinder/trunk/build/jpf/ gov.nasa.jpf.JPF +vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory +jpf.listener=gov.nasa.jpf.symbc.SymbolicListener +vm.storage.class= +symbolic.method='myMethod(sym#sym)' +search.multiple_errors=true +jpf.report.console.finished= +vm.classpath=.:/home/jwu/src/javapathfinder/trunk/lib/bcel.jar:/home/jwu/src/javapathfinder/trunk/build/jpf/ MyClass1
The JPF version was the SVN trunk checked out on 12/4/08