001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: package de.uka.ilkd.key.java;
010:
011: import java.util.LinkedList;
012:
013: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
014: import de.uka.ilkd.key.java.abstraction.ListOfField;
015: import de.uka.ilkd.key.java.declaration.*;
016: import de.uka.ilkd.key.java.declaration.modifier.Private;
017: import de.uka.ilkd.key.java.declaration.modifier.Protected;
018: import de.uka.ilkd.key.java.declaration.modifier.Static;
019: import de.uka.ilkd.key.java.recoderext.InstanceAllocationMethodBuilder;
020: import de.uka.ilkd.key.java.reference.MethodReference;
021: import de.uka.ilkd.key.java.reference.TypeRef;
022: import de.uka.ilkd.key.java.reference.TypeReference;
023: import de.uka.ilkd.key.java.statement.Return;
024: import de.uka.ilkd.key.logic.ProgramElementName;
025: import de.uka.ilkd.key.logic.op.LocationVariable;
026: import de.uka.ilkd.key.logic.op.ProgramMethod;
027: import de.uka.ilkd.key.logic.op.ProgramVariable;
028:
029: /**
030: * This class creates the <code><createArray></code> method for
031: * array creation and in particular its helper method
032: * <code><createArrayHelper></code>. This class hould be replaced
033: * by a recoder transformation as soon as we port our array data
034: * structures to RecodeR.
035: */
036: public class CreateTransientArrayMethodBuilder extends
037: CreateArrayMethodBuilder {
038:
039: /** current type for byte */
040: private final KeYJavaType byteType;
041:
042: /** create the method builder for transient array implict creation methods */
043: public CreateTransientArrayMethodBuilder(KeYJavaType integerType,
044: KeYJavaType objectType, KeYJavaType byteType) {
045: super (integerType, objectType);
046: this .byteType = byteType;
047: }
048:
049: /**
050: * create the method declaration of the
051: * <code><createArrayHelper></code> method for transient arrays
052: */
053: public ProgramMethod getCreateTransientArrayHelperMethod(
054: TypeReference arrayTypeReference, ProgramVariable length,
055: ListOfField fields) {
056:
057: final Modifier[] modifiers = new Modifier[] { new Private() };
058: final KeYJavaType arrayType = arrayTypeReference
059: .getKeYJavaType();
060:
061: final ProgramVariable pvLength = new LocationVariable(
062: new ProgramElementName("length"), integerType);
063:
064: final ProgramVariable pvTransientType = new LocationVariable(
065: new ProgramElementName("event"), integerType);
066:
067: final ParameterDeclaration param = new ParameterDeclaration(
068: new Modifier[0], new TypeRef(integerType),
069: new VariableSpecification(pvLength), false);
070:
071: final ParameterDeclaration paramTransientType = new ParameterDeclaration(
072: new Modifier[0], new TypeRef(integerType),
073: new VariableSpecification(pvTransientType), false);
074:
075: final MethodDeclaration md = new MethodDeclaration(
076: modifiers,
077: arrayTypeReference,
078: new ProgramElementName(
079: IMPLICIT_ARRAY_TRANSIENT_CREATION_HELPER),
080: new ParameterDeclaration[] { param, paramTransientType },
081: null, getCreateArrayHelperBody(length, pvLength,
082: fields, true, pvTransientType), false);
083:
084: return new ProgramMethod(md, arrayType, arrayType,
085: PositionInfo.UNDEFINED);
086: }
087:
088: private StatementBlock getCreateTransientArrayBody(
089: TypeReference arrayRef, ProgramVariable paramLength,
090: ProgramVariable paramTransientType) {
091:
092: final LocalVariableDeclaration local = declare(
093: new ProgramElementName("newObject"), arrayRef);
094: final ProgramVariable newObject = (ProgramVariable) local
095: .getVariables().getVariableSpecification(0)
096: .getProgramVariable();
097: final LinkedList body = new LinkedList();
098:
099: body.addLast(local);
100:
101: body
102: .addLast(assign(
103: newObject,
104: new MethodReference(
105: new ArrayOfExpression(
106: new Expression[] {}),
107: new ProgramElementName(
108: InstanceAllocationMethodBuilder.IMPLICIT_INSTANCE_ALLOCATE),
109: arrayRef)));
110:
111: body.add(new MethodReference(new ArrayOfExpression(
112: new Expression[] { paramLength, paramTransientType }),
113: new ProgramElementName(
114: IMPLICIT_ARRAY_TRANSIENT_CREATION_HELPER),
115: newObject));
116:
117: body.add(new Return(newObject));
118:
119: return new StatementBlock((Statement[]) body
120: .toArray(new Statement[body.size()]));
121: }
122:
123: /**
124: * create the implicit creation method
125: * <code>createTransientArray</code>
126: */
127: public ProgramMethod getCreateTransientArrayMethod(
128: TypeReference arrayTypeReference, ProgramVariable length,
129: ProgramMethod prepare, ListOfField fields) {
130:
131: final Modifier[] modifiers = new Modifier[] { new Protected(),
132: new Static() };
133:
134: final KeYJavaType arrayType = arrayTypeReference
135: .getKeYJavaType();
136:
137: final ProgramVariable pvLength = new LocationVariable(
138: new ProgramElementName("length"), integerType);
139:
140: final ProgramVariable pvTransientType = (new LocationVariable(
141: new ProgramElementName("event"), byteType));
142:
143: final ParameterDeclaration paramLength = new ParameterDeclaration(
144: new Modifier[0], new TypeRef(integerType),
145: new VariableSpecification(pvLength), false);
146:
147: final ParameterDeclaration transientType = new ParameterDeclaration(
148: new Modifier[0], new TypeRef(byteType),
149: new VariableSpecification(pvTransientType), false);
150:
151: final MethodDeclaration md = new MethodDeclaration(
152: modifiers,
153: arrayTypeReference,
154: new ProgramElementName(IMPLICIT_ARRAY_CREATE_TRANSIENT),
155: new ParameterDeclaration[] { paramLength, transientType },
156: null, getCreateTransientArrayBody(arrayTypeReference,
157: pvLength, pvTransientType), false);
158:
159: return new ProgramMethod(md, arrayType, arrayType,
160: PositionInfo.UNDEFINED);
161: }
162: }
|