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.JVMIsTransientMethodBuilder;
14: import de.uka.ilkd.key.logic.Term;
15: import de.uka.ilkd.key.logic.op.Location;
16: import de.uka.ilkd.key.logic.op.SVSubstitute;
17: import de.uka.ilkd.key.logic.sort.Sort;
18: import de.uka.ilkd.key.rule.MatchConditions;
19: import de.uka.ilkd.key.rule.inst.SVInstantiations;
20:
21: /**
22: * returns a term representing the static field
23: * "de.uka.ilkd.key.javacard.KeYJCSystem.<transactionCounter>"
24: */
25: public class MetaTransactionCounter extends MetaField implements
26: Location {
27:
28: public MetaTransactionCounter() {
29: super ("#transactionCounter", true);
30: }
31:
32: public boolean isRigid(Term t) {
33: return false;
34: }
35:
36: /**
37: */
38: public Sort sort() {
39: return METASORT;
40: }
41:
42: /**
43: * checks whether the top level structure of the given @link Term
44: * is syntactically valid, given the assumption that the top level
45: * operator of the term is the same as this Operator. The
46: * assumption that the top level operator and the term are equal
47: * is NOT checked.
48: * @return true iff the top level structure of
49: * the @link Term is valid.
50: */
51: public boolean validTopLevel(Term term) {
52: // a meta operator accepts almost everything
53: return term.arity() == arity();
54: }
55:
56: /* (non-Javadoc)
57: * @see de.uka.ilkd.key.logic.op.Location#mayBeAliasedBy(de.uka.ilkd.key.logic.op.Location)
58: */
59: public boolean mayBeAliasedBy(Location loc) {
60: return true;
61: }
62:
63: /** (non-Javadoc)
64: * by default meta operators do not match anything
65: * @see de.uka.ilkd.key.logic.op.Operator
66: * #match(SVSubstitute,
67: * de.uka.ilkd.key.rule.MatchConditions,
68: * de.uka.ilkd.key.java.Services)
69: */
70: public MatchConditions match(SVSubstitute subst,
71: MatchConditions mc, Services services) {
72: return null;
73: }
74:
75: /** calculates the resulting term. */
76: public Term calculate(Term term, SVInstantiations svInst,
77: Services services) {
78: return termFactory
79: .createVariableTerm(services
80: .getJavaInfo()
81: .getAttribute(
82: JVMIsTransientMethodBuilder.IMPLICIT_TRANSACTION_COUNTER,
83: "de.uka.ilkd.key.javacard.KeYJCSystem"));
84: }
85:
86: }
|