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 }