From 2d7ac7342fd75e5e8a7649f8108599411f65b876 Mon Sep 17 00:00:00 2001
From: david <david>
Date: Wed, 13 Jul 2011 00:07:21 +0000
Subject: [PATCH] refined annotation

---
 Robust/src/ClassLibrary/SSJava/PushbackInputStream.java | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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
   {
-- 
2.34.1