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.ProgramElement;
19: import de.uka.ilkd.key.java.Services;
20: import de.uka.ilkd.key.java.reference.*;
21: import de.uka.ilkd.key.logic.Name;
22: import de.uka.ilkd.key.logic.ProgramElementName;
23: import de.uka.ilkd.key.rule.inst.SVInstantiations;
24:
25: /**
26: * The constructor call meta construct is used to handle a allocation expression
27: * like <code>new Class(...)</code>. Thereby it replaces the allocation
28: * expression by a method reference to an implict method called
29: * <code><init></code> that is mainly the constructor but in its
30: * normalform.
31: */
32: public class SpecialConstructorCall extends ProgramMetaConstruct {
33:
34: private static final ProgramElementName NORMALFORM_IDENTIFIER = new ProgramElementName(
35: de.uka.ilkd.key.java.recoderext.ConstructorNormalformBuilder.CONSTRUCTOR_NORMALFORM_IDENTIFIER);
36:
37: /**
38: * creates the metaconstruct
39: */
40: public SpecialConstructorCall(ProgramElement consRef) {
41: super (new Name("special-constructor-call"), consRef);
42: }
43:
44: /**
45: * transforms the constructor's body into its normalform and
46: * returns the result. Thereby all necessary references are
47: * resolved.
48: */
49: public ProgramElement symbolicExecution(ProgramElement pe,
50: Services services, SVInstantiations svInst) {
51:
52: SpecialConstructorReference constructorReference = (SpecialConstructorReference) pe;
53:
54: return new MethodReference(
55: constructorReference.getArguments(),
56: NORMALFORM_IDENTIFIER,
57: constructorReference instanceof ThisConstructorReference ? (ReferencePrefix) new ThisReference()
58: : (ReferencePrefix) new SuperReference());
59:
60: }
61:
62: }
|