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 Buffer extends java.lang.Object
  {
     long address;
  
  
     /*@ requires true; ensures true; assignable \everything; */
     public final int capacity();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final int position();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.Buffer position(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final int limit();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.Buffer limit(int arg0);
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.Buffer mark();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.Buffer reset();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.Buffer clear();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.Buffer flip();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final java.nio.Buffer rewind();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final int remaining();
  
     /*@ requires true; ensures true; assignable \everything; */
     public final boolean hasRemaining();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract boolean isReadOnly();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract boolean hasArray();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract java.lang.Object array();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract int arrayOffset();
  
     /*@ requires true; ensures true; assignable \everything; */
     public abstract boolean isDirect();
  }
  