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.abstraction.KeYJavaType;
14: import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder;
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.logic.op.Location;
17: import de.uka.ilkd.key.logic.sort.Sort;
18: import de.uka.ilkd.key.parser.KeYSemanticException;
19: import de.uka.ilkd.key.rule.inst.SVInstantiations;
20:
21: /** this class implements the interface for
22: * MetaAdderators. MetaAdderators are used to do complex term
23: * transformation when applying a taclet. Often these transformation
24: * caanot be described with the taclet scheme (or trying to do so would
25: * result in a huge number of rules)
26: */
27: public class MetaCreated extends MetaField implements Location {
28:
29: public MetaCreated() {
30: super ("#created", false);
31: }
32:
33: /** calculates the resulting term.
34: * @throws KeYSemanticException */
35: public Term calculate(Term term, SVInstantiations svInst,
36: Services services) {
37:
38: final Term t = term.sub(0);
39:
40: final KeYJavaType objectKJT = services.getJavaInfo()
41: .getJavaLangObject();
42: if (!(t.sort().extendsTrans(objectKJT.getSort()))) {
43:
44: throw new RuntimeException(
45: "Error:"
46: + this
47: + ". Rules have to ensure that"
48: + "this meta operator is only applied on subtypes of java.lang.Object"
49: + ", but this is of type " + t.sort());
50: }
51:
52: return termFactory.createAttributeTerm(services.getJavaInfo()
53: .getAttribute(ImplicitFieldAdder.IMPLICIT_CREATED,
54: objectKJT), t);
55: }
56:
57: public boolean mayBeAliasedBy(Location loc) {
58: return true;
59: }
60:
61: public Sort sort() {
62: return METASORT;
63: }
64:
65: }
|