de.uka.ilkd.key.java

Class PosConvertException

java.lang.Object

java.lang.Throwable

java.lang.Exception

java.lang.RuntimeException

de.uka.ilkd.key.java.ConvertException

de.uka.ilkd.key.java.PosConvertException

All Implemented Interfaces:

java.io.Serializable

public class PosConvertException
extends ConvertException

A convert exception enriched with a location within a file/source. The source's name itself is not captured.

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field and Description
private int	column The column
private int	line The line
private static long	serialVersionUID

Constructor Summary

Constructors

Constructor and Description
PosConvertException(java.lang.String message, int line, int column) Instantiates a new exception with position information.
PosConvertException(java.lang.Throwable cause, int line, int column) Instantiates a new exception with position information.

Method Summary

Modifier and Type	Method and Description
int	getColumn() Gets the column of the exception location.
int	getLine() Gets the line of the exception location.

Methods inherited from class de.uka.ilkd.key.java.ConvertException

parseException, proofJavaException

Methods inherited from class java.lang.Throwable

addSuppressed, fillInStackTrace, getCause, getLocalizedMessage, getMessage, getStackTrace, getSuppressed, initCause, printStackTrace, printStackTrace, printStackTrace, setStackTrace, toString

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

serialVersionUID

private static final long serialVersionUID

See Also:

Constant Field Values

line

private final int line

The line

column

private int column

The column

Constructor Detail

PosConvertException

public PosConvertException(java.lang.String message,
                           int line,
                           int column)

Instantiates a new exception with position information.

Parameters:

message - the message, not null

line - the line to point to

column - the column to point to

PosConvertException

public PosConvertException(java.lang.Throwable cause,
                           int line,
                           int column)

Instantiates a new exception with position information.

Parameters:

cause - the exception causing this instance.

line - the line to point to

column - the column to point to

Method Detail

getLine

public int getLine()

Gets the line of the exception location.

Returns:

the line

getColumn

public int getColumn()

Gets the column of the exception location.

Returns:

the column