X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=Robust%2Fsrc%2FBenchmarks%2FSSJava%2FMP3Decoder%2FBitReserve.java;h=190fd65c3dc4e104b4a8ee2f204f842cbe0e8fd6;hb=ff3ceae6b47a1a01bc56fa55fa5770cba0bf252f;hp=d6dc322fb8d86a5d5069395daa1ccc73e9bac2cd;hpb=338b40f8f52cf09dc5fcef67796acc65a69758b9;p=IRC.git

diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/BitReserve.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/BitReserve.java
index d6dc322f..190fd65c 100644
--- a/Robust/src/Benchmarks/SSJava/MP3Decoder/BitReserve.java
+++ b/Robust/src/Benchmarks/SSJava/MP3Decoder/BitReserve.java
@@ -38,7 +38,7 @@
 // REVIEW: there is no range checking, so buffer underflow or overflow
 // can silently occur.
 @LATTICE("BUF<OFF,BUF<BIT,BIT*,OFF*")
-@METHODDEFAULT("OUT<THIS,THIS<IN,IN*,THISLOC=THIS,RETURNLOC=OUT")
+@METHODDEFAULT("OUT<THIS,THIS<IN,IN*,OUT*,THISLOC=THIS,RETURNLOC=OUT")
 final class BitReserve {
   /**
    * Size of the internal buffer to store the reserved bits. Must be a power of