From: yeom <yeom>
Date: Thu, 18 Aug 2011 01:50:57 +0000 (+0000)
Subject: changes.
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=IRC.git;a=commitdiff_plain;h=228b915898f49d8496fb35619969d2917a17a4e1

changes.
---

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 9d41b838..5b458dc6 100644
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -292,12 +292,14 @@ public class FlowDownCheck {
   private void checkDeclarationInMethodBody(ClassDescriptor cd, MethodDescriptor md) {
     BlockNode bn = state.getMethodBody(md);
 
+    System.out.println("\n#checkDeclarationInMethodBody=" + md);
+
     // first, check annotations on method parameters
     List<CompositeLocation> paramList = new ArrayList<CompositeLocation>();
     for (int i = 0; i < md.numParameters(); i++) {
       // process annotations on method parameters
       VarDescriptor vd = (VarDescriptor) md.getParameter(i);
-      assignLocationOfVarDescriptor(vd, md, md.getParameterTable(), bn);
+      assignLocationOfVarDescriptor(vd, md, md.getParameterTable(), null);
       paramList.add(d2loc.get(vd));
     }
     Vector<AnnotationDescriptor> methodAnnotations = md.getModifiers().getAnnotations();
@@ -323,7 +325,9 @@ public class FlowDownCheck {
         // if developer does not define method lattice
         // search return location in the method default lattice
         String rtrStr = ssjava.getMethodLattice(md).getReturnLoc();
-        returnLocComp = new CompositeLocation(new Location(md, rtrStr));
+        if(rtrStr!=null){
+          returnLocComp = new CompositeLocation(new Location(md, rtrStr));
+        }        
       }
 
       if (returnLocComp == null) {
@@ -345,6 +349,7 @@ public class FlowDownCheck {
 
       System.out.println("### ReturnLocGenerator=" + md);
       System.out.println("### md2ReturnLoc.get(md)=" + md2ReturnLoc.get(md));
+
       md2ReturnLocGen.put(md, new ReturnLocGenerator(md2ReturnLoc.get(md), md, paramList, md
           + " of " + cd.getSourceFileName()));
     }
@@ -1469,8 +1474,8 @@ public class FlowDownCheck {
 
     // currently enforce every variable to have corresponding location
     if (annotationVec.size() == 0) {
-      throw new Error("Location is not assigned to variable " + vd.getSymbol() + " in the method "
-          + md.getSymbol() + " of the class " + cd.getSymbol());
+      throw new Error("Location is not assigned to variable '" + vd.getSymbol() + "' in the method '"
+          + md + "' of the class " + cd.getSymbol() + " at " + generateErrorMessage(cd, n));
     }
 
     if (annotationVec.size() > 1) { // variable can have at most one location
diff --git a/Robust/src/ClassLibrary/SSJava/Character.java b/Robust/src/ClassLibrary/SSJava/Character.java
index 3e412818..edff16e4 100644
--- a/Robust/src/ClassLibrary/SSJava/Character.java
+++ b/Robust/src/ClassLibrary/SSJava/Character.java
@@ -1,3 +1,4 @@
+@LATTICE("VALUE")
 public class Character {
 
   public static int digit(char ch, int radix) {
@@ -24,7 +25,7 @@ public class Character {
       return false;
   }
 
-  char value;
+  @LOC("VALUE") char value;
 
   public Character(char c) {
     value = c;
@@ -34,6 +35,7 @@ public class Character {
     value = c.value;
   }
 
+  @LATTICE("OUT<THIS,RETURNLOC=OUT,THISLOC=THIS")
   public String toString() {
     return ""+value;
   }
diff --git a/Robust/src/ClassLibrary/SSJava/Integer.java b/Robust/src/ClassLibrary/SSJava/Integer.java
index 7c51d4ed..fac6d36d 100644
--- a/Robust/src/ClassLibrary/SSJava/Integer.java
+++ b/Robust/src/ClassLibrary/SSJava/Integer.java
@@ -95,8 +95,8 @@ public class Integer {
   }
   
   @RETURNLOC("V")
-  public static String toString(int i) {
-    Integer I = new Integer(i);
+  public static String toString(@LOC("IN") int i) {
+   @LOC("C") Integer I = new Integer(i);
     return I.toString();
   }
 
diff --git a/Robust/src/ClassLibrary/SSJava/Long.java b/Robust/src/ClassLibrary/SSJava/Long.java
index b53033bb..49afdba5 100644
--- a/Robust/src/ClassLibrary/SSJava/Long.java
+++ b/Robust/src/ClassLibrary/SSJava/Long.java
@@ -55,6 +55,8 @@ exception statement from your version. */
  * @since 1.0
  * @status updated to 1.5
  */
+@LATTICE("V<C, V<O")
+@METHODDEFAULT("O<V,V<C,C<IN,C*,THISLOC=IN,RETURNLOC=O")
 public final class Long //extends Number implements Comparable<Long>
 {
   /**
@@ -104,7 +106,7 @@ public final class Long //extends Number implements Comparable<Long>
    *
    * @serial the wrapped long
    */
-  private final long value;
+  @LOC("V") private final long value;
 
   /**
    * Create a <code>Long</code> object representing the value of the
diff --git a/Robust/src/ClassLibrary/SSJava/String.java b/Robust/src/ClassLibrary/SSJava/String.java
index 7bbb303b..b0fc9c0f 100644
--- a/Robust/src/ClassLibrary/SSJava/String.java
+++ b/Robust/src/ClassLibrary/SSJava/String.java
@@ -1,9 +1,19 @@
 import Vector;
 
+@LATTICE("V<C, V<O")
+@METHODDEFAULT("O<V,V<C,C<IN,C*,THISLOC=O,RETURNLOC=O")
 public class String {
+
+  @LOC("V")
   char value[];
+
+  @LOC("C")
   int count;
+
+  @LOC("O")
   int offset;
+
+  @LOC("V")
   private int cachedHashcode;
 
   private String() {
@@ -16,76 +26,75 @@ public class String {
   }
 
   public String(char str[]) {
-    char charstr[]=new char[str.length];
-    for(int i=0; i<str.length; i++)
-      charstr[i]=str[i];
-    this.value=charstr;
-    this.count=str.length;
-    this.offset=0;
+    char charstr[] = new char[str.length];
+    for (int i = 0; i < str.length; i++)
+      charstr[i] = str[i];
+    this.value = charstr;
+    this.count = str.length;
+    this.offset = 0;
   }
 
   public String(byte str[]) {
-    char charstr[]=new char[str.length];
-    for(int i=0; i<str.length; i++)
-      charstr[i]=(char)str[i];
-    this.value=charstr;
-    this.count=str.length;
-    this.offset=0;
+    char charstr[] = new char[str.length];
+    for (int i = 0; i < str.length; i++)
+      charstr[i] = (char) str[i];
+    this.value = charstr;
+    this.count = str.length;
+    this.offset = 0;
   }
 
   public String(byte str[], int offset, int length) {
-    if (length>(str.length-offset))
-      length=str.length-offset;
-    char charstr[]=new char[length];
-    for(int i=0; i<length; i++)
-      charstr[i]=(char)str[i+offset];
-    this.value=charstr;
-    this.count=length;
-    this.offset=0;
+    if (length > (str.length - offset))
+      length = str.length - offset;
+    char charstr[] = new char[length];
+    for (int i = 0; i < length; i++)
+      charstr[i] = (char) str[i + offset];
+    this.value = charstr;
+    this.count = length;
+    this.offset = 0;
   }
 
   public String(byte str[], String encoding) {
     int length = this.count;
-    if (length>(str.length))
-      length=str.length;
-    char charstr[]=new char[length];
-    for(int i=0; i<length; i++)
-      charstr[i]=(char)str[i];
-    this.value=charstr;
-    this.count=length;
-    this.offset=0;
+    if (length > (str.length))
+      length = str.length;
+    char charstr[] = new char[length];
+    for (int i = 0; i < length; i++)
+      charstr[i] = (char) str[i];
+    this.value = charstr;
+    this.count = length;
+    this.offset = 0;
   }
 
   public String(char str[], int offset, int length) {
-    if (length>(str.length-offset))
-      length=str.length-offset;
-    char charstr[]=new char[length];
-    for(int i=0; i<length; i++)
-      charstr[i]=str[i+offset];
-    this.value=charstr;
-    this.count=length;
-    this.offset=0;
+    if (length > (str.length - offset))
+      length = str.length - offset;
+    char charstr[] = new char[length];
+    for (int i = 0; i < length; i++)
+      charstr[i] = str[i + offset];
+    this.value = charstr;
+    this.count = length;
+    this.offset = 0;
   }
 
   public String(String str) {
-    this.value=str.value;
-    this.count=str.count;
-    this.offset=str.offset;
+    this.value = str.value;
+    this.count = str.count;
+    this.offset = str.offset;
   }
 
   public String(StringBuffer strbuf) {
-    value=new char[strbuf.length()];
-    count=strbuf.length();
-    offset=0;
-    for(int i=0; i<count; i++)
-      value[i]=strbuf.value[i];
+    value = new char[strbuf.length()];
+    count = strbuf.length();
+    offset = 0;
+    for (int i = 0; i < count; i++)
+      value[i] = strbuf.value[i];
   }
 
   public boolean endsWith(String suffix) {
     return regionMatches(count - suffix.count, suffix, 0, suffix.count);
   }
 
-
   public String substring(int beginIndex) {
     return substring(beginIndex, this.count);
   }
@@ -95,14 +104,14 @@ public class String {
   }
 
   public String substring(int beginIndex, int endIndex) {
-    String str=new String();
-    if (beginIndex>this.count||endIndex>this.count||beginIndex>endIndex) {
+    String str = new String();
+    if (beginIndex > this.count || endIndex > this.count || beginIndex > endIndex) {
       // FIXME
-      System.printString("Index error: "+beginIndex+" "+endIndex+" "+count+"\n"+this);
+      System.printString("Index error: " + beginIndex + " " + endIndex + " " + count + "\n" + this);
     }
-    str.value=this.value;
-    str.count=endIndex-beginIndex;
-    str.offset=this.offset+beginIndex;
+    str.value = this.value;
+    str.count = endIndex - beginIndex;
+    str.offset = this.offset + beginIndex;
     return str;
   }
 
@@ -115,69 +124,69 @@ public class String {
   }
 
   public int lastIndexOf(char ch) {
-    return this.lastindexOf((int)ch, count - 1);
+    return this.lastindexOf((int) ch, count - 1);
   }
 
   public static String concat2(String s1, String s2) {
-    if (s1==null)
+    if (s1 == null)
       return "null".concat(s2);
     else
       return s1.concat(s2);
   }
 
   public String concat(String str) {
-    String newstr=new String();
-    newstr.count=this.count+str.count;
-    char charstr[]=new char[newstr.count];
-    newstr.offset=0;
-    for(int i=0; i<count; i++) {
-      charstr[i]=value[i+offset];
+    String newstr = new String();
+    newstr.count = this.count + str.count;
+    char charstr[] = new char[newstr.count];
+    newstr.offset = 0;
+    for (int i = 0; i < count; i++) {
+      charstr[i] = value[i + offset];
     }
-    for(int i=0; i<str.count; i++) {
-      charstr[i+count]=str.value[i+str.offset];
+    for (int i = 0; i < str.count; i++) {
+      charstr[i + count] = str.value[i + str.offset];
     }
-    newstr.value=charstr;
+    newstr.value = charstr;
     return newstr;
   }
 
   public int lastindexOf(int ch, int fromIndex) {
-    for(int i=fromIndex; i>0; i--)
-      if (this.charAt(i)==ch)
+    for (int i = fromIndex; i > 0; i--)
+      if (this.charAt(i) == ch)
         return i;
     return -1;
   }
 
   public String replace(char oldch, char newch) {
-    char[] buffer=new char[count];
-    for(int i=0; i<count; i++) {
-      char x=charAt(i);
-      if (x==oldch)
-        x=newch;
-      buffer[i]=x;
+    char[] buffer = new char[count];
+    for (int i = 0; i < count; i++) {
+      char x = charAt(i);
+      if (x == oldch)
+        x = newch;
+      buffer[i] = x;
     }
     return new String(buffer);
   }
 
   public String toUpperCase() {
-    char[] buffer=new char[count];
-    for(int i=0; i<count; i++) {
-      char x=charAt(i);
-      if (x>='a'&&x<='z') {
-        x=(char) ((x-'a')+'A');
+    char[] buffer = new char[count];
+    for (int i = 0; i < count; i++) {
+      char x = charAt(i);
+      if (x >= 'a' && x <= 'z') {
+        x = (char) ((x - 'a') + 'A');
       }
-      buffer[i]=x;
+      buffer[i] = x;
     }
     return new String(buffer);
   }
 
   public String toLowerCase() {
-    char[] buffer=new char[count];
-    for(int i=0; i<count; i++) {
-      char x=charAt(i);
-      if (x>='A'&&x<='Z') {
-        x=(char) ((x-'A')+'a');
+    char[] buffer = new char[count];
+    for (int i = 0; i < count; i++) {
+      char x = charAt(i);
+      if (x >= 'A' && x <= 'Z') {
+        x = (char) ((x - 'A') + 'a');
       }
-      buffer[i]=x;
+      buffer[i] = x;
     }
     return new String(buffer);
   }
@@ -187,8 +196,8 @@ public class String {
   }
 
   public int indexOf(int ch, int fromIndex) {
-    for(int i=fromIndex; i<count; i++)
-      if (this.charAt(i)==ch)
+    for (int i = fromIndex; i < count; i++)
+      if (this.charAt(i) == ch)
         return i;
     return -1;
   }
@@ -198,9 +207,9 @@ public class String {
   }
 
   public int indexOf(String str, int fromIndex) {
-    if (fromIndex<0)
-      fromIndex=0;
-    for(int i=fromIndex; i<=(count-str.count); i++)
+    if (fromIndex < 0)
+      fromIndex = 0;
+    for (int i = fromIndex; i <= (count - str.count); i++)
       if (regionMatches(i, str, 0, str.count))
         return i;
     return -1;
@@ -212,10 +221,10 @@ public class String {
   }
 
   public int lastIndexOf(String str, int fromIndex) {
-    int k=count-str.count;
-    if (k>fromIndex)
-      k=fromIndex;
-    for(; k>=0; k--) {
+    int k = count - str.count;
+    if (k > fromIndex)
+      k = fromIndex;
+    for (; k >= 0; k--) {
       if (regionMatches(k, str, 0, str.count))
         return k;
     }
@@ -223,7 +232,7 @@ public class String {
   }
 
   public int lastIndexOf(String str) {
-    return lastIndexOf(str, count-str.count);
+    return lastIndexOf(str, count - str.count);
   }
 
   public boolean startsWith(String str) {
@@ -235,26 +244,25 @@ public class String {
   }
 
   public boolean regionMatches(int toffset, String other, int ooffset, int len) {
-    if (toffset<0 || ooffset <0 || (toffset+len)>count || (ooffset+len)>other.count)
+    if (toffset < 0 || ooffset < 0 || (toffset + len) > count || (ooffset + len) > other.count)
       return false;
-    for(int i=0; i<len; i++)
-      if (other.value[i+other.offset+ooffset]!=
-          this.value[i+this.offset+toffset])
+    for (int i = 0; i < len; i++)
+      if (other.value[i + other.offset + ooffset] != this.value[i + this.offset + toffset])
         return false;
     return true;
   }
 
   public char[] toCharArray() {
-    char str[]=new char[count];
-    for(int i=0; i<count; i++)
-      str[i]=value[i+offset];
+    char str[] = new char[count];
+    for (int i = 0; i < count; i++)
+      str[i] = value[i + offset];
     return str;
   }
 
   public byte[] getBytes() {
-    byte str[]=new byte[count];
-    for(int i=0; i<count; i++)
-      str[i]=(byte)value[i+offset];
+    byte str[] = new byte[count];
+    for (int i = 0; i < count; i++)
+      str[i] = (byte) value[i + offset];
     return str;
   }
 
@@ -263,15 +271,15 @@ public class String {
   }
 
   public void getChars(int srcBegin, int srcEnd, char dst[], int dstBegin) {
-    if((srcBegin < 0) || (srcEnd > count) || (srcBegin > srcEnd)) {
+    if ((srcBegin < 0) || (srcEnd > count) || (srcBegin > srcEnd)) {
       // FIXME
-      System.printString("Index error: "+srcBegin+" "+srcEnd+" "+count+"\n"+this);
+      System.printString("Index error: " + srcBegin + " " + srcEnd + " " + count + "\n" + this);
       System.exit(-1);
     }
     int len = srcEnd - srcBegin;
     int j = dstBegin;
-    for(int i=srcBegin; i<srcEnd; i++)
-      dst[j++]=value[i+offset];
+    for (int i = srcBegin; i < srcEnd; i++)
+      dst[j++] = value[i + offset];
     return;
   }
 
@@ -280,15 +288,15 @@ public class String {
   }
 
   public char charAt(int i) {
-    return value[i+offset];
+    return value[i + offset];
   }
 
   public String toString() {
     return this;
   }
 
-  public static String valueOf(Object o) {
-    if (o==null)
+  public static String valueOf(@LOC("IN") Object o) {
+    if (o == null)
       return "null";
     else
       return o.toString();
@@ -301,133 +309,133 @@ public class String {
       return new String("false");
   }
 
-  public static String valueOf(char c) {
-    char ar[]=new char[1];
-    ar[0]=c;
+  public static String valueOf(@LOC("IN") char c) {
+    @LOC("C") char ar[] = new char[1];
+    ar[0] = c;
     return new String(ar);
   }
 
-  public static String valueOf(int x) {
-    int length=0;
-    int tmp;
-    if (x<0)
-      tmp=-x;
+  public static String valueOf(@LOC("IN") int x) {
+    @LOC("C") int length = 0;
+    @LOC("C") int tmp;
+    if (x < 0)
+      tmp = -x;
     else
-      tmp=x;
+      tmp = x;
     do {
-      tmp=tmp/10;
-      length=length+1;
-    } while(tmp!=0);
+      tmp = tmp / 10;
+      length = length + 1;
+    } while (tmp != 0);
 
-    char chararray[];
-    if (x<0)
-      chararray=new char[length+1];
+    @LOC("C") char chararray[];
+    if (x < 0)
+      chararray = new char[length + 1];
     else
-      chararray=new char[length];
-    int voffset;
-    if (x<0) {
-      chararray[0]='-';
-      voffset=1;
-      x=-x;
+      chararray = new char[length];
+    @LOC("C") int voffset;
+    if (x < 0) {
+      chararray[0] = '-';
+      voffset = 1;
+      x = -x;
     } else
-      voffset=0;
+      voffset = 0;
 
     do {
-      chararray[--length+voffset]=(char)(x%10+'0');
-      x=x/10;
-    } while (length!=0);
+      chararray[--length + voffset] = (char) (x % 10 + '0');
+      x = x / 10;
+    } while (length != 0);
     return new String(chararray);
   }
 
   public static String valueOf(double val) {
-    char[] chararray=new char[20];
-    String s=new String();
-    s.offset=0;
-    s.count=convertdoubletochar(val, chararray);
-    s.value=chararray;
+    char[] chararray = new char[20];
+    String s = new String();
+    s.offset = 0;
+    s.count = convertdoubletochar(val, chararray);
+    s.value = chararray;
     return s;
   }
 
-  public static native int convertdoubletochar(double val, char [] chararray);
+  public static native int convertdoubletochar(double val, char[] chararray);
 
-  public static String valueOf(long x) {
-    int length=0;
-    long tmp;
-    if (x<0)
-      tmp=-x;
+  public static String valueOf(@LOC("IN") long x) {
+    @LOC("C") int length = 0;
+    @LOC("C") long tmp;
+    if (x < 0)
+      tmp = -x;
     else
-      tmp=x;
+      tmp = x;
     do {
-      tmp=tmp/10;
-      length=length+1;
-    } while(tmp!=0);
+      tmp = tmp / 10;
+      length = length + 1;
+    } while (tmp != 0);
 
-    char chararray[];
-    if (x<0)
-      chararray=new char[length+1];
+    @LOC("C") char chararray[];
+    if (x < 0)
+      chararray = new char[length + 1];
     else
-      chararray=new char[length];
-    int voffset;
-    if (x<0) {
-      chararray[0]='-';
-      voffset=1;
-      x=-x;
+      chararray = new char[length];
+    @LOC("C") int voffset;
+    if (x < 0) {
+      chararray[0] = '-';
+      voffset = 1;
+      x = -x;
     } else
-      voffset=0;
+      voffset = 0;
 
     do {
-      chararray[--length+voffset]=(char)(x%10+'0');
-      x=x/10;
-    } while (length!=0);
+      chararray[--length + voffset] = (char) (x % 10 + '0');
+      x = x / 10;
+    } while (length != 0);
     return new String(chararray);
   }
 
   public int compareTo(String s) {
-    int smallerlength=count<s.count?count:s.count;
+    int smallerlength = count < s.count ? count : s.count;
 
-    for( int i = 0; i < smallerlength; i++ ) {
+    for (int i = 0; i < smallerlength; i++) {
       int valDiff = this.charAt(i) - s.charAt(i);
-      if( valDiff != 0 ) {
+      if (valDiff != 0) {
         return valDiff;
       }
     }
-    return count-s.count;
+    return count - s.count;
   }
 
   public int hashCode() {
-    if (cachedHashcode!=0)
+    if (cachedHashcode != 0)
       return cachedHashcode;
-    int hashcode=0;
-    for(int i=0; i<count; i++)
-      hashcode=hashcode*31+value[i+offset];
-    cachedHashcode=hashcode;
+    @LOC("C") int hashcode = 0;
+    for (@LOC("C") int i = 0; i < count; i++)
+      hashcode = hashcode * 31 + value[i + offset];
+    cachedHashcode = hashcode;
     return hashcode;
   }
 
   public boolean equals(Object o) {
-    if (o.getType()!=getType())
+    if (o.getType() != getType())
       return false;
-    String s=(String)o;
-    if (s.count!=count)
+    String s = (String) o;
+    if (s.count != count)
       return false;
-    for(int i=0; i<count; i++) {
-      if (s.value[i+s.offset]!=value[i+offset])
+    for (int i = 0; i < count; i++) {
+      if (s.value[i + s.offset] != value[i + offset])
         return false;
     }
     return true;
   }
 
   public boolean equalsIgnoreCase(String s) {
-    if (s.count!=count)
+    if (s.count != count)
       return false;
-    for(int i=0; i<count; i++) {
-      char l=s.value[i+s.offset];
-      char r=value[i+offset];
-      if (l>='a'&&l<='z')
-        l=(char)((l-'a')+'A');
-      if (r>='a'&&r<='z')
-        r=(char)((r-'a')+'A');
-      if (l!=r)
+    for (int i = 0; i < count; i++) {
+      char l = s.value[i + s.offset];
+      char r = value[i + offset];
+      if (l >= 'a' && l <= 'z')
+        l = (char) ((l - 'a') + 'A');
+      if (r >= 'a' && r <= 'z')
+        r = (char) ((r - 'a') + 'A');
+      if (l != r)
         return false;
     }
     return true;
@@ -436,39 +444,40 @@ public class String {
   public Vector split() {
     Vector splitted = new Vector();
     int i;
-    int cnt =0;
+    int cnt = 0;
 
     // skip first spaces
-    for(i = 0; i< count; i++) {
-      if(value[i+offset] != '\n' && value[i+offset] != '\t' && value[i+offset] != ' ')
+    for (i = 0; i < count; i++) {
+      if (value[i + offset] != '\n' && value[i + offset] != '\t' && value[i + offset] != ' ')
         break;
     }
 
-    int oldi=i;
+    int oldi = i;
 
-    while(i<count) {
-      if(value[i+offset] == '\n' || value[i+offset] == '\t' || value[i+offset] == ' ') {
-        String t=new String();
-        t.value=value;
-        t.offset=oldi;
-        t.count=i-oldi;
+    while (i < count) {
+      if (value[i + offset] == '\n' || value[i + offset] == '\t' || value[i + offset] == ' ') {
+        String t = new String();
+        t.value = value;
+        t.offset = oldi;
+        t.count = i - oldi;
         splitted.addElement(t);
 
         // skip extra spaces
-        while( i < count && ( value[i+offset] == '\n' || value[i+offset] == '\t' || value[i+offset] == ' ')) {
+        while (i < count
+            && (value[i + offset] == '\n' || value[i + offset] == '\t' || value[i + offset] == ' ')) {
           i++;
         }
-        oldi=i;
+        oldi = i;
       } else {
         i++;
       }
     }
 
-    if(i!=oldi) {
-      String t=new String();
-      t.value=value;
-      t.offset=oldi;
-      t.count=i-oldi;
+    if (i != oldi) {
+      String t = new String();
+      t.value = value;
+      t.offset = oldi;
+      t.count = i - oldi;
       splitted.addElement(t);
     }
 
@@ -476,18 +485,18 @@ public class String {
   }
 
   public boolean contains(String str) {
-    int i,j;
+    int i, j;
     char[] strChar = str.toCharArray();
     int cnt;
 
-    for(i = 0; i < count; i++) {
-      if(value[i] == strChar[0]) {
-        cnt=0;
-        for(j=0; j < str.length() && i+j < count; j++) {
-          if(value[i+j] == strChar[j])
+    for (i = 0; i < count; i++) {
+      if (value[i] == strChar[0]) {
+        cnt = 0;
+        for (j = 0; j < str.length() && i + j < count; j++) {
+          if (value[i + j] == strChar[j])
             cnt++;
         }
-        if(cnt == str.length())
+        if (cnt == str.length())
           return true;
       }
     }
@@ -499,8 +508,8 @@ public class String {
   public String trim() {
     int len = count;
     int st = 0;
-    int off = offset;      /* avoid getfield opcode */
-    char[] val = value;    /* avoid getfield opcode */
+    int off = offset; /* avoid getfield opcode */
+    char[] val = value; /* avoid getfield opcode */
 
     while ((st < len) && (val[off + st] <= ' ')) {
       st++;
@@ -508,7 +517,7 @@ public class String {
     while ((st < len) && (val[off + len - 1] <= ' ')) {
       len--;
     }
-    return ((st > 0) || (len < count))?substring(st, len):this;
+    return ((st > 0) || (len < count)) ? substring(st, len) : this;
   }
 
   public boolean matches(String regex) {
diff --git a/Robust/src/ClassLibrary/SSJava/StringBuffer.java b/Robust/src/ClassLibrary/SSJava/StringBuffer.java
index fb1222b4..bebe02f0 100644
--- a/Robust/src/ClassLibrary/SSJava/StringBuffer.java
+++ b/Robust/src/ClassLibrary/SSJava/StringBuffer.java
@@ -1,23 +1,28 @@
+@LATTICE("V<C, V<O")
+@METHODDEFAULT("O<V,V<C,C<IN,C*,THISLOC=O,RETURNLOC=O")
 public class StringBuffer {
+  @LOC("V")
   char value[];
+  @LOC("C")
   int count;
-  //    private static final int DEFAULTSIZE=16;
+
+  // private static final int DEFAULTSIZE=16;
 
   public StringBuffer(String str) {
-    value=new char[str.count+16];    //16 is DEFAULTSIZE
-    count=str.count;
-    for(int i=0; i<count; i++)
-      value[i]=str.value[i+str.offset];
+    value = new char[str.count + 16]; // 16 is DEFAULTSIZE
+    count = str.count;
+    for (int i = 0; i < count; i++)
+      value[i] = str.value[i + str.offset];
   }
 
   public StringBuffer() {
-    value=new char[16];    //16 is DEFAULTSIZE
-    count=0;
+    value = new char[16]; // 16 is DEFAULTSIZE
+    count = 0;
   }
 
   public StringBuffer(int i) {
-    value=new char[i];
-    count=0;
+    value = new char[i];
+    count = 0;
   }
 
   public int length() {
@@ -32,56 +37,57 @@ public class StringBuffer {
     return value[x];
   }
 
-  public StringBuffer append(char c) {
+  public StringBuffer append(@LOC("IN") char c) {
     return append(String.valueOf(c));
   }
 
-  public StringBuffer append(String s) {
-    if ((s.count+count)>value.length) {
+  public StringBuffer append(@LOC("IN") String s) {
+    if ((s.count + count) > value.length) {
       // Need to allocate
-      char newvalue[]=new char[s.count+count+16];       //16 is DEFAULTSIZE
-      for(int i=0; i<count; i++)
-        newvalue[i]=value[i];
-      for(int i=0; i<s.count; i++)
-        newvalue[i+count]=s.value[i+s.offset];
-      value=newvalue;
-      count+=s.count;
+      @LOC("C") char newvalue[] = new char[s.count + count + 16]; // 16 is
+                                                                  // DEFAULTSIZE
+      for (@LOC("C") int i = 0; i < count; i++)
+        newvalue[i] = value[i];
+      for (@LOC("C") int i = 0; i < s.count; i++)
+        newvalue[i + count] = s.value[i + s.offset];
+      value = newvalue;
+      count += s.count;
     } else {
-      for(int i=0; i<s.count; i++) {
-        value[i+count]=s.value[i+s.offset];
+      for (@LOC("C") int i = 0; i < s.count; i++) {
+        value[i + count] = s.value[i + s.offset];
       }
-      count+=s.count;
+      count += s.count;
     }
     return this;
   }
 
   public void ensureCapacity(int i) {
-    int size=2*count;
-    if (i>size)
-      size=i;
-    if (i>value.length) {
-      char newvalue[]=new char[i];
-      for(int ii=0; ii<count; ii++)
-        newvalue[ii]=value[ii];
-      value=newvalue;
+    int size = 2 * count;
+    if (i > size)
+      size = i;
+    if (i > value.length) {
+      char newvalue[] = new char[i];
+      for (int ii = 0; ii < count; ii++)
+        newvalue[ii] = value[ii];
+      value = newvalue;
     }
   }
 
   public StringBuffer append(StringBuffer s) {
-    if ((s.count+count)>value.length) {
+    if ((s.count + count) > value.length) {
       // Need to allocate
-      char newvalue[]=new char[s.count+count+16];       //16 is DEFAULTSIZE
-      for(int i=0; i<count; i++)
-        newvalue[i]=value[i];
-      for(int i=0; i<s.count; i++)
-        newvalue[i+count]=s.value[i];
-      value=newvalue;
-      count+=s.count;
+      char newvalue[] = new char[s.count + count + 16]; // 16 is DEFAULTSIZE
+      for (int i = 0; i < count; i++)
+        newvalue[i] = value[i];
+      for (int i = 0; i < s.count; i++)
+        newvalue[i + count] = s.value[i];
+      value = newvalue;
+      count += s.count;
     } else {
-      for(int i=0; i<s.count; i++) {
-        value[i+count]=s.value[i];
+      for (int i = 0; i < s.count; i++) {
+        value[i + count] = s.value[i];
       }
-      count+=s.count;
+      count += s.count;
     }
     return this;
   }
@@ -102,7 +108,7 @@ public class StringBuffer {
   public synchronized StringBuffer replace(int start, int end, String str) {
     if (start < 0) {
       // FIXME
-      System.printString("StringIndexOutOfBoundsException: "+start+"\n");
+      System.printString("StringIndexOutOfBoundsException: " + start + "\n");
     }
     if (start > count) {
       // FIXME
@@ -131,7 +137,7 @@ public class StringBuffer {
   void expandCapacity(int minimumCapacity) {
     int newCapacity = (value.length + 1) * 2;
     if (newCapacity < 0) {
-      newCapacity = 0x7fffffff /*Integer.MAX_VALUE*/;
+      newCapacity = 0x7fffffff /* Integer.MAX_VALUE */;
     } else if (minimumCapacity > newCapacity) {
       newCapacity = minimumCapacity;
     }
diff --git a/Robust/src/Tests/ssJava/mp3decoder/Decoder.java b/Robust/src/Tests/ssJava/mp3decoder/Decoder.java
index 8b3ecbc6..febbd7c8 100644
--- a/Robust/src/Tests/ssJava/mp3decoder/Decoder.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/Decoder.java
@@ -26,8 +26,10 @@
  * @version 0.0.7 12/12/99
  * @since 0.0.5
  */
-@LATTICE("ST,DE<OUT,DE<FIL,DE<LA,O,EQ,PA,INIT,DE*")
+@LATTICE("OUT<DE,DE<FILTER,FILTER<FACTORS,FACTORS<EQ,EQ<PARAM,PARAM<INIT")
+@METHODDEFAULT("THIS,THISLOC=THIS,RETURNLOC=THIS")
 public class Decoder implements DecoderErrors {
+
   static private final Params DEFAULT_PARAMS = new Params();
 
   /**
@@ -64,15 +66,15 @@ public class Decoder implements DecoderErrors {
   // @LOC("DE")
   // private LayerIDecoder l1decoder;
 
-  @LOC("O")
+  @LOC("OUT")
   private int outputFrequency;
-  @LOC("O")
+  @LOC("OUT")
   private int outputChannels;
 
   @LOC("EQ")
   private Equalizer equalizer = new Equalizer();
 
-  @LOC("PA")
+  @LOC("PARAM")
   private Params params;
 
   @LOC("INIT")
@@ -136,27 +138,27 @@ public class Decoder implements DecoderErrors {
    * 
    * @return A SampleBuffer containing the decoded samples.
    */
-  @LATTICE("O<DE,DE<TH,TH<IN,THISLOC=TH")
-  @RETURNLOC("O")
-  public Obuffer decodeFrame(@LOC("IN") Header header) throws DecoderException {
+  @LATTICE("THIS<VAR,THISLOC=THIS,VAR*")
+  public void decodeFrame(@LOC("VAR") Header header) throws DecoderException {
 
     if (!initialized) {
-      float scalefactor = 32700.0f;
+      @LOC("VAR") float scalefactor = 32700.0f;
 
-      int mode = header.mode();
-      int layer = header.layer();
-      int channels = mode == Header.SINGLE_CHANNEL ? 1 : 2;
+      @LOC("VAR") int mode = header.mode();
+      @LOC("VAR") int layer = header.layer();
+      @LOC("VAR") int channels = mode == Header.SINGLE_CHANNEL ? 1 : 2;
 
       // set up output buffer if not set up by client.
       // if (output == null)
       // output = new SampleBuffer(header.frequency(), channels);
       SampleBufferWrapper.init(header.frequency(), channels);
 
-      float[] factors = equalizer.getBandFactors();
-      SynthesisFilter filter1 = new SynthesisFilter(0, scalefactor, factors);
+      @LOC("THIS,Decoder.FACTORS") float[] factors = equalizer.getBandFactors();
+      @LOC("THIS,Decoder.FILTER") SynthesisFilter filter1 =
+          new SynthesisFilter(0, scalefactor, factors);
 
       // REVIEW: allow mono output for stereo
-      SynthesisFilter filter2 = null;
+      @LOC("THIS,Decoder.FILTER") SynthesisFilter filter2 = null;
       if (channels == 2) {
         filter2 = new SynthesisFilter(1, scalefactor, factors);
       }
@@ -169,21 +171,10 @@ public class Decoder implements DecoderErrors {
       initialized = true;
     }
 
-    @LOC("TH") int layer = header.layer();
-
     SampleBufferWrapper.getOutput().clear_buffer();
-    // output.clear_buffer();
-
-    // @LOC("DE,Decoder.DE") FrameDecoder decoder = retrieveDecoder(header,
-    // stream, layer);
-    // decoder.decodeFrame();
-
     l3decoder.decodeFrame(header);
-
     SampleBufferWrapper.getOutput().write_buffer(1);
-    // output.write_buffer(1);
 
-    // return output;
   }
 
   /**
diff --git a/Robust/src/Tests/ssJava/mp3decoder/Header.java b/Robust/src/Tests/ssJava/mp3decoder/Header.java
index 10c7d343..4ac483a7 100644
--- a/Robust/src/Tests/ssJava/mp3decoder/Header.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/Header.java
@@ -34,7 +34,8 @@
  * Class for extracting information from a frame header.
  */
 @LATTICE("HI<HNS,HNS<H,C<H,NS<FS,FS<H,FS<HV,H<SYNC,HV<SYNC,HV<T,SYNC*,HV*,FS*,HI*")
-@METHODDEFAULT("OUT<V,V<THIS,THIS<SH,SH<IN,SH*,THISLOC=THIS,GLOBALLOC=IN")
+// @METHODDEFAULT("OUT<V,V<THIS,THIS<SH,SH<IN,SH*,THISLOC=THIS,GLOBALLOC=IN")
+@METHODDEFAULT("THIS,THISLOC=THIS,RETURNLOC=THIS")
 public final class Header {
 
   public static final int[][] frequencies = { { 22050, 24000, 16000, 1 },
@@ -112,14 +113,17 @@ public final class Header {
   @LOC("T")
   private int _headerstring = -1; // E.B
 
+  @LOC("T")
   private SideInfoBuffer sib;
+  @LOC("T")
   private BitReserve br;
 
   Header() {
   }
 
+  @LATTICE("OUT<BUF,BUF<THIS,THISLOC=THIS,RETURNLOC=OUT")
   public String toString() {
-    StringBuffer buffer = new StringBuffer(200);
+    @LOC("BUF") StringBuffer buffer = new StringBuffer(200);
     buffer.append("Layer ");
     buffer.append(layer_string());
     buffer.append(" frame ");
@@ -135,7 +139,7 @@ public final class Header {
     buffer.append(' ');
     buffer.append(bitrate_string());
 
-    String s = buffer.toString();
+    @LOC("OUT") String s = buffer.toString();
     return s;
   }
 
@@ -148,7 +152,7 @@ public final class Header {
     boolean sync = false;
     do {
       headerstring = stream.syncHeader(syncmode);
-      if(headerstring==-1){
+      if (headerstring == -1) {
         return -1;
       }
       _headerstring = headerstring; // E.B
@@ -357,7 +361,6 @@ public final class Header {
   /**
    * Returns version.
    */
-  @RETURNLOC("OUT")
   public int version() {
     return h_version;
   }
@@ -365,7 +368,6 @@ public final class Header {
   /**
    * Returns Layer ID.
    */
-  @RETURNLOC("OUT")
   public int layer() {
     return h_layer;
   }
@@ -373,7 +375,6 @@ public final class Header {
   /**
    * Returns bitrate index.
    */
-  @RETURNLOC("OUT")
   public int bitrate_index() {
     return h_bitrate_index;
   }
@@ -395,7 +396,6 @@ public final class Header {
   /**
    * Returns Mode.
    */
-  @RETURNLOC("OUT")
   public int mode() {
     return h_mode;
   }
@@ -473,7 +473,6 @@ public final class Header {
   /**
    * Returns Slots.
    */
-  @RETURNLOC("OUT")
   public int slots() {
     return nSlots;
   }
@@ -481,13 +480,11 @@ public final class Header {
   /**
    * Returns Mode Extension.
    */
-  @RETURNLOC("OUT")
   public int mode_extension() {
     return h_mode_extension;
   }
 
   // E.B -> private to public
-  @LOC("T")
   public static final int bitrates[][][] = {
       {
           { 0 /* free format */, 32000, 48000, 56000, 64000, 80000, 96000, 112000, 128000, 144000,
@@ -601,15 +598,16 @@ public final class Header {
    * 
    * @return milliseconds per frame
    */
+  @LATTICE("OUT<THIS,THISLOC=THIS,RETURNLOC=OUT")
   public float ms_per_frame() // E.B
   {
     if (h_vbr == true) {
-      double tpf = h_vbr_time_per_frame[layer()] / frequency();
+      @LOC("OUT") double tpf = h_vbr_time_per_frame[layer()] / frequency();
       if ((h_version == MPEG2_LSF) || (h_version == MPEG25_LSF))
         tpf /= 2;
       return ((float) (tpf * 1000));
     } else {
-      float ms_per_frame_array[][] =
+      @LOC("OUT") float ms_per_frame_array[][] =
           { { 8.707483f, 8.0f, 12.0f }, { 26.12245f, 24.0f, 36.0f }, { 26.12245f, 24.0f, 36.0f } };
       return (ms_per_frame_array[h_layer - 1][h_sample_frequency]);
     }
@@ -651,7 +649,6 @@ public final class Header {
   }
 
   // E.B -> private to public
-  @LOC("T")
   public static final String bitrate_str[][][] = {
       {
           { "free format", "32 kbit/s", "48 kbit/s", "56 kbit/s", "64 kbit/s", "80 kbit/s",
@@ -793,7 +790,6 @@ public final class Header {
    * 
    * @return number of subbands
    */
-  @RETURNLOC("OUT")
   public int number_of_subbands() {
     return h_number_of_subbands;
   }
@@ -805,7 +801,6 @@ public final class Header {
    * 
    * @return intensity
    */
-  @RETURNLOC("OUT")
   public int intensity_stereo_bound() {
     return h_intensity_stereo_bound;
   }
diff --git a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
index 3277f38b..4ec6a898 100644
--- a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
@@ -48,7 +48,7 @@
 // llth added for decode
 // @LATTICE("IS1D*,RO<IS1D,IS1D<SI2,SI2<SI1,SI<P2S,SF1<CH0,SF0*,SFB_SH<NS,NS<SI,SFB_SH*,SFB<SFB_SH,C,C*,SI1<SF2,SF2<SFB,SF1<BR,LR*,OUT<LR,LR<RO,NZ*,SI<SF1,SI1<NZ,NZ<SI,SI1<SBI,SBI<SI,BUF<FT,SF1<SF0,SF0<HD1,BR<ST,ST,FT<SP,SP<OUT,OUT<SI1,SI1<SI,P2S<CH0,CH0<MAX0,MAX0<BR1,FS<BR1,BR1<BR,BR<HD1,HD1<HD,OUT*,BR1*,SI1*,MAX0*,CH0*,RAW,TS,F,C,K,LY,VAR,IR,IP,CSH,GLSFD3,GLSFD4,GLSFD5,GLSFF4,GLSFF2,GLSFF3,GLSFF1,GSF4,GSF5,GSF1,GSF2,GSF3,HD2,HD3,BT,GR,RO6,RO5,RO9,RO8,RO7,RO4,RO1,RO3,RO2,SH,ME,TMP2,S,LSF,J")
 @LATTICE("ISR*,ISP*,LR<ISR,ISR<ISP,SI1<SF2,NS*,HD<ST,IS1D*,RO1<RO,RO1*,RO<IS1D,IS1D<SI2,SI2<SI1,BR<NS,NS<SI,SFB_SH*,SFB<SFB_SH,C,C*,SF2<SFB,LR*,OUT<LR,ISP<RO1,NZ*,SI<SF1,BR1<NZ,NZ<BR,SI1<RT,RT<SBI,SBI<SI,BUF<FT,SF1<CH0,CH0<HD1,FT<SP,SP<OUT,OUT<SI1,SI1<SI,SFB_SH<BR1,BR1<BR,HD1<HD,OUT*,BR1*,SI1*,CH0*,RAW,TS,F,C,K,LY,VAR,IR,IP,CSH,GLSFD3,GLSFD4,GLSFD5,GLSFF4,GLSFF2,GLSFF3,GLSFF1,GSF4,GSF5,GSF1,GSF2,GSF3,HD2,HD3,BT,GR,RO6,RO5,RO9,RO8,RO7,RO4,RO1,RO3,RO2,SH,ME,TMP2,S,LSF,J")
-@METHODDEFAULT("OUT<V,V<THIS,THIS<SH,SH<IN,SH*,THISLOC=THIS,GLOBALLOC=IN")
+@METHODDEFAULT("OUT<V,V<THIS,THIS<SH,SH<IN,SH*,THISLOC=THIS,GLOBALLOC=IN,RETURNLOC=OUT")
 final class LayerIIIDecoder implements FrameDecoder {
   static final double d43 = (4.0 / 3.0);
   @LOC("SFB")
@@ -106,8 +106,10 @@ final class LayerIIIDecoder implements FrameDecoder {
   @LOC("SBI")
   private int sfreq;
 
+  @LOC("ST")
   private int part2_start;
 
+  @LOC("ST")
   private boolean initialized = false;
 
   // constructor for the linear type system
@@ -210,7 +212,8 @@ final class LayerIIIDecoder implements FrameDecoder {
 
   }
 
-  private void init(Header header) {
+  @LATTICE("THIS<C,THIS<IN,C*,THISLOC=THIS")
+  private void init(@LOC("IN") Header header) {
 
     frame_start = 0;
     channels = (header.mode() == Header.SINGLE_CHANNEL) ? 1 : 2;
@@ -242,8 +245,8 @@ final class LayerIIIDecoder implements FrameDecoder {
       first_channel = last_channel = 0;
     }
 
-    for (@LOC("CH") int ch = 0; ch < 2; ch++)
-      for (@LOC("J") int j = 0; j < 576; j++)
+    for (@LOC("C") int ch = 0; ch < 2; ch++)
+      for (@LOC("C") int j = 0; j < 576; j++)
         prevblck[ch][j] = 0.0f;
 
     nonzero[0] = nonzero[1] = 576;
@@ -433,7 +436,7 @@ final class LayerIIIDecoder implements FrameDecoder {
     br = new BitReserve();
   }
 
-  public void decodeFrame(Header header) {
+  public void decodeFrame(@LOC("IN") Header header) {
     decode(header);
   }
 
@@ -457,7 +460,7 @@ final class LayerIIIDecoder implements FrameDecoder {
    */
   // @LATTICE("BYTE<THIS,THIS<MAIN,MAIN<VAR,THIS<GR,GR<VAR,BYTE*,GR*,THISLOC=THIS,GLOBALLOC=VAR")
   @LATTICE("VAR<THIS,C<THIS,THIS<IN,THISLOC=THIS,C*,VAR*")
-  public void decode(Header header) {
+  public void decode(@LOC("IN") Header header) {
 
     if (!initialized) {
       init(header);
@@ -598,11 +601,13 @@ final class LayerIIIDecoder implements FrameDecoder {
    * Reads the side info from the stream, assuming the entire. frame has been
    * read already. Mono : 136 bits (= 17 bytes) Stereo : 256 bits (= 32 bytes)
    */
-  private boolean get_side_info(Header header) {
+  @LATTICE("THIS<C,C<IN,C*,THISLOC=THIS,RETURNLOC=THIS")
+  private boolean get_side_info(@LOC("IN") Header header) {
 
-    SideInfoBuffer sib = header.getSideInfoBuffer();
+    @LOC("IN") SideInfoBuffer sib = header.getSideInfoBuffer();
 
-    int ch, gr;
+    @LOC("C") int ch;
+    @LOC("C") int gr;
     // System.out.println("#get_side_info");
     if (header.version() == Header.MPEG1) {
 
@@ -727,7 +732,7 @@ final class LayerIIIDecoder implements FrameDecoder {
 	 *
 	 */
   @LATTICE("THIS<IN,THISLOC=THIS,GLOBALLOC=IN")
-  private void get_scale_factors(Header header, @LOC("THIS,LayerIIIDecoder.CH0") int ch,
+  private void get_scale_factors(@LOC("IN") Header header, @LOC("THIS,LayerIIIDecoder.CH0") int ch,
       @LOC("THIS,LayerIIIDecoder.CH0") int gr) {
 
     // gr_info_s gr_info = (si.ch[ch].gr[gr]); remove alias
@@ -841,8 +846,8 @@ final class LayerIIIDecoder implements FrameDecoder {
 
   // ssjava
   @LATTICE("M<THIS,THIS<IN,THIS<C,C*,M*,THISLOC=THIS,GLOBALLOC=THIS")
-  private void get_LSF_scale_data(Header header, @LOC("THIS,LayerIIIDecoder.CH0") int ch,
-      @LOC("THIS,LayerIIIDecoder.CH0") int gr) {
+  private void get_LSF_scale_data(@LOC("IN") Header header,
+      @LOC("THIS,LayerIIIDecoder.CH0") int ch, @LOC("THIS,LayerIIIDecoder.CH0") int gr) {
 
     @LOC("THIS,LayerIIIDecoder.HD1") int mode_ext = header.mode_extension();
     // @LOC("THIS,LayerIIIDecoder.GLSFD1") gr_info_s gr_info =
@@ -945,8 +950,8 @@ final class LayerIIIDecoder implements FrameDecoder {
 	 *
 	 */
   @LATTICE("THIS<IN,THISLOC=THIS,GLOBALLOC=IN")
-  private void get_LSF_scale_factors(Header header, @LOC("THIS,LayerIIIDecoder.CH0") int ch,
-      @LOC("THIS,LayerIIIDecoder.CH0") int gr) {
+  private void get_LSF_scale_factors(@LOC("IN") Header header,
+      @LOC("THIS,LayerIIIDecoder.CH0") int ch, @LOC("THIS,LayerIIIDecoder.CH0") int gr) {
 
     @LOC("THIS,LayerIIIDecoder.SFB_SH") int sfb;
     @LOC("THIS,LayerIIIDecoder.SFB_SH") int m = 0;
@@ -1013,21 +1018,22 @@ final class LayerIIIDecoder implements FrameDecoder {
   @LOC("SI1")
   int w[] = { 0 };
 
-  private void huffman_decode(int ch, int gr) {
+  private void huffman_decode(@LOC("THIS,LayerIIIDecoder.CH0") int ch,
+      @LOC("THIS,LayerIIIDecoder.CH0") int gr) {
     x[0] = 0;
     y[0] = 0;
     v[0] = 0;
     w[0] = 0;
 
-    int part2_3_end = part2_start + si.ch[ch].gr[gr].part2_3_length;
-    int num_bits;
-    int region1Start;
-    int region2Start;
-    int index;
-
-    int buf, buf1;
+    @LOC("THIS,LayerIIIDecoder.BR,BitReserve.BIT") int part2_3_end =
+        part2_start + si.ch[ch].gr[gr].part2_3_length;
+    @LOC("THIS,LayerIIIDecoder.BR,BitReserve.BIT") int num_bits;
+    @LOC("THIS,LayerIIIDecoder.SI1") int region1Start;
+    @LOC("THIS,LayerIIIDecoder.SI1") int region2Start;
+    @LOC("THIS,LayerIIIDecoder.BR,BitReserve.BIT") int index;
 
-    huffcodetab h;
+    @LOC("THIS,LayerIIIDecoder.SI1") int buf;
+    @LOC("THIS,LayerIIIDecoder.SI1") int buf1;
 
     // Find region boundary for short block case
 
@@ -1053,9 +1059,10 @@ final class LayerIIIDecoder implements FrameDecoder {
 
     index = 0;
     // Read bigvalues area
-    for (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) {
 
-      int htIdx;
+      @LOC("THIS,LayerIIIDecoder.BR,BitReserve.BIT")  int htIdx;
       if (i < region1Start) {
         htIdx = si.ch[ch].gr[gr].table_select[0];
         // h = huffcodetab.ht[si.ch[ch].gr[gr].table_select[0]];
@@ -1080,7 +1087,7 @@ final class LayerIIIDecoder implements FrameDecoder {
 
     // Read count1 area
 
-    int htIdx = si.ch[ch].gr[gr].count1table_select + 32;
+    @LOC("THIS,LayerIIIDecoder.BR,BitReserve.BIT")     int htIdx = si.ch[ch].gr[gr].count1table_select + 32;
     // h = huffcodetab.ht[si.ch[ch].gr[gr].count1table_select + 32];
     num_bits = br.hsstell();
 
@@ -1427,7 +1434,7 @@ final class LayerIIIDecoder implements FrameDecoder {
 
   // ssjava
   @LATTICE("IO<THIS,THIS<IN,THISLOC=THIS,GLOBALLOC=IN")
-  private void stereo(Header header, @LOC("THIS,LayerIIIDecoder.CH0") int gr) {
+  private void stereo(@LOC("IN") Header header, @LOC("THIS,LayerIIIDecoder.CH0") int gr) {
     @LOC("THIS,LayerIIIDecoder.RO1") int sb;
     @LOC("THIS,LayerIIIDecoder.RO1") int ss;
 
@@ -1725,8 +1732,9 @@ final class LayerIIIDecoder implements FrameDecoder {
     @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,LayerIIIDecoder$III_side_info_t.CH,LayerIIIDecoder$temporaire.GR1") gr_info_s gr_info =
-//        (si.ch[ch].gr[gr]);
+    // @LOC("THIS,LayerIIIDecoder.SI,LayerIIIDecoder$III_side_info_t.CH,LayerIIIDecoder$temporaire.GR1")
+    // gr_info_s gr_info =
+    // (si.ch[ch].gr[gr]);
     // 31 alias-reduction operations between each pair of sub-bands
     // with 8 butterflies between each pair
 
diff --git a/Robust/src/Tests/ssJava/mp3decoder/OutputChannels.java b/Robust/src/Tests/ssJava/mp3decoder/OutputChannels.java
index 544dfb25..276ca6a2 100644
--- a/Robust/src/Tests/ssJava/mp3decoder/OutputChannels.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/OutputChannels.java
@@ -27,7 +27,7 @@
  * @since 0.0.7
  */
 @LATTICE("B<T")
-@METHODDEFAULT("OUT<IN")
+@METHODDEFAULT("OUT<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT")
 public class OutputChannels {
   /**
    * Flag to indicate output should include both channels.
@@ -49,13 +49,9 @@ public class OutputChannels {
    */
   public static final int DOWNMIX_CHANNELS = 3;
 
-  @LOC("B")
   public static final OutputChannels LEFT = new OutputChannels(LEFT_CHANNEL);
-  @LOC("B")
   public static final OutputChannels RIGHT = new OutputChannels(RIGHT_CHANNEL);
-  @LOC("B")
   public static final OutputChannels BOTH = new OutputChannels(BOTH_CHANNELS);
-  @LOC("B")
   public static final OutputChannels DOWNMIX = new OutputChannels(DOWNMIX_CHANNELS);
 
   @LOC("T")
diff --git a/Robust/src/Tests/ssJava/mp3decoder/Player.java b/Robust/src/Tests/ssJava/mp3decoder/Player.java
index 2c54b3d7..d06bfb6e 100644
--- a/Robust/src/Tests/ssJava/mp3decoder/Player.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/Player.java
@@ -112,7 +112,6 @@ public class Player {
   public boolean play(@LOC("IN") int frames) throws JavaLayerException {
     @LOC("IN") boolean ret = true;
 
-    int count = 0;
     SSJAVA: while (frames-- > 0 && ret) {
       ret = decodeFrame();
     }
@@ -171,8 +170,7 @@ public class Player {
    * 
    * @return true if there are no more frames to decode, false otherwise.
    */
-  @LATTICE("O<TH,THISLOC=TH")
-  @RETURNLOC("O")
+  @LATTICE("C,O<THIS,THIS<IN,C*,THISLOC=THIS,RETURNLOC=O")
   protected boolean decodeFrame() throws JavaLayerException {
     try {
       // AudioDevice out = audio;
@@ -180,7 +178,7 @@ public class Player {
       // return false;
 
       // Header h = bitstream.readFrame();
-      Header h = BitstreamWrapper.readFrame();
+      @LOC("IN") Header h = BitstreamWrapper.readFrame();
 
       if (h == null)
         return false;
@@ -189,10 +187,10 @@ public class Player {
       decoder.decodeFrame(h);
 
       // eom debug
-      int sum = 0;
-      short[] outbuf = SampleBufferWrapper.getOutput().getBuffer();
+      @LOC("C") int sum = 0;
+      @LOC("C") short[] outbuf = SampleBufferWrapper.getBuffer();
       // short[] outbuf = output.getBuffer();
-      for (int i = 0; i < SampleBufferWrapper.getOutput().getBufferLength(); i++) {
+      for (@LOC("C") int i = 0; i < SampleBufferWrapper.getBufferLength(); i++) {
         // System.out.println(outbuf[i]);
         sum += outbuf[i];
       }
diff --git a/Robust/src/Tests/ssJava/mp3decoder/SampleBufferWrapper.java b/Robust/src/Tests/ssJava/mp3decoder/SampleBufferWrapper.java
index 45f96ef9..72aeb6b3 100644
--- a/Robust/src/Tests/ssJava/mp3decoder/SampleBufferWrapper.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/SampleBufferWrapper.java
@@ -12,4 +12,19 @@ public class SampleBufferWrapper {
     return output;
   }
 
+  @TRUST
+  static short[] getBuffer() {
+    return output.getBuffer();
+  }
+
+  @TRUST
+  static int getBufferLength() {
+    return output.getBufferLength();
+  }
+
+  @TRUST
+  static void appendSamples(int channel, float[] f) {
+    output.appendSamples(channel, f);
+  }
+
 }
diff --git a/Robust/src/Tests/ssJava/mp3decoder/SideInfoBuffer.java b/Robust/src/Tests/ssJava/mp3decoder/SideInfoBuffer.java
index d3a3e1d5..47d827d6 100644
--- a/Robust/src/Tests/ssJava/mp3decoder/SideInfoBuffer.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/SideInfoBuffer.java
@@ -1,85 +1,89 @@
+@LATTICE("BUF<IDX,V,IDX*")
+@METHODDEFAULT("THIS<IN,THISLOC=THIS,RETURNLOC=THIS")
 public class SideInfoBuffer {
 
-	/**
-	 * The frame buffer that holds the data for the current frame.
-	 */
-	private final int[] framebuffer = new int[BUFFER_INT_SIZE];
+  /**
+   * The frame buffer that holds the data for the current frame.
+   */
+  @LOC("BUF")
+  private final int[] framebuffer = new int[BUFFER_INT_SIZE];
 
-	/**
-	 * Maximum size of the frame buffer.
-	 */
-	private static final int BUFFER_INT_SIZE = 433;
+  /**
+   * Maximum size of the frame buffer.
+   */
+  private static final int BUFFER_INT_SIZE = 433;
 
-	/**
-	 * Index into <code>framebuffer</code> where the next bits are retrieved.
-	 */
-	private int wordpointer;
+  /**
+   * Index into <code>framebuffer</code> where the next bits are retrieved.
+   */
+  @LOC("IDX")
+  private int wordpointer;
 
-	/**
-	 * Number (0-31, from MSB to LSB) of next bit for get_bits()
-	 */
-	private int bitindex;
+  /**
+   * Number (0-31, from MSB to LSB) of next bit for get_bits()
+   */
+  @LOC("IDX")
+  private int bitindex;
 
-	private int main_data_begin;
+  @LOC("V")
+  private int main_data_begin;
 
-	public int getMain_data_begin() {
-		return main_data_begin;
-	}
+  public int getMain_data_begin() {
+    return main_data_begin;
+  }
 
-	public void setMain_data_begin(int main_data_begin) {
-		this.main_data_begin = main_data_begin;
-	}
+  public void setMain_data_begin(@LOC("IN") int main_data_begin) {
+    this.main_data_begin = main_data_begin;
+  }
 
-	private final int bitmask[] = {
-			0, // dummy
-			0x00000001, 0x00000003, 0x00000007, 0x0000000F, 0x0000001F,
-			0x0000003F, 0x0000007F, 0x000000FF, 0x000001FF, 0x000003FF,
-			0x000007FF, 0x00000FFF, 0x00001FFF, 0x00003FFF, 0x00007FFF,
-			0x0000FFFF, 0x0001FFFF };
+  private static final int bitmask[] = {
+      0, // dummy
+      0x00000001, 0x00000003, 0x00000007, 0x0000000F, 0x0000001F, 0x0000003F, 0x0000007F,
+      0x000000FF, 0x000001FF, 0x000003FF, 0x000007FF, 0x00000FFF, 0x00001FFF, 0x00003FFF,
+      0x00007FFF, 0x0000FFFF, 0x0001FFFF };
 
-	public int get_bits(int number_of_bits) {
-		int returnvalue = 0;
-		int sum = bitindex + number_of_bits;
-		// System.out.println("bitindex=" + bitindex + " wordpointer="
-		// + wordpointer);
-		// E.B
-		// There is a problem here, wordpointer could be -1 ?!
-		if (wordpointer < 0)
-			wordpointer = 0;
-		// E.B : End.
+  @LATTICE("OUT<THIS,THIS<IN,THISLOC=THIS,RETURNLOC=OUT")
+  public int get_bits(@LOC("IN") int number_of_bits) {
+    @LOC("OUT") int returnvalue = 0;
+    @LOC("THIS,SideInfoBuffer.IDX") int sum = bitindex + number_of_bits;
+    // System.out.println("bitindex=" + bitindex + " wordpointer="
+    // + wordpointer);
+    // E.B
+    // There is a problem here, wordpointer could be -1 ?!
+    if (wordpointer < 0)
+      wordpointer = 0;
+    // E.B : End.
 
-		if (sum <= 32) {
-			// all bits contained in *wordpointer
-			returnvalue = (framebuffer[wordpointer] >>> (32 - sum))
-					& bitmask[number_of_bits];
-			// returnvalue = (wordpointer[0] >> (32 - sum)) &
-			// bitmask[number_of_bits];
-			if ((bitindex += number_of_bits) == 32) {
-				bitindex = 0;
-				wordpointer++; // added by me!
-			}
-			return returnvalue;
-		}
+    if (sum <= 32) {
+      // all bits contained in *wordpointer
+      returnvalue = (framebuffer[wordpointer] >>> (32 - sum)) & bitmask[number_of_bits];
+      // returnvalue = (wordpointer[0] >> (32 - sum)) &
+      // bitmask[number_of_bits];
+      if ((bitindex += number_of_bits) == 32) {
+        bitindex = 0;
+        wordpointer++; // added by me!
+      }
+      return returnvalue;
+    }
 
-		// E.B : Check that ?
-		// ((short[])&returnvalue)[0] = ((short[])wordpointer + 1)[0];
-		// wordpointer++; // Added by me!
-		// ((short[])&returnvalue + 1)[0] = ((short[])wordpointer)[0];
-		int Right = (framebuffer[wordpointer] & 0x0000FFFF);
-		wordpointer++;
-		int Left = (framebuffer[wordpointer] & 0xFFFF0000);
-		returnvalue = ((Right << 16) & 0xFFFF0000)
-				| ((Left >>> 16) & 0x0000FFFF);
+    // E.B : Check that ?
+    // ((short[])&returnvalue)[0] = ((short[])wordpointer + 1)[0];
+    // wordpointer++; // Added by me!
+    // ((short[])&returnvalue + 1)[0] = ((short[])wordpointer)[0];
+    @LOC("THIS,SideInfoBuffer.IDX") int Right = (framebuffer[wordpointer] & 0x0000FFFF);
+    wordpointer++;
+    @LOC("THIS,SideInfoBuffer.IDX") int Left = (framebuffer[wordpointer] & 0xFFFF0000);
+    returnvalue = ((Right << 16) & 0xFFFF0000) | ((Left >>> 16) & 0x0000FFFF);
 
-		returnvalue >>>= 48 - sum; // returnvalue >>= 16 - (number_of_bits - (32
-									// - bitindex))
-		returnvalue &= bitmask[number_of_bits];
-		bitindex = sum - 32;
-		return returnvalue;
-	}
+    returnvalue >>>= 48 - sum; // returnvalue >>= 16 - (number_of_bits - (32
+    // - bitindex))
+    returnvalue &= bitmask[number_of_bits];
+    bitindex = sum - 32;
+    return returnvalue;
+  }
 
-	public void setBuffer(int idx, int value) {
-		framebuffer[idx] = value;
-	}
+  public void setBuffer(int idx, int value) {
+    framebuffer[idx] = value;
+  }
 
 }
diff --git a/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java b/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java
index 39871d82..0f276849 100644
--- a/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java
@@ -34,16 +34,25 @@
  * from 32, 44.1 or 48 kHz to 8 kHz, if ULAW is defined. Frequencies above 4 kHz
  * are removed by ignoring higher subbands.
  */
+@LATTICE("OUT<V,V<SAMPLE,SAMPLE<EQ,EQ<IDX")
 final class SynthesisFilter {
-  private int vcount = 0;
+
+  @LOC("IDX")
   private int vidx = 1;
+  @LOC("V")
   private float[] v1;
+  @LOC("V")
   private float[] v2;
   // private float[] actual_v; // v1 or v2
+  @LOC("IDX")
   private int actual_write_pos; // 0-15
+  @LOC("SAMPLE")
   private float[] samples; // 32 new subband samples
+  @LOC("V")
   private int channel;
+  @LOC("V")
   private float scalefactor;
+  @LOC("EQ")
   private float[] eq;
 
   /**
@@ -871,7 +880,7 @@ final class SynthesisFilter {
    * Compute PCM Samples.
    */
 
-  private float[] _tmpOut = new float[32];
+  @LOC("OUT") private float[] _tmpOut = new float[32];
 
   private void compute_pcm_samples0() {
 
@@ -1819,7 +1828,7 @@ final class SynthesisFilter {
     // if (buffer != null) {
     // buffer.appendSamples(channel, _tmpOut);
     // }
-    SampleBufferWrapper.getOutput().appendSamples(channel, _tmpOut);
+    SampleBufferWrapper.appendSamples(channel, _tmpOut);
 
     /*
      * // MDM: I was considering putting in quality control for // low-spec
@@ -1914,6 +1923,7 @@ final class SynthesisFilter {
    * d[] split into subarrays of length 16. This provides for more faster access
    * by allowing a block of 16 to be addressed with constant offset.
    **/
+  @LOC("V")
   private static float d16[][] = null;
 
   /**