de.uka.ilkd.key.java.expression.literal

Class LongLiteral

java.lang.Object

de.uka.ilkd.key.java.JavaSourceElement

de.uka.ilkd.key.java.JavaProgramElement

de.uka.ilkd.key.java.expression.Literal

de.uka.ilkd.key.java.expression.literal.AbstractIntegerLiteral

de.uka.ilkd.key.java.expression.literal.LongLiteral

All Implemented Interfaces:

Expression, ModelElement, ProgramElement, SourceElement, TerminalProgramElement, SVSubstitute

public class LongLiteral
extends AbstractIntegerLiteral

Long literal.

Author:

AutoDoc

Field Summary

Fields

Modifier and Type	Field and Description
private static java.math.BigInteger	MAX_LONG A constant holding the maximum valid value of a signed long: 263-1
private static java.math.BigInteger	MAX_ULONG A constant holding the maximum valid value as if a long was interpreted unsigned: : 264-1
private static java.math.BigInteger	MIN_LONG A constant holding the minimum valid value of a signed long: -263
private long	value The actual value of the literal.
private java.lang.String	valueStr Textual representation of the value as a decimal number (always ends with 'L').

Constructor Summary

Constructors

Constructor and Description
LongLiteral(ExtList children, java.lang.String valStr) Constructor for Recoder2KeY transformation.
LongLiteral(long value) Creates a new LongLiteral representing the given long.
LongLiteral(java.lang.String valStr) Creates a new LongLiteral from the given String.

Method Summary

Modifier and Type	Method and Description
KeYJavaType	getKeYJavaType(Services javaServ) retrieves the literal's type
long	getValue()
java.lang.String	getValueString()
protected long	parseFromString(java.lang.String sourceStr) Parses the String and extracts the actual value of the literal.
void	prettyPrint(PrettyPrinter p) Pretty printing the source element.
void	visit(Visitor v) calls the corresponding method of a visitor in order to perform some action/transformation on this element

Methods inherited from class de.uka.ilkd.key.java.expression.literal.AbstractIntegerLiteral

computeHashCode, equals, equalsModRenaming, getLDTName, representsDecLiteral, toString

Methods inherited from class de.uka.ilkd.key.java.expression.Literal

getKeYJavaType, match

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

getComments, hashCode, prettyPrintMain, reuseSignature

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

getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getLastElement, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.java.ProgramElement

getComments

Methods inherited from interface de.uka.ilkd.key.java.SourceElement

getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getLastElement, getPositionInfo, getRelativePosition, getStartPosition

Field Detail

MAX_LONG

private static final java.math.BigInteger MAX_LONG

A constant holding the maximum valid value of a signed long: 2⁶³-1

MIN_LONG

private static final java.math.BigInteger MIN_LONG

A constant holding the minimum valid value of a signed long: -2⁶³

MAX_ULONG

private static final java.math.BigInteger MAX_ULONG

A constant holding the maximum valid value as if a long was interpreted unsigned: : 2⁶⁴-1

valueStr

private final java.lang.String valueStr

Textual representation of the value as a decimal number (always ends with 'L').

value

private final long value

The actual value of the literal.

Constructor Detail

LongLiteral

public LongLiteral(long value)

Creates a new LongLiteral representing the given long.

Parameters:

value - the long value represented by the literal

LongLiteral

public LongLiteral(java.lang.String valStr)

Creates a new LongLiteral from the given String. The String is parsed and checked for range. The input may be any String containing a literal as described by the Java 8 Language Specification. This includes hexadecimal, decimal, octal, and binary literals as well as literals containing underscores as separators. In addition, a preceding '-' sign is allowed.

Parameters:

valStr - the String that contains the literal

Throws:

java.lang.NumberFormatException - if the given String does not represent a syntactically valid literal or represents a value out of long range

See Also:

http://docs.oracle.com/javase/specs/jls/se8/html/jls-3.html#jls-3.10.1

LongLiteral

public LongLiteral(ExtList children,
                   java.lang.String valStr)

Constructor for Recoder2KeY transformation.

Parameters:

children - the children of this AST element as KeY classes, may contain: Comments

valStr - the value of the literal

Throws:

java.lang.NumberFormatException - if the given String does not represent a syntactically valid literal or represents a value out of long range

Method Detail

visit

public void visit(Visitor v)

Description copied from interface: SourceElement

calls the corresponding method of a visitor in order to perform some action/transformation on this element

Parameters:

v - the Visitor

prettyPrint

public void prettyPrint(PrettyPrinter p)
                 throws java.io.IOException

Description copied from class: JavaSourceElement

Pretty printing the source element.

Specified by:

prettyPrint in interface SourceElement

Overrides:

prettyPrint in class JavaProgramElement

Parameters:

p - a pretty printer.

Throws:

java.io.IOException - occasionally thrown.

getKeYJavaType

public KeYJavaType getKeYJavaType(Services javaServ)

Description copied from class: Literal

retrieves the literal's type

Specified by:

getKeYJavaType in class Literal

Parameters:

javaServ - the Services offering access to the Java model

Returns:

the literal's type

getValue

public long getValue()

Specified by:

getValue in class AbstractIntegerLiteral

Returns:

the actual value of the literal as a long

getValueString

public java.lang.String getValueString()

Specified by:

getValueString in class AbstractIntegerLiteral

Returns:

the actual value of the literal converted to a decimal String. If the literal represents a negative value, the first character is a '-' sign. The returned String always ends with 'L' to indicate a long.

parseFromString

protected long parseFromString(java.lang.String sourceStr)

Parses the String and extracts the actual value of the literal. This method is able to parse literals as described in the Java 8 Language Specification: hexadecimal (beginning with '0x'), decimal, octal (beginning with '0'), and binary (beginning with '0b') literals. In addition, underscores are allowed as separators inside the literal. All values parsed by this method are checked for range correctly, particularly considering the asymmetric range of long. Hexadecimal, octal and binary literals are converted using two's complement.

Parameters:

sourceStr - the String containing the value

Returns:

the parsed value as a long

Throws:

java.lang.NumberFormatException - if the given String does not represent a syntactically valid literal or represents a value out of long range

See Also:

http://docs.oracle.com/javase/specs/jls/se8/html/jls-3.html#jls-3.10.1