de.uka.ilkd.key.rule.metaconstruct

Class InitArray

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.rule.metaconstruct.ProgramTransformer

de.uka.ilkd.key.rule.metaconstruct.InitArray

All Implemented Interfaces:

Expression, ExpressionContainer, ModelElement, NamedModelElement, NamedProgramElement, NonTerminalProgramElement, ProgramElement, Reference, MemberReference, NameReference, PackageReferenceContainer, ReferencePrefix, ReferenceSuffix, TypeReference, TypeReferenceContainer, TypeReferenceInfix, SourceElement, Statement, StatementContainer, SVSubstitute

Direct Known Subclasses:

InitArrayCreation

public abstract class InitArray
extends ProgramTransformer

Split an array creation expression with explicit array initializer, creating a creation expression with dimension expression and a list of assignments (-> Java language specification, 15.10)

Constructor Summary

Constructors

Constructor and Description
InitArray(java.lang.String name, ProgramElement body)

Method Summary

Modifier and Type	Method and Description
protected void	createArrayAssignments(int p_start, Statement[] p_statements, ProgramVariable[] p_initializers, ReferencePrefix p_array, NewArray p_creationExpression) Convert the variable initializers to assignments to the array elements (the initializers may itself be array initializers, in which case valid creation expressions are created by inserting the new-operator)
protected Expression	createArrayCreation(NewArray p_creationExpression) Create an array creation expression for an array of the size given by the array initializer
protected Statement	createAssignment(ReferencePrefix p_array, int p_index, Expression p_initializer, KeYJavaType p_elementType, TypeReference p_baseType) Convert one variable initializers to an assignment to the appropriate array element (the initializer may itself be an array initializer, in which case a valid creation expression is created by inserting the new-operator)
protected ProgramVariable[]	evaluateInitializers(Statement[] p_stmnts, NewArray p_creationExpression, Services services) The variable initializers have to be evaluated and assigned to temporary variables (the initializers may itself be array initializers, in which case valid creation expressions are created by inserting the new-operator)
protected ImmutableArray<Expression>	extractInitializers(NewArray p_creationExpression) Extract the variable initializers from the array initializer
protected KeYJavaType	getElementType(NewArray p_creationExpression)

Methods inherited from class de.uka.ilkd.key.rule.metaconstruct.ProgramTransformer

body, getChildAt, getChildCount, getDimensions, getExpressionAt, getExpressionCount, getKeYJavaType, getKeYJavaType, getKeYJavaType, getLastElement, getName, getPackageReference, getProgramElementName, getReferencePrefix, getStatementAt, getStatementCount, getTypeReferenceAt, getTypeReferenceCount, name, neededInstantiations, needs, prettyPrint, setReferencePrefix, toString, transform, visit

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, reuseSignature

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

getEndPosition, getFirstElement, getFirstElementIncludingBlocks, 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, match

Constructor Detail

InitArray

public InitArray(java.lang.String name,
                 ProgramElement body)

Method Detail

extractInitializers

protected ImmutableArray<Expression> extractInitializers(NewArray p_creationExpression)

Extract the variable initializers from the array initializer

getElementType

protected KeYJavaType getElementType(NewArray p_creationExpression)

createArrayCreation

protected Expression createArrayCreation(NewArray p_creationExpression)

Create an array creation expression for an array of the size given by the array initializer

evaluateInitializers

protected ProgramVariable[] evaluateInitializers(Statement[] p_stmnts,
                                                 NewArray p_creationExpression,
                                                 Services services)

The variable initializers have to be evaluated and assigned to temporary variables (the initializers may itself be array initializers, in which case valid creation expressions are created by inserting the new-operator)

createArrayAssignments

protected void createArrayAssignments(int p_start,
                                      Statement[] p_statements,
                                      ProgramVariable[] p_initializers,
                                      ReferencePrefix p_array,
                                      NewArray p_creationExpression)

Convert the variable initializers to assignments to the array elements (the initializers may itself be array initializers, in which case valid creation expressions are created by inserting the new-operator)

createAssignment

protected Statement createAssignment(ReferencePrefix p_array,
                                     int p_index,
                                     Expression p_initializer,
                                     KeYJavaType p_elementType,
                                     TypeReference p_baseType)

Convert one variable initializers to an assignment to the appropriate array element (the initializer may itself be an array initializer, in which case a valid creation expression is created by inserting the new-operator)