001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package javafe.util;
004
005 import javafe.genericfile.*;
006
007
008 /**
009 * A <I>location</I> is an integer that identifies the position in a
010 * file of a particular piece of program source text. This class is
011 * never instantiated. It contains static functions for manipulating
012 * locations. Locations are produced by the
013 * <code>CorrelatedReader</code> class (and by this class), they are
014 * stored in ASTs, and they are passed to <code>ErrorSet</code> to
015 * identify the program source that caused a particular error or
016 * warning.
017
018 * <p> There are three kinds of locations.
019 * <ol>
020 * <li> <i>Regular locations</i> encode the file, line, column, and
021 * offset of a character read by <code>CorrelatedReader</code>. A
022 * call to the <code>getLocation()</code> method of a
023 * <code>CorrelatedReader</code> object returns the regular location
024 * of the last character read from that <code>CorrelatedReader</code>
025 * object. The file/line/column/offset of that location can be
026 * extracted via the methods described below.
027
028 * <br> Following emacs, line numbers begin at 1, column numbers at 0,
029 * and offsets at 1. A newline character is considered the last
030 * character on a line.
031
032 * <li> <i>Whole file locations</i> encode just file information.
033 * They are currently used for error messages that are global to a
034 * file (eg. the error message given when a file that is expected to
035 * contain a package declaration does not have one). We expect they
036 * will also be used in ASTs produced from class files (since there is
037 * no meaningful line or column information, and offset information
038 * would not be useful in an error message).
039
040 * <li><i>The null location</i> is a constant that plays a similar
041 * role for locations that null plays for reference types.
042 * </ol>
043 *
044 * <p> Interface reviewed at Sparta Meeting 1/8/97.
045 *
046 * @see javafe.util.CorrelatedReader
047 * @see javafe.util.ErrorSet
048 */
049
050 public class Location
051 {
052 //@ public model JMLDataGroup internalState;
053
054 /** Private constructor. Never called. */
055
056 private Location() {}
057
058
059 /** The null location, is the constant 0. */
060
061 public static final int NULL = 0;
062
063
064 /**********************************************************************
065 * Check if a location is a whole file location.
066
067 * <p>Precondition: loc should be a valid location (ie a regular,
068 * whole file, or dummy location).
069 *********************************************************************/
070
071 //@ pure
072 public static boolean isWholeFileLoc(int loc) {
073 return LocationManagerCorrelatedReader.isWholeFileLoc(loc);
074 }
075
076
077 /**********************************************************************
078 * Extracts the file corresponding to a location.
079
080 * <p>Precondition: loc should be a regular location or a whole file
081 location.
082 *********************************************************************/
083
084 //@ requires loc != Location.NULL;
085 //@ modifies \nothing;
086 //@ ensures \result != null;
087 public static GenericFile toFile(int loc) {
088 return LocationManagerCorrelatedReader.locToFile(loc);
089 }
090
091
092 /**********************************************************************
093 * Extracts the filename corresponding to a location.
094
095 * <p>Precondition: loc should be a regular location or a whole file
096 location.
097 *********************************************************************/
098
099 //@ requires loc != Location.NULL;
100 //@ modifies \nothing;
101 //@ ensures \result != null;
102 public static String toFileName(int loc) {
103 return LocationManagerCorrelatedReader.locToFile(loc).getHumanName();
104 }
105
106
107 /**********************************************************************
108 * Extracts the offset corresponding to a location.
109
110 * The first character in a stream is at offset 1.
111
112 * <p>Precondition: loc should be a regular location.
113 *********************************************************************/
114
115 //@ requires loc != Location.NULL;
116 //@ modifies \nothing;
117 public static int toOffset(int loc) {
118 return LocationManagerCorrelatedReader.locToOffset(loc);
119 }
120
121 /**********************************************************************
122 * Extracts the line number corresponding to a location.
123
124 * The first line in a stream is numbered 1.
125
126 * <p>Precondition: loc should be a regular location.
127 *********************************************************************/
128
129 //@ requires loc != Location.NULL;
130 //@ modifies \nothing;
131 //@ ensures \result >= 1;
132 public static int toLineNumber(int loc) {
133 return LocationManagerCorrelatedReader.locToLineNumber(loc);
134 }
135
136 /**********************************************************************
137 * Extracts the column corresponding to a location.
138
139 * The first column on each line is numbered 0.
140
141 * <p>Precondition: loc should be a regular location.
142 *********************************************************************/
143
144 //@ requires loc != Location.NULL;
145 //@ modifies \nothing;
146 //@ ensures \result >= 0;
147 public static int toColumn(int loc) {
148 return LocationManagerCorrelatedReader.locToColumn(loc);
149 }
150
151 /**********************************************************************
152 * Convert a location into a printable description suitable for use
153 * in a warning or error message.
154
155 * <p>Precondition: loc should be a valid location (ie a regular,
156 * whole file, or dummy location).
157 *********************************************************************/
158
159 public static /*@non_null*/String toString(int loc) {
160
161 if( loc == NULL )
162 return "<dummy location>";
163
164 String name = "\"" + toFileName(loc) + "\"";
165
166 if (isWholeFileLoc(loc))
167 return name;
168
169 return name + ", line " + toLineNumber(loc)
170 +", col " + toColumn(loc);
171 }
172
173 public static String toFileLineString(int loc) {
174 String s = Location.toFileName(loc);
175 if (!Location.isWholeFileLoc(loc))
176 s = s + ":" + Location.toLineNumber(loc);
177 return s;
178 }
179
180 /**********************************************************************
181 * Create a whole file location corresponding to the given GenericFile.
182 * Calls to <code>toFile</code> on that location will return
183 * this file.
184 *********************************************************************/
185
186 //@ ensures \result != Location.NULL;
187 public static int createWholeFileLoc(/*@ non_null @*/ GenericFile file) {
188 return FileCorrelatedReader.createWholeFileLoc(file);
189 }
190
191
192 /**
193 * Create a fake location described by description.<p>
194 *
195 * This should only be used by debugging code and in places where
196 * it should never see the light of day.
197 *
198 * The resulting location is a whole-file location associated
199 * with an unopenable file with human-name description.
200 */
201 //@ ensures \result != Location.NULL;
202 public static int createFakeLoc(/*@ non_null @*/ String description) {
203 return FileCorrelatedReader.createWholeFileLoc(
204 new UnopenableFile(description));
205 }
206
207
208
209 //@ requires 0 <= streamId;
210 //@ requires streamId < LocationManagerCorrelatedReader.allCorrStreams.elementCount;
211 //@ requires line > 0;
212 //@ requires col >= 0;
213 //@ ensures \result != Location.NULL ;
214 public static int make(int streamId, int line, int col) {
215 return LocationManagerCorrelatedReader.makeLocation(streamId, line, col);
216 }
217
218 /**
219 * Attempts to return a location <code>n</code> characters further
220 * to the right of <code>loc</code> on the same line. Returns the
221 * same location if it is not a regular location.
222 *
223 * Produces an assertion failure if that location does not exist
224 * (e.g., the line is too short.).
225 */
226 //@ requires n >= 0;
227 //@ ensures loc != NULL ==> \result != NULL;
228 public static int inc(int loc, int n) {
229 if (isWholeFileLoc(loc) || loc==NULL)
230 return loc;
231
232 // Should be a regular location here:
233 // This assertion is commented out because when we translate
234 // Java's assert construct into a conditional throws clause,
235 // under some circumstances, the translated (fictional) IfStmt
236 // does not actually fit on the original line. E.g.,
237 // assert false;
238 // becomes
239 // if !false throw new java.lang.AssertionError();
240 // which obviously is longer than the original statement.
241 // Assert.notFalse(toLineNumber(loc) == toLineNumber(loc+n)); //@ nowarn pre
242 return loc+n;
243 } //@ nowarn Post;
244
245
246 /**
247 * Returns the internal stream ID used for the stream associated
248 * with location <code>loc</code>.
249 */
250 //@ requires loc != Location.NULL;
251 public static int toStreamId(int loc) {
252 return LocationManagerCorrelatedReader.locToStreamId(loc);
253 }
254
255 /**
256 * Returns the file associated with stream id <code>id</code>,
257 * where <code>id</code> has previously been returned by
258 * <code>toStreamId</code>.
259 */
260 //@ requires 0 <= id && id < LocationManagerCorrelatedReader.allCorrStreams.elementCount;
261 public static GenericFile streamIdToFile(int id) {
262 return LocationManagerCorrelatedReader.streamIdToFile(id);
263 }
264 }