have linear-type-safe source codes of mp3decoder

[IRC.git] / Robust / src / Tests / ssJava / mp3decoder / BitstreamWrapper.java

diff --git a/Robust/src/Tests/ssJava/mp3decoder/BitstreamWrapper.java b/Robust/src/Tests/ssJava/mp3decoder/BitstreamWrapper.java
new file mode 100644 (file)
index 0000000..6a3209d
--- /dev/null
+++ b/Robust/src/Tests/ssJava/mp3decoder/BitstreamWrapper.java
@@ -0,0 +1,17 @@
+public class BitstreamWrapper {
+
+  private static Bitstream stream;
+
+  @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() {
+    return stream.readFrame();
+  }
+
+}