org.jmlspecs.jml4.rac.runtime
Class JMLAssertionError.Location

java.lang.Object
  org.jmlspecs.jml4.rac.runtime.JMLAssertionError.Location

Enclosing class:

JMLAssertionError

public static class JMLAssertionError.Location
extends java.lang.Object

Data structure class to represent a source code location including file name, line number, and character position.

Field Summary

int	character 1-based position of a character in a line.
java.lang.String	file File name
int	line 1-based line number.

Constructor Summary

JMLAssertionError.Location(java.lang.String file, int line)
Creates a new location with the given information.

JMLAssertionError.Location(java.lang.String file, int line, int character)
Creates a new location with the given information.

Method Summary

java.lang.String

toString() Returns a string representation of this location.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

file

public java.lang.String file

File name

line

public int line

1-based line number. The value 0 means that the line number is not known.

character

public int character

1-based position of a character in a line. The value of 0 means that the character position is not known.

Constructor Detail

JMLAssertionError.Location

public JMLAssertionError.Location(java.lang.String file,
                                  int line,
                                  int character)

Creates a new location with the given information.

JMLAssertionError.Location

public JMLAssertionError.Location(java.lang.String file,
                                  int line)

Creates a new location with the given information.

Method Detail

toString

public java.lang.String toString()

Returns a string representation of this location. The returned string has the following form:

  File "T.java", line 10, character 20
 

It is the form used by JML2, and this makes JML4 output compatible to that of JML2; there are tools use error messages of the above form to locate the corresponding source code line.

Overrides:

toString in class java.lang.Object