From: david <david>
Date: Wed, 13 Jul 2011 00:07:21 +0000 (+0000)
Subject: refined annotation
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=2d7ac7342fd75e5e8a7649f8108599411f65b876;p=IRC.git

refined annotation
---

diff --git a/Robust/src/ClassLibrary/SSJava/PushbackInputStream.java b/Robust/src/ClassLibrary/SSJava/PushbackInputStream.java
index 06403f84..c9910732 100644
--- 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
   {