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.java.expression;
12:
13: import de.uka.ilkd.key.java.*;
14: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
15: import de.uka.ilkd.key.java.reference.ExecutionContext;
16: import de.uka.ilkd.key.rule.MatchConditions;
17: import de.uka.ilkd.key.util.Debug;
18: import de.uka.ilkd.key.util.ExtList;
19:
20: /**
21: * Literal.
22: * @author <TT>AutoDoc</TT>
23: */
24:
25: public abstract class Literal extends JavaProgramElement implements
26: Expression, TerminalProgramElement {
27:
28: /**
29: * Constructor for the transformation of COMPOST ASTs to KeY.
30: * @param children the children of this AST element as KeY classes.
31: * May contain: Comments
32: */
33: public Literal(ExtList children) {
34: super (children);
35: }
36:
37: /**
38: * Literal
39: */
40: public Literal() {
41:
42: }
43:
44: /** retrieves the literal's type (as it is independant of the
45: * execution context, it is same as using {@link #getKeYJavaType(Services)})
46: * @param javaServ the Services offering access to the Java model
47: * @param ec the ExecutionContext in which the expression is evaluated
48: * @return the literal's type
49: */
50: public KeYJavaType getKeYJavaType(Services javaServ,
51: ExecutionContext ec) {
52: return getKeYJavaType(javaServ);
53: }
54:
55: /** retrieves the literal's type
56: * @param javaServ the Services offering access to the Java model
57: * @return the literal's type
58: */
59: public abstract KeYJavaType getKeYJavaType(Services javaServ);
60:
61: public MatchConditions match(SourceData source,
62: MatchConditions matchCond) {
63: final ProgramElement src = source.getSource();
64: if (this .equals(src)) {
65: source.next();
66: return matchCond;
67: } else {
68: Debug.out("Program match failed (pattern, source)", this,
69: src);
70: return null;
71: }
72: }
73:
74: }
|