Robust/src/Benchmarks/SSJava/MP3Decoder/BitstreamWrapper.java

   1 public class BitstreamWrapper {
   2
   3   private static Bitstream stream;
   4   private static int idx=0;
   5
   6   @TRUST
   7   public static void init(String filename) {
   8     FileInputStream fin = new FileInputStream(filename);
   9     BufferedInputStream bin = new BufferedInputStream(fin);
  10     stream = new Bitstream(bin);
  11   }
  12
  13   @TRUST
  14   public static Header readFrame() {
  15     Header h=stream.readFrame();
  16     h.idx=idx++;
  17     return h;
  18   }
  19
  20 }