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 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    }