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: //
010: //
011: //
012:
013: package de.uka.ilkd.key.rule.metaconstruct;
014:
015: import de.uka.ilkd.key.java.ArrayOfExpression;
016: import de.uka.ilkd.key.java.Expression;
017: import de.uka.ilkd.key.java.ProgramElement;
018: import de.uka.ilkd.key.java.Services;
019: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
020: import de.uka.ilkd.key.java.expression.PassiveExpression;
021: import de.uka.ilkd.key.java.recoderext.ClassInitializeMethodBuilder;
022: import de.uka.ilkd.key.java.reference.ExecutionContext;
023: import de.uka.ilkd.key.java.reference.FieldReference;
024: import de.uka.ilkd.key.java.reference.MethodReference;
025: import de.uka.ilkd.key.java.reference.TypeRef;
026: import de.uka.ilkd.key.logic.ProgramElementName;
027: import de.uka.ilkd.key.logic.op.ProgramMethod;
028: import de.uka.ilkd.key.logic.op.ProgramVariable;
029: import de.uka.ilkd.key.rule.inst.SVInstantiations;
030: import de.uka.ilkd.key.util.Debug;
031:
032: public class StaticInitialisation extends ProgramMetaConstruct {
033:
034: public StaticInitialisation(Expression expr) {
035: super ("static-initialisation", expr);
036:
037: }
038:
039: /** performs the program transformation needed for symbolic
040: * program transformation
041: * @return the transformated program
042: */
043: public ProgramElement symbolicExecution(ProgramElement pe,
044: Services services, SVInstantiations insts) {
045: KeYJavaType typeToBeInitialised = null;
046: if (pe instanceof FieldReference) {
047: final ProgramVariable pv = ((FieldReference) pe)
048: .getProgramVariable();
049: if (pv.isStatic()) {
050: typeToBeInitialised = pv.getContainerType();
051: } else {
052: return null; // no static initialisation necessary
053: }
054: } else if (pe instanceof ProgramVariable) {
055: final ProgramVariable pv = (ProgramVariable) pe;
056: if (pv.isStatic()) {
057: typeToBeInitialised = pv.getContainerType();
058: } else {
059: return null; // no static initialisation necessary
060: }
061: } else if (pe instanceof MethodReference) {
062: final MethodReference mr = (MethodReference) pe;
063: final ExecutionContext ec = insts.getContextInstantiation()
064: .activeStatementContext();
065: final ProgramMethod m;
066: final KeYJavaType mrPrefixType = mr
067: .determineStaticPrefixType(services, ec);
068: if (ec == null) {
069: // in this case we are at the top level of a diamond
070: // in this case we assume as scope the type of the method prefix
071: m = mr.method(services, mrPrefixType, mr
072: .getMethodSignature(services, null),
073: mrPrefixType);
074: } else {
075: m = mr.method(services, mr.determineStaticPrefixType(
076: services, ec), ec);
077: }
078: if (m != null) {
079: if (m.isStatic()) {
080: typeToBeInitialised = m.getContainerType();
081: } else {
082: return null; // no static initialisation necessary
083: }
084: }
085:
086: } else {
087: // at the moment the 'new' case is catched via static method
088: // call of <createObject>
089: Debug
090: .fail("static initialisation: Unexpected case in static initialisation.");
091: }
092:
093: if (typeToBeInitialised == null) {
094: Debug.fail("static initialisation failed");
095: return null;
096: }
097:
098: return new PassiveExpression(
099: new MethodReference(
100: new ArrayOfExpression(),
101: new ProgramElementName(
102: ClassInitializeMethodBuilder.CLASS_INITIALIZE_IDENTIFIER),
103: new TypeRef(typeToBeInitialised)));
104: }
105: }
|