public final class CreateArrayMethodBuilder extends KeYJavaASTFactory
<createArray>
method for array
creation and in particular its helper method
<createArrayHelper>
. This class should be replaced by a
recoder transformation as soon as we port our array data structures to
RecodeR.Modifier and Type | Field and Description |
---|---|
private java.util.Map<java.lang.String,ProgramVariable> |
cache |
private int |
heapCount |
private Sort |
heapSort |
static java.lang.String |
IMPLICIT_ARRAY_CREATE |
static java.lang.String |
IMPLICIT_ARRAY_CREATION_HELPER |
private KeYJavaType |
integerType
keeps the currently used integer type
|
private KeYJavaType |
objectType
stores the currently used object type
|
Constructor and Description |
---|
CreateArrayMethodBuilder(KeYJavaType integerType,
KeYJavaType objectType,
Sort heapSort,
int heapCount)
create the method builder for array implict creation methods
|
Modifier and Type | Method and Description |
---|---|
protected java.util.List<Statement> |
createArray(ImmutableList<Field> fields)
creates the statements which take the next object out of the list of
available objects
|
protected ImmutableList<Field> |
filterField(FieldDeclaration field)
extracts all fields out of fielddeclaration
|
protected ImmutableList<Field> |
filterField(ImmutableArray<MemberDeclaration> list)
extracts all field specifications out of the given list.
|
protected ImmutableList<Field> |
filterImplicitFields(ImmutableList<Field> list)
extracts all implicit field specifications out of the given list
|
protected ProgramVariable |
find(java.lang.String name,
ImmutableList<Field> fields)
retrieves a field with the given name out of the list
|
protected ProgramVariable |
findInObjectFields(java.lang.String name) |
IProgramMethod |
getArrayInstanceAllocatorMethod(TypeReference arrayTypeReference)
creates the implicit method
<allocate> which is a
stump and given meaning by a contract |
protected StatementBlock |
getCreateArrayBody(TypeReference arrayRef,
ProgramVariable paramLength) |
protected StatementBlock |
getCreateArrayHelperBody(ProgramVariable length,
ImmutableList<Field> fields,
boolean createTransient,
ProgramVariable transientType)
creates the body of method
<createArrayHelper(int
paramLength)>
therefore it first adds the statements responsible to take the correct
one out of the list, then the arrays length attribute is set followed by
a call to <prepare>() setting the arrays fields on
their default value. |
IProgramMethod |
getCreateArrayHelperMethod(TypeReference arrayTypeReference,
ProgramVariable length,
ImmutableList<Field> fields)
create the method declaration of the
<createArrayHelper> method |
IProgramMethod |
getCreateArrayMethod(TypeReference arrayTypeReference,
IProgramMethod prepare,
ImmutableList<Field> fields)
creates the implicit method
<createArray> it
fulfills a similar purpose as <createObject> in
addition it sets the arrays length and calls the prepare method |
protected Expression |
getDefaultValue(Type type)
returns the default value of the given type according to JLS \S 4.5.5
|
IProgramMethod |
getPrepareArrayMethod(TypeRef arrayRef,
ProgramVariable length,
Expression defaultValue,
ImmutableList<Field> fields)
returns the prepare method for arrays initialising all array fields with
their default value
|
arrayFieldAccess, arrayInitializer, arrayLength, assign, assign, assign, assignArrayField, attribute, block, block, block, breakStatement, breakStatement, caseBlock, caseBlock, caseBlock, cast, catchClause, catchClause, catchClause, catchClause, catchClause, continueStatement, declare, declare, declare, declare, declare, declare, declare, declare, declare, declare, declare, declare, declare, declare, declare, declare, declare, declareMethodCall, declareMethodCall, declareZero, defaultBlock, defaultBlock, defaultBlock, doLoop, elseBlock, elseBlock, elseBlock, emptyStatement, enhancedForLoop, equalsNullOperator, equalsOperator, equalsOperator, executionContext, falseLiteral, fieldReference, fieldReference, finallyBlock, finallyBlock, finallyBlock, finallyBlock, forLoop, forLoop, forLoop, forLoop, forUpdates, ifElse, ifElse, ifStatement, ifThen, ifThen, ifThen, insertStatementInBlock, insertStatementInBlock, insertStatementInBlock, insertStatementInBlock, instanceOf, intLiteral, labeledStatement, labeledStatement, labeledStatement, lessThanArrayLengthGuard, lessThanGuard, lessThanOperator, lessThanZeroOperator, localVariable, localVariable, localVariable, logicalAndOperator, logicalOrOperator, loopInit, loopInitZero, methodBody, methodBody, methodBody, methodCall, methodCall, methodCall, methodCall, methodCall, methodCall, methodCall, methodCall, methodFrame, methodFrame, methodFrame, methodFrame, newArray, newArray, newArray, newArray, newOperator, newOperator, newOperator, newOperator, notEqualsOperator, parameterDeclaration, parameterDeclaration, parameterDeclaration, parenthesizedExpression, passiveExpression, postIncrementForUpdates, returnClause, superConstructor, superReference, switchBlock, switchBlock, synchronizedBlock, thenBlock, thenBlock, thenBlock, thisConstructor, thisReference, throwClause, transactionStatement, trueGuard, trueLiteral, tryBlock, tryBlock, tryBlock, tryBlock, typeRef, typeRef, variableSpecification, variableSpecification, whileLoop, whileLoop, zeroLiteral
public static final java.lang.String IMPLICIT_ARRAY_CREATE
public static final java.lang.String IMPLICIT_ARRAY_CREATION_HELPER
private final java.util.Map<java.lang.String,ProgramVariable> cache
private final KeYJavaType integerType
private final KeYJavaType objectType
private final Sort heapSort
private final int heapCount
public CreateArrayMethodBuilder(KeYJavaType integerType, KeYJavaType objectType, Sort heapSort, int heapCount)
protected java.util.List<Statement> createArray(ImmutableList<Field> fields)
protected ImmutableList<Field> filterField(ImmutableArray<MemberDeclaration> list)
list
- the ArrayOfprotected final ImmutableList<Field> filterField(FieldDeclaration field)
field
- the FieldDeclaration of which the field specifications have to
be extractedprotected ImmutableList<Field> filterImplicitFields(ImmutableList<Field> list)
list
- the IListprotected ProgramVariable find(java.lang.String name, ImmutableList<Field> fields)
name
- a String with the name of the field to be looked forfields
- the IListprotected ProgramVariable findInObjectFields(java.lang.String name)
public IProgramMethod getArrayInstanceAllocatorMethod(TypeReference arrayTypeReference)
<allocate>
which is a
stump and given meaning by a contractprotected StatementBlock getCreateArrayBody(TypeReference arrayRef, ProgramVariable paramLength)
protected StatementBlock getCreateArrayHelperBody(ProgramVariable length, ImmutableList<Field> fields, boolean createTransient, ProgramVariable transientType)
<createArrayHelper(int
paramLength)>
therefore it first adds the statements responsible to take the correct
one out of the list, then the arrays length attribute is set followed by
a call to <prepare>()
setting the arrays fields on
their default value.length
- the final public ProgramVariable
length of the array
fields
- the IListcreateTransient
- a boolean indicating if a transient array has
to be created (this is special to JavaCard)transientType
- a ProgramVariable identifying the kind of transient
{
this. = this..;
this. = false;
this. = true;
this.();
this. = transientType;
this. = true;
return this;
}
public IProgramMethod getCreateArrayHelperMethod(TypeReference arrayTypeReference, ProgramVariable length, ImmutableList<Field> fields)
<createArrayHelper>
methodpublic IProgramMethod getCreateArrayMethod(TypeReference arrayTypeReference, IProgramMethod prepare, ImmutableList<Field> fields)
<createArray>
it
fulfills a similar purpose as <createObject>
in
addition it sets the arrays length and calls the prepare methodprotected Expression getDefaultValue(Type type)
public IProgramMethod getPrepareArrayMethod(TypeRef arrayRef, ProgramVariable length, Expression defaultValue, ImmutableList<Field> fields)