content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.nio.charset;
  
  public abstract class CharsetDecoder extends java.lang.Object
  {
     final static boolean $assertionsDisabled;
  
  
     /*@ requires true; ensures true; assignable \everything; */
     protected CharsetDecoder(java.nio.charset.Charset arg0, float arg1, float arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.charset.Charset charset();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.lang.String replacement();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.charset.CharsetDecoder replaceWith(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     protected void implReplaceWith(java.lang.String arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.charset.CodingErrorAction malformedInputAction();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.charset.CharsetDecoder onMalformedInput(java.nio.charset.CodingErrorAction arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     protected void implOnMalformedInput(java.nio.charset.CodingErrorAction arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.charset.CodingErrorAction unmappableCharacterAction();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.charset.CharsetDecoder onUnmappableCharacter(java.nio.charset.CodingErrorAction arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     protected void implOnUnmappableCharacter(java.nio.charset.CodingErrorAction arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final float averageCharsPerByte();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final float maxCharsPerByte();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.charset.CoderResult decode(java.nio.ByteBuffer arg0, java.nio.CharBuffer arg1, boolean arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.charset.CoderResult flush(java.nio.CharBuffer arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     protected java.nio.charset.CoderResult implFlush(java.nio.CharBuffer arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.charset.CharsetDecoder reset();
  
     /*@ requires true; ensures true; assignable \everything; */
     protected void implReset();
  
     /*@ requires true; ensures true; assignable \everything; */
     protected abstract java.nio.charset.CoderResult decodeLoop(java.nio.ByteBuffer arg0, java.nio.CharBuffer arg1);
  
     /*@ requires true; ensures true; assignable \everything; signals (java.nio.charset.CharacterCodingException e) true; */
     public final java.nio.CharBuffer decode(java.nio.ByteBuffer arg0) throws java.nio.charset.CharacterCodingException;
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isAutoDetecting();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean isCharsetDetected();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.charset.Charset detectedCharset();
  }
  