#66 Fixed-size output buffer makes OutputStreamWriter crash

[Strider]

For long strings, OutputStreamWriter.write is guaranteed to crash.
Both env/jpf/java/io/OutputStreamWriter.java and env/jvm/gov/nasa/jpf/jvm/JPF_java_io_OutputStreamWriter.java have a fixed BUF_SIZE of 128. When writing a string of length 129 to the OutputStreamWriter, that method will cause a BufferOverFlowException:

at java.nio.Buffer.nextPutIndex(Buffer.java:419)
at java.nio.HeapCharBuffer.put(HeapCharBuffer.java:145)
at gov.nasa.jpf.jvm.JPF_java_io_OutputStreamWriter.encode___3CII_3B__I(JPF_java_io_OutputStreamWriter.java:45)
at gov.nasa.jpf.jvm.JPF_java_io_OutputStreamWriter.encode__Ljava_lang_String_2II_3B__I(JPF_java_io_OutputStreamWriter.java:65)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
at java.lang.reflect.Method.invoke(Method.java:585)
at gov.nasa.jpf.jvm.NativePeer.executeMethod(NativePeer.java:201)
at gov.nasa.jpf.jvm.MethodInfo.execute(MethodInfo.java:828)
at gov.nasa.jpf.jvm.bytecode.INVOKESPECIAL.execute(INVOKESPECIAL.java:62)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1637)
at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:2341)
at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:506)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1467)
at gov.nasa.jpf.search.Search.forward(Search.java:403)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:83)
at gov.nasa.jpf.JPF.run(JPF.java:529)
at gov.nasa.jpf.JPF.main(JPF.java:161)

Fix: rewrite the code such that it uses the buffer in small (buffer-sized) chunks, multiple times per loop. There is such a loop in the code now, but it seems not to have been written/tested properly.

Workaround: Declare a much larger buffer :-)

[Strider]

Simple example with a 129-byte string written to an OutputStreamWriter