refined annotation

diff --git a/Robust/src/ClassLibrary/SSJava/PushbackInputStream.java b/Robust/src/ClassLibrary/SSJava/PushbackInputStream.java
index 06403f84800365cee914fc222d7d2b7fd4d8d416..c9910732f8e0fdb8c7bbd43340ed5a19fbfc0deb 100644 (file)
--- a/Robust/src/ClassLibrary/SSJava/PushbackInputStream.java
+++ b/Robust/src/ClassLibrary/SSJava/PushbackInputStream.java
@@ -207,9 +207,9 @@ public class PushbackInputStream extends FilterInputStream
    *
    * @exception IOException If an error occurs.
    */
-  @LATTICE("THIS<BUF,THISLOCAL=THIS")
+  @LATTICE("OUT<THIS,THISLOC=THIS")
   @RETURNLOC("THIS")
-  public synchronized int read(@LOC("THIS,PushbackInputStream.POS") byte[] b,
+  public synchronized int read(@LOC("OUT") byte[] b,
                                @LOC("THIS,PushbackInputStream.POS") int off,
                                @LOC("THIS,PushbackInputStream.POS") int len) throws IOException
   {