mp3decoder passes the loop termination analysis.

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

diff --git a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
index cd0d38e6021b7af49bf8c92242afe1a7d8db3cbe..31cd7a1c6e4c96703a3642147e22bd5c83adc60b 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
@@ -948,7 +948,8 @@ final class LayerIIIDecoder implements FrameDecoder {
 
     m = 0;
     for (@LOC("THIS,LayerIIIDecoder.NS") int i = 0; i < 4; i++) {
 
     m = 0;
     for (@LOC("THIS,LayerIIIDecoder.NS") int i = 0; i < 4; i++) {

-      for (@LOC("THIS,LayerIIIDecoder.NS") int j = 0; j < nr_of_sfb_block[blocknumber][blocktypenumber][i]; j++) {
+      int jmax=nr_of_sfb_block[blocknumber][blocktypenumber][i];
+      for (@LOC("THIS,LayerIIIDecoder.NS") int j = 0; j < jmax; j++) {

         scalefac_buffer[m] = (new_slen[i] == 0) ? 0 : br.hgetbits(new_slen[i]);
         m++;
 
         scalefac_buffer[m] = (new_slen[i] == 0) ? 0 : br.hgetbits(new_slen[i]);
         m++;
 


@@ -1071,6 +1072,7 @@ final class LayerIIIDecoder implements FrameDecoder {
 
     index = 0;
     // Read bigvalues area
 
     index = 0;
     // Read bigvalues area

+    TERMINATE:

     for (@LOC("THIS,LayerIIIDecoder.BR,BitReserve.BIT") int i = 0; i < (si.ch[ch].gr[gr].big_values << 1); i +=
         2) {
 
     for (@LOC("THIS,LayerIIIDecoder.BR,BitReserve.BIT") int i = 0; i < (si.ch[ch].gr[gr].big_values << 1); i +=
         2) {
 


@@ -1103,6 +1105,7 @@ final class LayerIIIDecoder implements FrameDecoder {
     // h = huffcodetab.ht[si.ch[ch].gr[gr].count1table_select + 32];
     num_bits = br.hsstell();
 
     // h = huffcodetab.ht[si.ch[ch].gr[gr].count1table_select + 32];
     num_bits = br.hsstell();
 

+    TERMINATE:

     while ((num_bits < part2_3_end) && (index < 576)) {
 
       huffcodetab.huffman_decoder(htIdx, x, y, v, w, br);
     while ((num_bits < part2_3_end) && (index < 576)) {
 
       huffcodetab.huffman_decoder(htIdx, x, y, v, w, br);


@@ -1497,11 +1500,12 @@ final class LayerIIIDecoder implements FrameDecoder {
             for (@LOC("THIS,LayerIIIDecoder.RO1") int j = 0; j < 3; j++) {
               @LOC("THIS,LayerIIIDecoder.RO1") int sfbcnt;
               sfbcnt = 2;
             for (@LOC("THIS,LayerIIIDecoder.RO1") int j = 0; j < 3; j++) {
               @LOC("THIS,LayerIIIDecoder.RO1") int sfbcnt;
               sfbcnt = 2;

+              TERMINATE:

               for (sfb = 12; sfb >= 3; sfb--) {
                 i = sfBandIndex[sfreq].s[sfb];
                 lines = sfBandIndex[sfreq].s[sfb + 1] - i;
                 i = (i << 2) - i + (j + 1) * lines - 1;
               for (sfb = 12; sfb >= 3; sfb--) {
                 i = sfBandIndex[sfreq].s[sfb];
                 lines = sfBandIndex[sfreq].s[sfb + 1] - i;
                 i = (i << 2) - i + (j + 1) * lines - 1;

-
+                TERMINATE:

                 while (lines > 0) {
                   if (ro[1][i / 18][i % 18] != 0.0f) {
                     // MDM: in java, array access is very slow.
                 while (lines > 0) {
                   if (ro[1][i / 18][i % 18] != 0.0f) {
                     // MDM: in java, array access is very slow.


@@ -1528,6 +1532,7 @@ final class LayerIIIDecoder implements FrameDecoder {
                 sb = sfBandIndex[sfreq].s[sfb + 1] - temp;
                 i = (temp << 2) - temp + j * sb;
 
                 sb = sfBandIndex[sfreq].s[sfb + 1] - temp;
                 i = (temp << 2) - temp + j * sb;
 

+                TERMINATE:

                 for (; sb > 0; sb--) {
                   is_pos[i] = scalefac[1].s[j][sfb];
                   if (is_pos[i] != 7)
                 for (; sb > 0; sb--) {
                   is_pos[i] = scalefac[1].s[j][sfb];
                   if (is_pos[i] != 7)


@@ -1546,7 +1551,7 @@ final class LayerIIIDecoder implements FrameDecoder {
               temp = sfBandIndex[sfreq].s[11];
               sb = sfBandIndex[sfreq].s[12] - temp;
               i = (temp << 2) - temp + j * sb;
               temp = sfBandIndex[sfreq].s[11];
               sb = sfBandIndex[sfreq].s[12] - temp;
               i = (temp << 2) - temp + j * sb;

-
+              TERMINATE:

               for (; sb > 0; sb--) {
                 is_pos[i] = is_pos[sfb];
 
               for (; sb > 0; sb--) {
                 is_pos[i] = is_pos[sfb];
 


@@ -1563,6 +1568,7 @@ final class LayerIIIDecoder implements FrameDecoder {
               i = 2;
               ss = 17;
               sb = -1;
               i = 2;
               ss = 17;
               sb = -1;

+              TERMINATE:

               while (i >= 0) {
                 if (ro[1][i][ss] != 0.0f) {
                   sb = (i << 4) + (i << 1) + ss;
               while (i >= 0) {
                 if (ro[1][i][ss] != 0.0f) {
                   sb = (i << 4) + (i << 1) + ss;


@@ -1582,6 +1588,7 @@ final class LayerIIIDecoder implements FrameDecoder {
               i = sfBandIndex[sfreq].l[i];
               for (; sfb < 8; sfb++) {
                 sb = sfBandIndex[sfreq].l[sfb + 1] - sfBandIndex[sfreq].l[sfb];
               i = sfBandIndex[sfreq].l[i];
               for (; sfb < 8; sfb++) {
                 sb = sfBandIndex[sfreq].l[sfb + 1] - sfBandIndex[sfreq].l[sfb];

+                TERMINATE:

                 for (; sb > 0; sb--) {
                   is_pos[i] = scalefac[1].l[sfb];
                   if (is_pos[i] != 7)
                 for (; sb > 0; sb--) {
                   is_pos[i] = scalefac[1].l[sfb];
                   if (is_pos[i] != 7)


@@ -1597,11 +1604,12 @@ final class LayerIIIDecoder implements FrameDecoder {
             for (@LOC("THIS,LayerIIIDecoder.RO1") int j = 0; j < 3; j++) {
               @LOC("THIS,LayerIIIDecoder.RO1") int sfbcnt;
               sfbcnt = -1;
             for (@LOC("THIS,LayerIIIDecoder.RO1") int j = 0; j < 3; j++) {
               @LOC("THIS,LayerIIIDecoder.RO1") int sfbcnt;
               sfbcnt = -1;

+              TERMINATE:

               for (sfb = 12; sfb >= 0; sfb--) {
                 temp = sfBandIndex[sfreq].s[sfb];
                 lines = sfBandIndex[sfreq].s[sfb + 1] - temp;
                 i = (temp << 2) - temp + (j + 1) * lines - 1;
               for (sfb = 12; sfb >= 0; sfb--) {
                 temp = sfBandIndex[sfreq].s[sfb];
                 lines = sfBandIndex[sfreq].s[sfb + 1] - temp;
                 i = (temp << 2) - temp + (j + 1) * lines - 1;

-
+                TERMINATE:

                 while (lines > 0) {
                   if (ro[1][i / 18][i % 18] != 0.0f) {
                     // MDM: in java, array access is very slow.
                 while (lines > 0) {
                   if (ro[1][i / 18][i % 18] != 0.0f) {
                     // MDM: in java, array access is very slow.


@@ -1621,6 +1629,7 @@ final class LayerIIIDecoder implements FrameDecoder {
                 temp = sfBandIndex[sfreq].s[sfb];
                 sb = sfBandIndex[sfreq].s[sfb + 1] - temp;
                 i = (temp << 2) - temp + j * sb;
                 temp = sfBandIndex[sfreq].s[sfb];
                 sb = sfBandIndex[sfreq].s[sfb + 1] - temp;
                 i = (temp << 2) - temp + j * sb;

+                TERMINATE:

                 for (; sb > 0; sb--) {
                   is_pos[i] = scalefac[1].s[j][sfb];
                   if (is_pos[i] != 7)
                 for (; sb > 0; sb--) {
                   is_pos[i] = scalefac[1].s[j][sfb];
                   if (is_pos[i] != 7)


@@ -1639,7 +1648,7 @@ final class LayerIIIDecoder implements FrameDecoder {
               sfb = (temp << 2) - temp + j * sb;
               sb = sfBandIndex[sfreq].s[12] - temp2;
               i = (temp2 << 2) - temp2 + j * sb;
               sfb = (temp << 2) - temp + j * sb;
               sb = sfBandIndex[sfreq].s[12] - temp2;
               i = (temp2 << 2) - temp2 + j * sb;

-
+              TERMINATE:

               for (; sb > 0; sb--) {
                 is_pos[i] = is_pos[sfb];
 
               for (; sb > 0; sb--) {
                 is_pos[i] = is_pos[sfb];
 


@@ -1657,6 +1666,7 @@ final class LayerIIIDecoder implements FrameDecoder {
           i = 31;
           ss = 17;
           sb = 0;
           i = 31;
           ss = 17;
           sb = 0;

+          TERMINATE:

           while (i >= 0) {
             if (ro[1][i][ss] != 0.0f) {
               sb = (i << 4) + (i << 1) + ss;
           while (i >= 0) {
             if (ro[1][i][ss] != 0.0f) {
               sb = (i << 4) + (i << 1) + ss;


@@ -1677,6 +1687,7 @@ final class LayerIIIDecoder implements FrameDecoder {
           i = sfBandIndex[sfreq].l[i];
           for (; sfb < 21; sfb++) {
             sb = sfBandIndex[sfreq].l[sfb + 1] - sfBandIndex[sfreq].l[sfb];
           i = sfBandIndex[sfreq].l[i];
           for (; sfb < 21; sfb++) {
             sb = sfBandIndex[sfreq].l[sfb + 1] - sfBandIndex[sfreq].l[sfb];

+            TERMINATE:

             for (; sb > 0; sb--) {
               is_pos[i] = scalefac[1].l[sfb];
               if (is_pos[i] != 7)
             for (; sb > 0; sb--) {
               is_pos[i] = scalefac[1].l[sfb];
               if (is_pos[i] != 7)


@@ -1688,6 +1699,7 @@ final class LayerIIIDecoder implements FrameDecoder {
             }
           }
           sfb = sfBandIndex[sfreq].l[20];
             }
           }
           sfb = sfBandIndex[sfreq].l[20];

+          TERMINATE:

           for (sb = 576 - sfBandIndex[sfreq].l[21]; (sb > 0) && (i < 576); sb--) {
             is_pos[i] = is_pos[sfb]; // error here : i >=576
 
           for (sb = 576 - sfBandIndex[sfreq].l[21]; (sb > 0) && (i < 576); sb--) {
             is_pos[i] = is_pos[sfb]; // error here : i >=576