add source code that does not have location annotations.

[IRC.git] / Robust / src / Benchmarks / SSJava / MP3DecoderInfer / BitstreamWrapper.java

diff --git a/Robust/src/Benchmarks/SSJava/MP3DecoderInfer/BitstreamWrapper.java b/Robust/src/Benchmarks/SSJava/MP3DecoderInfer/BitstreamWrapper.java
new file mode 100644 (file)
index 0000000..344370c
--- /dev/null
+++ b/Robust/src/Benchmarks/SSJava/MP3DecoderInfer/BitstreamWrapper.java
@@ -0,0 +1,20 @@
+public class BitstreamWrapper {
+
+  private static Bitstream stream;
+  private static int idx=0;
+
+  @TRUST
+  public static void init(String filename) {
+    FileInputStream fin = new FileInputStream(filename);
+    BufferedInputStream bin = new BufferedInputStream(fin);
+    stream = new Bitstream(bin);
+  }
+
+  @TRUST
+  public static Header readFrame() {
+    Header h=stream.readFrame();
+    h.idx=idx++;
+    return h;
+  }
+
+}