try to make mp3decoder pass SSJava checking

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 1f4c7fc59500bd8a8ba3045000e44c016ecbeb19..e752141d1b61b9cff557aa78db1a5eda01c3db3c 100644 (file)
--- 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 cc8b9f3357cc58b6b5b4a14f8559e1b5fa74f89a..ead2f26f3c514e1aa2f328fc702256df41f93fc4 100644 (file)
--- 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 1d26f3613b51b755332a16044814a2cc7b65ffa3..fd2d6a7178694c4f9c8401418521d2d0ae1f52c1 100644 (file)
--- 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 78fe1bb9f455d0823dc7be947e9c25b20de50a89..fddf74f3ff898882e6470cfa75ad5fbc58ed639b 100644 (file)
--- 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 7fd9be88f988f3001f771d96af3f0edc1cf6ea2e..2692393560d51910640431380e816242b1dfc36e 100644 (file)
--- 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\r
         * synchronization to the start of a frame.\r
         */\r
-       static byte             INITIAL_SYNC = 0;\r
+       static final byte               INITIAL_SYNC = 0;\r
 \r
        /**\r
         * Synchronization control constant for non-initial frame\r
         * synchronizations.\r
         */\r
-       static byte             STRICT_SYNC = 1;\r
+       static final byte               STRICT_SYNC = 1;\r
 \r
        // max. 1730 bytes per frame: 144 * 384kbit/s / 32000 Hz + 2 Bytes CRC\r
        /**\r

diff --git a/Robust/src/Tests/ssJava/mp3decoder/BitstreamException.java b/Robust/src/Tests/ssJava/mp3decoder/BitstreamException.java
index 07aa18fb74d303d849d2b5be18c03dd3a75286ce..fb2e60c71e221f23728c755a5725d85ded22fd75 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/BitstreamException.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/BitstreamException.java
@@ -34,11 +34,11 @@
  * @since 0.0.6\r
  * @author MDM 12/12/99\r
  */\r
-\r
+@LATTICE("E")\r
 public class BitstreamException extends JavaLayerException\r
        implements BitstreamErrors\r
 {      \r
-       private int errorcode = UNKNOWN_ERROR;\r
+       @LOC("E") private int errorcode = UNKNOWN_ERROR;\r
        \r
        public BitstreamException(String msg, Throwable t)\r
        {\r

diff --git a/Robust/src/Tests/ssJava/mp3decoder/LayerIDecoder.java b/Robust/src/Tests/ssJava/mp3decoder/LayerIDecoder.java
index fbbdd278f00165c4adcefd3ddd4207802e7ed549..a1eec6e4e54b0f1e0e57de4e6387a8b87903fb80 100644 (file)
--- 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 a65f2efe68938f5a8f7c8f6cdf9f3511c3782430..116f32f11bbde5020c52d447c7724b349f7320cd 100644 (file)
--- 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