1) changes on the definitely written analysis: it only takes care about locations...

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

diff --git a/Robust/src/Tests/ssJava/mp3decoder/Player.java b/Robust/src/Tests/ssJava/mp3decoder/Player.java
index d82e6e8919b8d49bad2ce04a23a01650e13aa970..e3a92107591b6890580c11cb63f1daaeb2a5da71 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/Player.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/Player.java
@@ -107,16 +107,22 @@ public class Player {
    * @return true if the last frame was played, or false if there are more\r
    *         frames.\r
    */\r
-  @LATTICE("T<IN,T*,IN*,THISLOC=T")\r
-  @RETURNLOC("T")\r
+  @LATTICE("OUT<THIS,THIS<IN,IN*,THISLOC=THIS")\r
+  @RETURNLOC("OUT")\r
   public boolean play(@LOC("IN") int frames) throws JavaLayerException {\r
-    @LOC("T") boolean ret = true;\r
-    \r
-    @LOC("T") int count=0;\r
+    @LOC("OUT") boolean ret = true;\r
+\r
+    // initialization before ssjava loop\r
+    @LOC("THIS,Player.FR") boolean init = true;\r
+    @LOC("THIS,Player.ST") Header h = BitstreamWrapper.readFrame();\r
+    decoder.init(h);\r
+\r
+    @LOC("IN") int count = 0;\r
     SSJAVA: while (count++ < 2147483646) {\r
-      ret = decodeFrame();\r
-      if(!ret){\r
-          break;\r
+      ret = decodeFrame(init, h);\r
+      init = false;\r
+      if (!ret) {\r
+        break;\r
       }\r
     }\r
 \r
@@ -175,14 +181,17 @@ public class Player {
    * @return true if there are no more frames to decode, false otherwise.\r
    */\r
   @LATTICE("C<THIS,O<THIS,THIS<IN,C*,THISLOC=THIS,RETURNLOC=O,GLOBALLOC=THIS")\r
-  protected boolean decodeFrame() throws JavaLayerException {\r
+  protected boolean decodeFrame(@LOC("THIS,Player.FR") boolean init, @LOC("THIS,Player.ST") Header h)\r
+      throws JavaLayerException {\r
     try {\r
       // AudioDevice out = audio;\r
       // if (out==null)\r
       // return false;\r
 \r
       // Header h = bitstream.readFrame();\r
-      @LOC("THIS,Player.ST") Header h = BitstreamWrapper.readFrame();\r
+      if (!init) {\r
+        h = BitstreamWrapper.readFrame();\r
+      }\r
 \r
       if (h == null)\r
         return false;\r
@@ -194,8 +203,7 @@ public class Player {
       @LOC("C") int sum = 0;\r
       @LOC("C") short[] outbuf = SampleBufferWrapper.getBuffer();\r
       // short[] outbuf = output.getBuffer();\r
-      TERMINATE:\r
-      for (@LOC("C") int i = 0; i < SampleBufferWrapper.getBufferLength(); i++) {\r
+      TERMINATE: for (@LOC("C") int i = 0; i < SampleBufferWrapper.getBufferLength(); i++) {\r
         // System.out.println(outbuf[i]);\r
         sum += outbuf[i];\r
       }\r