mp3decoder passes the loop termination analysis.

[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 83851e297c749ae17143de3d8aed154414a871f5..2e2b02cd0e7d8cf975b21489a1a6bb27ed0144b0 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/Player.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/Player.java
@@ -111,9 +111,14 @@ public class Player {
   @RETURNLOC("T")\r
   public boolean play(@LOC("IN") int frames) throws JavaLayerException {\r
     @LOC("T") boolean ret = true;\r
-\r
-    SSJAVA: while (frames-- > 0 && ret) {\r
+    \r
+    int maxFrame=frames-1;\r
+    int count=0;\r
+    SSJAVA: while (count++ < maxFrame) {\r
       ret = decodeFrame();\r
+      if(!ret){\r
+          break;\r
+      }\r
     }\r
 \r
     /*\r
@@ -190,6 +195,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
         // System.out.println(outbuf[i]);\r
         sum += outbuf[i];\r