01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: // This file is part of KeY - Integrated Deductive Software Design
10: // Copyright (C) 2001-2004 Universitaet Karlsruhe, Germany
11: // Universitaet Koblenz-Landau, Germany
12: // Chalmers University of Technology, Sweden
13: //
14: // The KeY system is protected by the GNU General Public License.
15: // See LICENSE.TXT for details.
16: package de.uka.ilkd.key.rule.metaconstruct;
17:
18: import de.uka.ilkd.key.java.ArrayOfExpression;
19: import de.uka.ilkd.key.java.ProgramElement;
20: import de.uka.ilkd.key.java.Services;
21: import de.uka.ilkd.key.java.declaration.ClassDeclaration;
22: import de.uka.ilkd.key.java.expression.operator.New;
23: import de.uka.ilkd.key.java.recoderext.CreateObjectBuilder;
24: import de.uka.ilkd.key.java.reference.MethodReference;
25: import de.uka.ilkd.key.java.reference.TypeReference;
26: import de.uka.ilkd.key.logic.ProgramElementName;
27: import de.uka.ilkd.key.rule.inst.SVInstantiations;
28:
29: /**
30: * If an allocation expression <code>new Class(...)</code> occurs, a new object
31: * has to be created, in KeY this is quite similar to take it out of a list of
32: * objects and setting the implicit flag <code> <created> </code> to
33: * <code>true</code> as well as setting all fields of the object to their
34: * default values. For the complete procedure, the method creates the
35: * implicit method <code><createObject></code> which on its part calls
36: * another implicit method <code>lt;prepare></code> for setting the fields
37: * values.
38: */
39: public class CreateObject extends ProgramMetaConstruct {
40:
41: public CreateObject(ProgramElement newExpr) {
42: super ("create-object", newExpr);
43: }
44:
45: /**
46: * creates and returns a method reference to the implicit '<createObject>'
47: * method
48: */
49: public ProgramElement symbolicExecution(ProgramElement pe,
50: Services services, SVInstantiations svInst) {
51:
52: TypeReference classReference = ((New) pe).getTypeReference();
53:
54: if (!(classReference.getKeYJavaType().getJavaType() instanceof ClassDeclaration)) {
55: // no implementation available
56: return pe;
57: }
58:
59: return new MethodReference(new ArrayOfExpression(),
60: new ProgramElementName(
61: CreateObjectBuilder.IMPLICIT_OBJECT_CREATE),
62: classReference);
63: }
64: }
|