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: //
10: package de.uka.ilkd.key.rule.metaconstruct;
11:
12: import de.uka.ilkd.key.java.Services;
13: import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder;
14: import de.uka.ilkd.key.logic.Term;
15: import de.uka.ilkd.key.rule.inst.SVInstantiations;
16:
17: /**
18: * returns a reference to <traInitialized>
19: */
20: public class MetaTraInitialized extends MetaField {
21:
22: public MetaTraInitialized() {
23: super ("#traInitialized");
24: }
25:
26: /** calculates the resulting term. */
27: public Term calculate(Term term, SVInstantiations svInst,
28: Services services) {
29: return termFactory
30: .createAttributeTerm(
31: services
32: .getJavaInfo()
33: .getAttribute(
34: ImplicitFieldAdder.IMPLICT_ARRAY_TRA_INITIALIZED,
35: services
36: .getJavaInfo()
37: .getKeYJavaType(
38: term.sub(0)
39: .sort())),
40: term.sub(0));
41: }
42:
43: }
|