de.uka.ilkd.key.rule.metaconstruct

Class InitArrayCreation

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

de.uka.ilkd.key.rule.metaconstruct.InitArrayCreation

All Implemented Interfaces:

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

public class InitArrayCreation
extends InitArray

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) This meta construct delivers the creation expression

Field Summary

Fields

Modifier and Type	Field and Description
private static java.lang.String	createArrayName
private SchemaVariable	newObjectSV

Constructor Summary

Constructors

Constructor and Description
InitArrayCreation(SchemaVariable newObjectSV, ProgramElement newExpr)

Method Summary

Modifier and Type	Method and Description
private ProgramElement	arrayCreationWithoutInitializers(Expression newObject, NewArray na, Services services) executes an array creation without initializers involved
private If	checkNegativeDimension(Expression cond, Services services) trying to create an array of negative length causes a NegativeArraySizeException to be thrown.
private void	createNDimensionalArray(java.util.LinkedList<Statement> bodyStmnts, Expression resultVar, KeYJavaType arrayType, ProgramVariable[] dimensions, Services services) creates an array of dimension dimensions.length
private ProgramVariable[]	evaluateAndCheckDimensionExpressions(java.util.LinkedList<Statement> bodyStmnts, ImmutableArray<Expression> dimExpr, Services services) creates statements for evaluation of the dimension expressions, check if a dimension is non-negative and adds them to given list of statements.
ProgramElement[]	transform(ProgramElement pe, Services services, SVInstantiations svInst) performs the program transformation needed for symbolic program transformation

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

createArrayAssignments, createArrayCreation, createAssignment, evaluateInitializers, extractInitializers, getElementType

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

Field Detail

newObjectSV

private final SchemaVariable newObjectSV

createArrayName

private static final java.lang.String createArrayName

See Also:

Constant Field Values

Constructor Detail

InitArrayCreation

public InitArrayCreation(SchemaVariable newObjectSV,
                         ProgramElement newExpr)

Method Detail

checkNegativeDimension

private If checkNegativeDimension(Expression cond,
                                  Services services)

trying to create an array of negative length causes a NegativeArraySizeException to be thrown. The if statement implementing this behaviour is created by this method.

Parameters:

cond - the Expression representing the guard checking if the given length is negative or not

services - the Services offering access to the type model

Returns:

an if statement throwing a NegativeArraySizeException if cond is evaluated to false

evaluateAndCheckDimensionExpressions

private ProgramVariable[] evaluateAndCheckDimensionExpressions(java.util.LinkedList<Statement> bodyStmnts,
                                                               ImmutableArray<Expression> dimExpr,
                                                               Services services)

creates statements for

1. evaluation of the dimension expressions,
3. check if a dimension is non-negative

and adds them to given list of statements. Further more the new declared program variables initialised with the evaluated dimension expressions are returned

Parameters:

bodyStmnts - the LinkedList of statements where the new statements are inserted

dimExpr - the ArrayOf which describe the array's dimensions

services - the Services object

createNDimensionalArray

private void createNDimensionalArray(java.util.LinkedList<Statement> bodyStmnts,
                                     Expression resultVar,
                                     KeYJavaType arrayType,
                                     ProgramVariable[] dimensions,
                                     Services services)

creates an array of dimension dimensions.length

arrayCreationWithoutInitializers

private ProgramElement arrayCreationWithoutInitializers(Expression newObject,
                                                        NewArray na,
                                                        Services services)

executes an array creation without initializers involved

transform

public ProgramElement[] transform(ProgramElement pe,
                                  Services services,
                                  SVInstantiations svInst)

Description copied from class: ProgramTransformer

performs the program transformation needed for symbolic program transformation

Specified by:

transform in class ProgramTransformer

Parameters:

pe - the ProgramElement on which the execution is performed

services - the Services with all necessary information about the java programs

svInst - the instantiations of the schemavariables

Returns:

the transformated program