public class InitArrayCreation extends InitArray
Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
createArrayName |
private SchemaVariable |
newObjectSV |
Constructor and Description |
---|
InitArrayCreation(SchemaVariable newObjectSV,
ProgramElement newExpr) |
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
|
createArrayAssignments, createArrayCreation, createAssignment, evaluateInitializers, extractInitializers, getElementType
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
compatibleBlockSize, computeHashCode, equals, equalsModRenaming, getArrayPos, match, matchChildren
getComments, hashCode, prettyPrintMain, reuseSignature
getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
getComments, match
private final SchemaVariable newObjectSV
private static final java.lang.String createArrayName
public InitArrayCreation(SchemaVariable newObjectSV, ProgramElement newExpr)
private If checkNegativeDimension(Expression cond, Services services)
NegativeArraySizeException
to be thrown. The if
statement implementing this behaviour is created by this method.cond
- the Expression representing the guard checking if the given
length is negative or notservices
- the Services offering access to the type modelprivate ProgramVariable[] evaluateAndCheckDimensionExpressions(java.util.LinkedList<Statement> bodyStmnts, ImmutableArray<Expression> dimExpr, Services services)
bodyStmnts
- the LinkedList of statements where the new statements are
inserteddimExpr
- the ArrayOfservices
- the Services objectprivate void createNDimensionalArray(java.util.LinkedList<Statement> bodyStmnts, Expression resultVar, KeYJavaType arrayType, ProgramVariable[] dimensions, Services services)
dimensions.length
private ProgramElement arrayCreationWithoutInitializers(Expression newObject, NewArray na, Services services)
public ProgramElement[] transform(ProgramElement pe, Services services, SVInstantiations svInst)
ProgramTransformer
transform
in class ProgramTransformer
pe
- the ProgramElement on which the execution is performedservices
- the Services with all necessary information
about the java programssvInst
- the instantiations of the schemavariables