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;
12:
13: import recoder.java.JavaProgramFactory;
14: import recoder.service.ConstantEvaluator;
15: import recoder.service.DefaultConstantEvaluator;
16: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
17: import de.uka.ilkd.key.java.recoderext.KeYCrossReferenceServiceConfiguration;
18:
19: public class ConstantExpressionEvaluator {
20:
21: private Services services = null;
22:
23: private ConstantEvaluator recCe = null;
24:
25: static final int BOOLEAN_TYPE = 0, BYTE_TYPE = 1, SHORT_TYPE = 2,
26: CHAR_TYPE = 3, INT_TYPE = 4, LONG_TYPE = 5, FLOAT_TYPE = 6,
27: DOUBLE_TYPE = 7, STRING_TYPE = 8;
28:
29: ConstantExpressionEvaluator(Services s) {
30: services = s;
31: }
32:
33: public Services getServices() {
34: return services;
35: }
36:
37: public boolean isCompileTimeConstant(Expression expr) {
38: return getRecoderConstantEvaluator().isCompileTimeConstant(
39: parseExpression(expr));
40:
41: }
42:
43: public boolean isCompileTimeConstant(Expression expr,
44: ConstantEvaluator.EvaluationResult result) {
45: return getRecoderConstantEvaluator().isCompileTimeConstant(
46: parseExpression(expr), result);
47:
48: }
49:
50: public KeYJavaType getCompileTimeConstantType(Expression expr) {
51: recoder.abstraction.Type javaType = getRecoderConstantEvaluator()
52: .getCompileTimeConstantType(parseExpression(expr));
53: return services.getJavaInfo().getKeYJavaType(
54: javaType.getFullName());
55: }
56:
57: private ConstantEvaluator getRecoderConstantEvaluator() {
58: if (recCe == null) {
59: KeYCrossReferenceServiceConfiguration servConf = services
60: .getJavaInfo().getKeYProgModelInfo().getServConf();
61: recCe = new DefaultConstantEvaluator(servConf);
62: }
63: return recCe;
64: }
65:
66: private recoder.java.Expression parseExpression(Expression expr) {
67: recoder.java.Expression recExpr = null;
68: try {
69: recExpr = JavaProgramFactory.getInstance().parseExpression(
70: expr.toString());
71: } catch (recoder.ParserException exc) {
72: System.err.println("Failed to parse \n" + expr
73: + "\nas Java expression!");
74: }
75: return recExpr;
76: }
77:
78: }
|