update location identifier according to changes of class structure

diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java
index 031113ff2d49dac990f614c39c5a5aeb8c835d95..3936ca16d5e2505fbc0c68942929e331ca864739 100644 (file)
--- a/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java
+++ b/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java
@@ -667,7 +667,7 @@ final class LayerIIIDecoder implements FrameDecoder {
   @LATTICE("OUT<THIS,THIS<C,C<IN,C*,THISLOC=THIS,RETURNLOC=OUT")
   private boolean get_side_info(@LOC("THIS,LayerIIIDecoder.HD1") Header header) {
 
-    @LOC("THIS,LayerIIIDecoder.SI,LayerIIIDecoder$III_side_info_t.TEMP") SideInfoBuffer sib =
+    @LOC("THIS,LayerIIIDecoder.SI,III_side_info_t.TEMP") SideInfoBuffer sib =
         header.getSideInfoBuffer();
     @LOC("THIS,LayerIIIDecoder.SF1") int version = header.version();
 
@@ -699,7 +699,7 @@ final class LayerIIIDecoder implements FrameDecoder {
           si.ch[ch].gr[gr].big_values = sib.get_bits(9);
           si.ch[ch].gr[gr].global_gain = sib.get_bits(8);
           si.ch[ch].gr[gr].scalefac_compress = sib.get_bits(4);
-          @LOC("THIS,LayerIIIDecoder.SI,LayerIIIDecoder$III_side_info_t.TEMP") int cond =
+          @LOC("THIS,LayerIIIDecoder.SI,III_side_info_t.TEMP") int cond =
               sib.get_bits(1);
           // si.ch[ch].gr[gr].window_switching_flag = sib.get_bits(1);
           // if ((si.ch[ch].gr[gr].window_switching_flag) != 0) {
@@ -758,7 +758,7 @@ final class LayerIIIDecoder implements FrameDecoder {
         si.ch[ch].gr[0].global_gain = sib.get_bits(8);
         si.ch[ch].gr[0].scalefac_compress = sib.get_bits(9);
 
-        @LOC("THIS,LayerIIIDecoder.SI,LayerIIIDecoder$III_side_info_t.TEMP") int cond =
+        @LOC("THIS,LayerIIIDecoder.SI,III_side_info_t.TEMP") int cond =
             sib.get_bits(1);
         // si.ch[ch].gr[0].window_switching_flag = sib.get_bits(1);
         // if ((si.ch[ch].gr[0].window_switching_flag) != 0) {
@@ -930,13 +930,13 @@ final class LayerIIIDecoder implements FrameDecoder {
     // @LOC("THIS,LayerIIIDecoder.GLSFD1") gr_info_s gr_info =
     // (si.ch[ch].gr[gr]); // remove alias
 
-    @LOC("THIS,LayerIIIDecoder.SI,LayerIIIDecoder$III_side_info_t.CH,LayerIIIDecoder$temporaire.GR,LayerIIIDecoder$gr_info_s.V") int scalefac_comp =
+    @LOC("THIS,LayerIIIDecoder.SI,III_side_info_t.CH,temporaire.GR,gr_info_s.V") int scalefac_comp =
         si.ch[ch].gr[gr].scalefac_compress;
     @LOC("THIS,LayerIIIDecoder.NS") int blocktypenumber;
 
-    @LOC("THIS,LayerIIIDecoder.SI,LayerIIIDecoder$III_side_info_t.CH,LayerIIIDecoder$temporaire.GR,LayerIIIDecoder$gr_info_s.V") int int_scalefac_comp;
+    @LOC("THIS,LayerIIIDecoder.SI,III_side_info_t.CH,temporaire.GR,gr_info_s.V") int int_scalefac_comp;
     @LOC("THIS,LayerIIIDecoder.SFB_SH") int m;
-    @LOC("THIS,LayerIIIDecoder.SI,LayerIIIDecoder$III_side_info_t.CH,LayerIIIDecoder$temporaire.GR,LayerIIIDecoder$gr_info_s.V") int blocknumber =
+    @LOC("THIS,LayerIIIDecoder.SI,III_side_info_t.CH,temporaire.GR,gr_info_s.V") int blocknumber =
         0;
 
     if (si.ch[ch].gr[gr].block_type == 2) {
@@ -1803,11 +1803,11 @@ final class LayerIIIDecoder implements FrameDecoder {
   private void antialias(@LOC("THIS,LayerIIIDecoder.SI") int ch,
       @LOC("THIS,LayerIIIDecoder.SI") int gr) {
 
-    @LOC("THIS,LayerIIIDecoder.SI,LayerIIIDecoder$III_side_info_t.CH,LayerIIIDecoder$temporaire.GR2") int sb18;
+    @LOC("THIS,LayerIIIDecoder.SI,III_side_info_t.CH,temporaire.GR2") int sb18;
     @LOC("THIS,LayerIIIDecoder.SI1") int ss;
-    @LOC("THIS,LayerIIIDecoder.SI,LayerIIIDecoder$III_side_info_t.CH,LayerIIIDecoder$temporaire.GR2") int sb18lim;
+    @LOC("THIS,LayerIIIDecoder.SI,III_side_info_t.CH,temporaire.GR2") int sb18lim;
 
-    // @LOC("THIS,LayerIIIDecoder.SI,LayerIIIDecoder$III_side_info_t.CH,LayerIIIDecoder$temporaire.GR1")
+    // @LOC("THIS,LayerIIIDecoder.SI,III_side_info_t.CH,temporaire.GR1")
     // gr_info_s gr_info =
     // (si.ch[ch].gr[gr]);
     // 31 alias-reduction operations between each pair of sub-bands
@@ -1817,6 +1817,7 @@ final class LayerIIIDecoder implements FrameDecoder {
         && !(si.ch[ch].gr[gr].mixed_block_flag != 0))
       return;
 
+     
     if ((si.ch[ch].gr[gr].window_switching_flag != 0) && (si.ch[ch].gr[gr].mixed_block_flag != 0)
         && (si.ch[ch].gr[gr].block_type == 2)) {
       sb18lim = 18;

diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/Player.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/Player.java
index a19768ec23fdb5a5147e6ccae26a826337885dec..7268b1d94f09e941c25c6698486bfe1dee5e289c 100644 (file)
--- a/Robust/src/Benchmarks/SSJava/MP3Decoder/Player.java
+++ b/Robust/src/Benchmarks/SSJava/MP3Decoder/Player.java
@@ -71,10 +71,9 @@ public class Player {
   @LOC("B")\r
   private int lastPosition = 0;\r
 \r
-\r
+  @LOC("B")\r
   private long sampleNumber;\r
 \r
-\r
   /**\r
    * Creates a new <code>Player</code> instance.\r
    */\r
@@ -122,7 +121,7 @@ public class Player {
     decoder.init(h);\r
 \r
     sampleNumber = 1;\r
-    System.out.println( "Gobble sentinel: +++" );\r
+    System.out.println("Gobble sentinel: +++");\r
 \r
     @LOC("IN") int count = 0;\r
     SSJAVA: while (count++ < 2147483646) {\r
@@ -185,7 +184,6 @@ public class Player {
     return 0;\r
   }\r
 \r
-\r
   /**\r
    * Decodes a single frame.\r
    * \r
@@ -208,16 +206,7 @@ public class Player {
       // @LOC("O") SampleBuffer output = (SampleBuffer) decoder.decodeFrame(h);\r
       decoder.decodeFrame(h);\r
 \r
-      // it looks like there is left and right channel interleaved into the\r
-      // output buffer, so only sample one channel (stride=2)\r
-      short[] outbuf = SampleBufferWrapper.getBuffer();\r
-      TERMINATE: for (@LOC("C") int i = 0; i < SampleBufferWrapper.getBufferLength(); i = i + 2) {\r
-        System.out.println( sampleNumber+" "+outbuf[i] );\r
-        sampleNumber++;\r
-      }\r
-\r
-\r
-\r
+      DEBUG_OUTPUT();\r
       // synchronized (this)\r
       // {\r
       // out = audio;\r
@@ -243,4 +232,15 @@ public class Player {
     return true;\r
   }\r
 \r
+  @TRUST\r
+  public void DEBUG_OUTPUT() {\r
+    // it looks like there is left and right channel interleaved into the\r
+    // output buffer, so only sample one channel (stride=2)\r
+    short[] outbuf = SampleBufferWrapper.getBuffer();\r
+    for (int i = 0; i < SampleBufferWrapper.getBufferLength(); i = i + 2) {\r
+      System.out.println(sampleNumber + " " + outbuf[i]);\r
+      sampleNumber++;\r
+    }\r
+  }\r
+\r
 }\r