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: // This file is part of KeY - Integrated Deductive Software Design
010: // Copyright (C) 2001-2004 Universitaet Karlsruhe, Germany
011: // Universitaet Koblenz-Landau, Germany
012: // Chalmers University of Technology, Sweden
013: //
014: // The KeY system is protected by the GNU General Public License.
015: // See LICENSE.TXT for details.
016: package de.uka.ilkd.key.java.recoderext;
017:
018: import recoder.CrossReferenceServiceConfiguration;
019: import recoder.java.CompilationUnit;
020: import recoder.java.Identifier;
021: import recoder.java.StatementBlock;
022: import recoder.java.declaration.ClassDeclaration;
023: import recoder.java.declaration.MethodDeclaration;
024: import recoder.java.declaration.ParameterDeclaration;
025: import recoder.java.declaration.TypeDeclaration;
026: import recoder.java.declaration.modifier.Public;
027: import recoder.java.reference.*;
028: import recoder.java.statement.Return;
029: import recoder.list.*;
030:
031: /**
032: */
033: public class JVMIsTransientMethodBuilder extends
034: RecoderModelTransformer {
035:
036: public static final String IMPLICIT_JVM_IS_TRANSIENT = "<jvmIsTransient>";
037:
038: public static final String IMPLICIT_TRANSACTION_COUNTER = "<transactionCounter>";
039:
040: private boolean alreadyTransformed = false;
041:
042: public JVMIsTransientMethodBuilder(
043: CrossReferenceServiceConfiguration services,
044: CompilationUnitMutableList units) {
045: super (services, units);
046: }
047:
048: private ReferencePrefix createJavaLangPrefix() {
049: return new PackageReference(new PackageReference(
050: new Identifier("java")), new Identifier("lang"));
051: }
052:
053: /**
054: * creates the implicit <code><jvmIsTransient>(Object obj);</code>
055: * method
056: * @param type the TypeDeclaration
057: * @return the implicit method
058: */
059: public MethodDeclaration createMethod(ClassDeclaration type) {
060: ParameterDeclaration paramDecl = new ParameterDeclaration(
061: new TypeReference(createJavaLangPrefix(),
062: new Identifier("Object")),
063: new Identifier("obj"));
064:
065: StatementMutableList body = new StatementArrayList(2);
066:
067: body.add(new Return(new FieldReference(new VariableReference(
068: new Identifier("obj")), new ImplicitIdentifier(
069: ImplicitFieldAdder.IMPLICIT_TRANSIENT))));
070:
071: ModifierMutableList modifiers = new ModifierArrayList(2);
072: modifiers.add(new Public());
073:
074: ParameterDeclarationMutableList params = new ParameterDeclarationArrayList(
075: 1);
076: params.add(paramDecl);
077:
078: MethodDeclaration md = new MethodDeclaration(modifiers,
079: new TypeReference(new Identifier("int")),
080: new ImplicitIdentifier(IMPLICIT_JVM_IS_TRANSIENT),
081: params, null, new StatementBlock(body));
082:
083: md.makeAllParentRolesValid();
084: return md;
085: }
086:
087: /**
088: * entry method for the constructor normalform builder
089: * @param td the TypeDeclaration
090: */
091: protected void makeExplicit(TypeDeclaration td) {
092: if (alreadyTransformed)
093: return;
094: if ("KeYJCSystem".equals(td.getName())) {
095:
096: PackageReference pr = td.getASTParent() instanceof CompilationUnit ? ((CompilationUnit) td
097: .getASTParent()).getPackageSpecification()
098: .getPackageReference()
099: : null;
100: String[] keyJavaCard = { "de", "uka", "ilkd", "key",
101: "javacard" };
102: PackageReference prefix = pr;
103: boolean res = true;
104: for (int i = keyJavaCard.length - 1; i >= 0; i--) {
105: if (prefix == null
106: || !keyJavaCard[i].equals(prefix.getName())) {
107: res = false;
108: break;
109: }
110: prefix = (PackageReference) prefix.getReferencePrefix();
111: }
112: if (res) {
113: attach(ImplicitFieldAdder
114: .createImplicitRecoderField("int",
115: IMPLICIT_TRANSACTION_COUNTER, true,
116: true), td, 0);
117: attach(createMethod((ClassDeclaration) td), td, td
118: .getMembers().size());
119: alreadyTransformed = true;
120: }
121: }
122: }
123:
124: }
|