content: /* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
   * Date: Wed Nov 26 11:26:00 CET 2014
   */
  package java.nio;
  
  public abstract class ByteBuffer extends java.nio.Buffer implements java.lang.Comparable
  {
     final byte[] hb;
     final int offset;
     boolean isReadOnly;
     boolean bigEndian;
     boolean nativeByteOrder;
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.nio.ByteBuffer allocateDirect(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.nio.ByteBuffer allocate(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.nio.ByteBuffer wrap(byte[] arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public static java.nio.ByteBuffer wrap(byte[] arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer slice();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer duplicate();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer asReadOnlyBuffer();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract byte get();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer put(byte arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract byte get(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer put(int arg0, byte arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.ByteBuffer get(byte[] arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.ByteBuffer get(byte[] arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.ByteBuffer put(java.nio.ByteBuffer arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.nio.ByteBuffer put(byte[] arg0, int arg1, int arg2);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.ByteBuffer put(byte[] arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final boolean hasArray();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final byte[] array();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final int arrayOffset();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer compact();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract boolean isDirect();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.String toString();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int hashCode();
  
     /*@ requires true; ensures true; assignable \everything; */
     public boolean equals(java.lang.Object arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public int compareTo(java.nio.ByteBuffer arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.ByteOrder order();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.ByteBuffer order(java.nio.ByteOrder arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract char getChar();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer putChar(char arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract char getChar(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer putChar(int arg0, char arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.CharBuffer asCharBuffer();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract short getShort();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer putShort(short arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract short getShort(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer putShort(int arg0, short arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ShortBuffer asShortBuffer();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract int getInt();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer putInt(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract int getInt(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer putInt(int arg0, int arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.IntBuffer asIntBuffer();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract long getLong();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer putLong(long arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract long getLong(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer putLong(int arg0, long arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.LongBuffer asLongBuffer();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract float getFloat();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer putFloat(float arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract float getFloat(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer putFloat(int arg0, float arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.FloatBuffer asFloatBuffer();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract double getDouble();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer putDouble(double arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract double getDouble(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.ByteBuffer putDouble(int arg0, double arg1);
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.nio.DoubleBuffer asDoubleBuffer();
  
     /*@ requires true; ensures true; assignable \everything; */
     public java.lang.Object array();
  
     /*@ requires true; ensures true; assignable \everything; */
     public int compareTo(java.lang.Object arg0);
  }
  