    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    }