From: yeom <yeom>
Date: Wed, 13 Jul 2011 01:03:45 +0000 (+0000)
Subject: try to make mp3decoder pass SSJava checking
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=IRC.git;a=commitdiff_plain;h=dde70cfcaee9aee77dacd393a431d5acd1414b5e

try to make mp3decoder pass SSJava checking
---

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 1f4c7fc5..e752141d 100644
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -1018,12 +1018,12 @@ public class FlowDownCheck {
 
     ClassDescriptor cd = md.getClassDesc();
     Vector<AnnotationDescriptor> annotationVec = vd.getType().getAnnotationMarkers();
-    
-    if(!md.getModifiers().isAbstract()){
+
+    if (!md.getModifiers().isAbstract()) {
       // 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.getSymbol() + " of the class " + cd.getSymbol());
       }
 
       if (annotationVec.size() > 1) { // variable can have at most one location
@@ -1057,7 +1057,6 @@ public class FlowDownCheck {
       }
     }
 
-
   }
 
   private DeltaLocation parseDeltaDeclaration(MethodDescriptor md, TreeNode n, String locDec) {
@@ -1160,7 +1159,10 @@ public class FlowDownCheck {
     // Check to see that fields are okay
     for (Iterator field_it = cd.getFields(); field_it.hasNext();) {
       FieldDescriptor fd = (FieldDescriptor) field_it.next();
-      checkFieldDeclaration(cd, fd);
+
+      if (!(fd.isFinal() && fd.isStatic())) {
+        checkFieldDeclaration(cd, fd);
+      }
     }
   }
 
diff --git a/Robust/src/ClassLibrary/SSJava/BufferedInputStream.java b/Robust/src/ClassLibrary/SSJava/BufferedInputStream.java
index cc8b9f33..ead2f26f 100644
--- a/Robust/src/ClassLibrary/SSJava/BufferedInputStream.java
+++ b/Robust/src/ClassLibrary/SSJava/BufferedInputStream.java
@@ -61,7 +61,7 @@ exception statement from your version. */
  * @author Warren Levy (warrenl@cygnus.com)
  * @author Jeroen Frijters (jeroen@frijters.net)
  */
-@LATTICE("BUF<C")
+@LATTICE("BUF<C,IN<T")
 @METHODDEFAULT("D<IN,D<C,THISLOC=D")
 public class BufferedInputStream extends FilterInputStream
 {
diff --git a/Robust/src/ClassLibrary/SSJava/ByteArrayInputStream.java b/Robust/src/ClassLibrary/SSJava/ByteArrayInputStream.java
index 1d26f361..fd2d6a71 100644
--- a/Robust/src/ClassLibrary/SSJava/ByteArrayInputStream.java
+++ b/Robust/src/ClassLibrary/SSJava/ByteArrayInputStream.java
@@ -44,6 +44,7 @@ exception statement from your version. */
   * @author Warren Levy (warrenl@cygnus.com)
   * @author Aaron M. Renn (arenn@urbanophile.com)
   */ 
+@LATTICE("")
 public class ByteArrayInputStream extends InputStream
 {
   /**
diff --git a/Robust/src/ClassLibrary/SSJava/FileOutputStream.java b/Robust/src/ClassLibrary/SSJava/FileOutputStream.java
index 78fe1bb9..fddf74f3 100644
--- a/Robust/src/ClassLibrary/SSJava/FileOutputStream.java
+++ b/Robust/src/ClassLibrary/SSJava/FileOutputStream.java
@@ -1,7 +1,7 @@
 //import java.io.FileDescriptor;
-
+@LATTICE("FD")
 public class FileOutputStream extends OutputStream {
-  private int fd;
+  @LOC("FD") private int fd;
 
   public FileOutputStream(String pathname) {
     fd=nativeOpen(pathname.getBytes());
diff --git a/Robust/src/Tests/ssJava/mp3decoder/Bitstream.java b/Robust/src/Tests/ssJava/mp3decoder/Bitstream.java
index 7fd9be88..26923935 100644
--- a/Robust/src/Tests/ssJava/mp3decoder/Bitstream.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/Bitstream.java
@@ -48,13 +48,13 @@ public final class Bitstream implements BitstreamErrors
 	 * Synchronization control constant for the initial
 	 * synchronization to the start of a frame.
 	 */
-	static byte		INITIAL_SYNC = 0;
+	static final byte		INITIAL_SYNC = 0;
 
 	/**
 	 * Synchronization control constant for non-initial frame
 	 * synchronizations.
 	 */
-	static byte		STRICT_SYNC = 1;
+	static final byte		STRICT_SYNC = 1;
 
 	// max. 1730 bytes per frame: 144 * 384kbit/s / 32000 Hz + 2 Bytes CRC
 	/**
diff --git a/Robust/src/Tests/ssJava/mp3decoder/BitstreamException.java b/Robust/src/Tests/ssJava/mp3decoder/BitstreamException.java
index 07aa18fb..fb2e60c7 100644
--- a/Robust/src/Tests/ssJava/mp3decoder/BitstreamException.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/BitstreamException.java
@@ -34,11 +34,11 @@
  * @since 0.0.6
  * @author MDM	12/12/99
  */
-
+@LATTICE("E")
 public class BitstreamException extends JavaLayerException
 	implements BitstreamErrors
 {	
-	private int errorcode = UNKNOWN_ERROR;
+	@LOC("E") private int errorcode = UNKNOWN_ERROR;
 	
 	public BitstreamException(String msg, Throwable t)
 	{
diff --git a/Robust/src/Tests/ssJava/mp3decoder/LayerIDecoder.java b/Robust/src/Tests/ssJava/mp3decoder/LayerIDecoder.java
index fbbdd278..a1eec6e4 100644
--- a/Robust/src/Tests/ssJava/mp3decoder/LayerIDecoder.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/LayerIDecoder.java
@@ -188,7 +188,7 @@
 	 * Used for single channel mode
 	 * and in derived class for intensity stereo mode
 	 */
-        @LATTICE("S<L,L<H,H<SH,SH*,S*")
+     @LATTICE("_bottom_<L,S<L,L<H,H<SH,SH*,S*")
 	@METHODDEFAULT("OUT<V,V<SH,SH<IN,SH*,THISLOC=V,GLOBALLOC=IN")
 	static class SubbandLayer1 extends Subband
 	{
diff --git a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
index a65f2efe..116f32f1 100644
--- a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
@@ -38,7 +38,7 @@
  * 
  * @since 0.0
  */
-@LATTICE("FS<BR,BR<SF,LR<IR,IR<IP,IP<SF,LR<K,K<F,LR<VAR,LR<RO,RO<F,VAR<F,VAR<RAW,CSH<F,SAM<O,O<F,NS<SI,SI<CH,SFREQ<H,MAX<H,H<CH,FLCH<CH,FLCH<WCH,SF<SFT,SFT<NS,NS<C,TS<RAW,O<TS,LY<F,NZ<VAR,C*,FS*,SI*,IP*,IR*,LR*,K*,O*,TS*,TS<BT,BT<GR,GR<SI,LR<S,S<ME,ME<CH,K<SH,K<LSF,LSF<H,LSF<CH,IP<SH,SH<J,J<S,S<ME,SH<SFREQ,SH<RO,IP<TMP2,LSF<H,TMP2<F,J*,SH*,O<RO2,RO2<RO3,RO3<RO4,RO4<RO5,O<RO1,RO1<RO5,RO5<RO6,RO6<RO7,RO7<RO8,RO8<RO9,RO9<SFREQ,RO9<F,RO1*,RO4*,RO5*,RO6*,RO9*,VAR<HD3,HD3<HD2,HD2<HD1,HD1<SI,HD1<SFREQ,HD1<RAW,HD2*,HD3*,SFB<GLSFD5,GLSFD5<NS,GLSFD5<GLSFD4,NS<GLSFD3,GLSFD4<GLSFD3,GLSFD3<GLSFD2,GLSFD2<GLSFD1,GLSFD1<SI,GLSFD5*,SF<GLSFF4,GLSFF4<GLSFF3,GLSFF3<GLSFF2,GLSFF2<GLSFF1,GLSFF1<SI,GLSFF4*,GLSFF3*,GLSFF2*,SF<GSF5,GSF5<GSF4,GSF4<GSF3,GSF3<GSF2,GSF2<GSF1,GSF1<SI,GSF5*,GSF4*,O<D3,D3<D2,D2<D1,D1<FLCH,D1*,D2*")
+@LATTICE("FS<BR,BR<SF,LR<IR,IR<IP,IP<SF,LR<K,K<F,LR<VAR,LR<RO,RO<F,VAR<F,VAR<RAW,CSH<F,SAM<O,O<F,NS<SI,SI<CH,SFREQ<H,MAX<H,H<CH,FLCH<CH,FLCH<WC,SF<SFT,SFT<NS,NS<C,TS<RAW,O<TS,LY<F,NZ<VAR,C*,FS*,SI*,IP*,IR*,LR*,K*,O*,TS*,TS<BT,BT<GR,GR<SI,LR<S,S<ME,ME<CH,K<SH,K<LSF,LSF<H,LSF<CH,IP<SH,SH<J,J<S,S<ME,SH<SFREQ,SH<RO,IP<TMP2,LSF<H,TMP2<F,J*,SH*,O<RO2,RO2<RO3,RO3<RO4,RO4<RO5,O<RO1,RO1<RO5,RO5<RO6,RO6<RO7,RO7<RO8,RO8<RO9,RO9<SFREQ,RO9<F,RO1*,RO4*,RO5*,RO6*,RO9*,VAR<HD3,HD3<HD2,HD2<HD1,HD1<SI,HD1<SFREQ,HD1<RAW,HD2*,HD3*,SFB<GLSFD5,GLSFD5<NS,GLSFD5<GLSFD4,NS<GLSFD3,GLSFD4<GLSFD3,GLSFD3<GLSFD2,GLSFD2<GLSFD1,GLSFD1<SI,GLSFD5*,SF<GLSFF4,GLSFF4<GLSFF3,GLSFF3<GLSFF2,GLSFF2<GLSFF1,GLSFF1<SI,GLSFF4*,GLSFF3*,GLSFF2*,SF<GSF5,GSF5<GSF4,GSF4<GSF3,GSF3<GSF2,GSF2<GSF1,GSF1<SI,GSF5*,GSF4*,O<D3,D3<D2,D2<D1,D1<FLCH,D1*,D2*")
 //4th line added for hybrid.
 //5th added for stereo
 //6th added for reorder method