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

Class IntLiteral

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.IntLiteral

All Implemented Interfaces:

Expression, ModelElement, ProgramElement, SourceElement, TerminalProgramElement, SVSubstitute

public class IntLiteral
extends AbstractIntegerLiteral

Int literal.

Author:

AutoDoc

Field Summary

Fields

Modifier and Type	Field and Description
private static long	MAX_UINT A constant holding the maximum valid value as if an int was interpreted unsigned: 232-1
private int	value The actual value of the literal.
private java.lang.String	valueStr Textual representation of the value as a decimal number.

Constructor Summary

Constructors

Constructor and Description
IntLiteral(ExtList children, java.lang.String valStr) Constructor for Recoder2KeY transformation.
IntLiteral(int value) Creates a new IntLiteral representing the given int.
IntLiteral(java.lang.String valStr) Creates a new IntLiteral 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 int	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_UINT

private static final long MAX_UINT

A constant holding the maximum valid value as if an int was interpreted unsigned: 2³²-1

See Also:

Constant Field Values

valueStr

private final java.lang.String valueStr

Textual representation of the value as a decimal number.

value

private final int value

The actual value of the literal.

Constructor Detail

IntLiteral

public IntLiteral(int value)

Creates a new IntLiteral representing the given int.

Parameters:

value - the int value represented by the literal

IntLiteral

public IntLiteral(java.lang.String valStr)

Creates a new IntLiteral 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 int range

See Also:

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

IntLiteral

public IntLiteral(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 int 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.

parseFromString

protected int parseFromString(java.lang.String sourceStr)
                       throws java.lang.NumberFormatException

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 int. 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 int range

See Also:

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