de.uka.ilkd.key.java.expression.operator

Class NewArray

java.lang.Object

de.uka.ilkd.key.java.JavaSourceElement

de.uka.ilkd.key.java.JavaProgramElement

de.uka.ilkd.key.java.JavaNonTerminalProgramElement

de.uka.ilkd.key.java.expression.Operator

de.uka.ilkd.key.java.expression.operator.TypeOperator

de.uka.ilkd.key.java.expression.operator.NewArray

All Implemented Interfaces:

Expression, ExpressionContainer, ModelElement, NonTerminalProgramElement, ProgramElement, Reference, ReferencePrefix, TypeReferenceContainer, SourceElement, SVSubstitute

public class NewArray
extends TypeOperator
implements Reference, ReferencePrefix

The array allocation operator. There are two variants for NewArray:

1. Ordinary array construction
   new XYZ[d₁]...[d_n]
2. Initialized array construction
   new XYZ[]...[] { a₁, ..., a_n }

Contrary to an ordinary New, a NewArray is no ConstructorReference (since all ArrayType constructors are predefined) and is not used as a Statement (since there are no side-effects in the constructor). No access path is required for new, since there is no inner class problem.

NewArray has either a list of dimension length expressions, or a single ArrayInitializer.

Field Summary

Fields

Modifier and Type	Field and Description
protected ArrayInitializer	arrayInitializer Array initializer.
protected int	dimensions Dimensions.
private KeYJavaType	keyJavaType the key java type of this array

Fields inherited from class de.uka.ilkd.key.java.expression.operator.TypeOperator

typeReference

Fields inherited from class de.uka.ilkd.key.java.expression.Operator

children, INFIX, POSTFIX, PREFIX

Constructor Summary

Constructors

Constructor and Description
NewArray(Expression[] arguments, TypeReference typeRef, KeYJavaType keyJavaType, ArrayInitializer init, int dimensions) New array.
NewArray(ExtList children, KeYJavaType keyJavaType, ArrayInitializer init, int dimensions) New array.

Method Summary

Modifier and Type	Method and Description
int	getArity() Get arity.
ArrayInitializer	getArrayInitializer() Get array initializer.
ProgramElement	getChildAt(int index) Returns the child at the specified index in this node's "virtual" child array
int	getChildCount() Returns the number of children of this node.
int	getDimensions() Get dimensions.
Expression	getExpressionAt(int index)
int	getExpressionCount() Get the number of expressions in this container.
KeYJavaType	getKeYJavaType()
KeYJavaType	getKeYJavaType(Services javaServ) same as getKeYJavaType()
SourceElement	getLastElement() Finds the source element that occurs last in the source.
int	getNotation() Get notation.
int	getPrecedence() Get precedence.
ReferencePrefix	getReferencePrefix() We do not have a prefix, so fake it!
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.operator.TypeOperator

getKeYJavaType, getTypeReference, getTypeReferenceAt, getTypeReferenceCount

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

getArguments, getFirstElement, getFirstElementIncludingBlocks, isLeftAssociative, isToBeParenthesized, precedes, reuseSignature

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

compatibleBlockSize, computeHashCode, equals, equalsModRenaming, getArrayPos, match, matchChildren

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

getComments, hashCode, prettyPrintMain

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

getEndPosition, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString, 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, match

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

equalsModRenaming, getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getPositionInfo, getRelativePosition, getStartPosition

Field Detail

dimensions

protected final int dimensions

Dimensions.

arrayInitializer

protected final ArrayInitializer arrayInitializer

Array initializer.

keyJavaType

private final KeYJavaType keyJavaType

the key java type of this array

Constructor Detail

NewArray

public NewArray(ExtList children,
                KeYJavaType keyJavaType,
                ArrayInitializer init,
                int dimensions)

New array.

Parameters:

children - an ExtList with the children of this node (remove the ArrayInitializer out of the list).

init - the arrayInitializer

dimensions - an int value.

NewArray

public NewArray(Expression[] arguments,
                TypeReference typeRef,
                KeYJavaType keyJavaType,
                ArrayInitializer init,
                int dimensions)

New array.

Parameters:

arguments - an array of expressions describing the dimensions

typeRef - a reference to the arraytype

init - the arrayInitializer

dimensions - an int value.

Method Detail

getLastElement

public SourceElement getLastElement()

Description copied from class: JavaSourceElement

Finds the source element that occurs last in the source. The default implementation returns this element, which is correct for all terminal program elements, and many non terminals such as statements and prefixed operators.

Specified by:

getLastElement in interface SourceElement

Overrides:

getLastElement in class Operator

Returns:

the last source element in the syntactical representation of this element, may be equals to this element.

See Also:

JavaSourceElement.toSource(), JavaSourceElement.getEndPosition()

getArity

public int getArity()

Get arity.

Specified by:

getArity in class Operator

Returns:

the int value.

getPrecedence

public int getPrecedence()

Get precedence.

Specified by:

getPrecedence in class Operator

Returns:

the int value.

getNotation

public int getNotation()

Get notation.

Specified by:

getNotation in class Operator

Returns:

the int value.

getDimensions

public int getDimensions()

Get dimensions.

Returns:

the int value.

getArrayInitializer

public ArrayInitializer getArrayInitializer()

Get array initializer.

Returns:

the array initializer.

getChildCount

public int getChildCount()

Returns the number of children of this node.

Specified by:

getChildCount in interface NonTerminalProgramElement

Overrides:

getChildCount in class Operator

Returns:

an int giving the number of children of this node

getChildAt

public ProgramElement getChildAt(int index)

Returns the child at the specified index in this node's "virtual" child array

Specified by:

getChildAt in interface NonTerminalProgramElement

Overrides:

getChildAt in class Operator

Parameters:

index - an index into this node's "virtual" child array

Returns:

the program element at the given position

Throws:

java.lang.ArrayIndexOutOfBoundsException - if index is out of bounds

getExpressionCount

public int getExpressionCount()

Get the number of expressions in this container.

Specified by:

getExpressionCount in interface ExpressionContainer

Overrides:

getExpressionCount in class Operator

Returns:

the number of expressions.

getExpressionAt

public Expression getExpressionAt(int index)

Specified by:

getExpressionAt in interface ExpressionContainer

Overrides:

getExpressionAt in class Operator

visit

public void visit(Visitor v)

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

Specified by:

visit in interface SourceElement

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.

getReferencePrefix

public ReferencePrefix getReferencePrefix()

We do not have a prefix, so fake it! This way we implement ReferencePrefix

Specified by:

getReferencePrefix in interface ReferencePrefix

getKeYJavaType

public KeYJavaType getKeYJavaType(Services javaServ)

same as getKeYJavaType()

Overrides:

getKeYJavaType in class TypeOperator

getKeYJavaType

public KeYJavaType getKeYJavaType()