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:
11: package de.uka.ilkd.key.rule;
12:
13: import de.uka.ilkd.key.java.Services;
14: import de.uka.ilkd.key.logic.Constraint;
15: import de.uka.ilkd.key.logic.PosInOccurrence;
16:
17: /**
18: * A subclass of <code>NoPosTacletApp</code> for the special case of a
19: * taclet app without any instantiations. The method
20: * <code>setupMatchConditions</code> is overwritten to avoid object
21: * creations.
22: */
23: class UninstantiatedNoPosTacletApp extends NoPosTacletApp {
24:
25: /**
26: * @param taclet
27: */
28: UninstantiatedNoPosTacletApp(Taclet taclet) {
29: super (taclet);
30: }
31:
32: /* (non-Javadoc)
33: * @see de.uka.ilkd.key.rule.NoPosTacletApp#setupMatchConditions(de.uka.ilkd.key.logic.PosInOccurrence, de.uka.ilkd.key.java.Services, de.uka.ilkd.key.logic.Constraint)
34: */
35: protected MatchConditions setupMatchConditions(PosInOccurrence pos,
36: Services services, Constraint userConstraint) {
37: if (taclet() instanceof RewriteTaclet)
38: return ((RewriteTaclet) taclet()).checkUpdatePrefix(pos,
39: MatchConditions.EMPTY_MATCHCONDITIONS, services,
40: userConstraint);
41:
42: return MatchConditions.EMPTY_MATCHCONDITIONS;
43: }
44: }
|