001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.java;
012:
013: import java.io.IOException;
014:
015: import de.uka.ilkd.key.java.annotation.Annotation;
016: import de.uka.ilkd.key.java.reference.ExecutionContext;
017: import de.uka.ilkd.key.rule.MatchConditions;
018: import de.uka.ilkd.key.util.Debug;
019: import de.uka.ilkd.key.util.ExtList;
020:
021: /**
022: * Top level implementation of a Java {@link ProgramElement}.
023: * taken from COMPOST and changed to achieve an immutable structure
024: */
025: public abstract class JavaProgramElement extends JavaSourceElement
026: implements ProgramElement {
027:
028: private final static Comment[] NO_COMMENTS = new Comment[0];
029: /**
030: * Comments.
031: */
032:
033: private final Comment[] comments;
034:
035: /**
036: * Java program element.
037: */
038:
039: public JavaProgramElement() {
040: comments = NO_COMMENTS;
041: }
042:
043: /**
044: * Java program element.
045: * @param list ExtList with comments
046: */
047: public JavaProgramElement(ExtList list) {
048: super (list);
049: comments = extractComments(list);
050: }
051:
052: /**
053: * creates a java program element with the given position information
054: * @param pos the PositionInfo where the Java program element occurs in
055: * the source
056: */
057: public JavaProgramElement(PositionInfo pos) {
058: super (pos);
059: comments = NO_COMMENTS;
060: }
061:
062: public JavaProgramElement(ExtList children, PositionInfo pos) {
063: super (children, pos);
064: comments = extractComments(children);
065: }
066:
067: /**
068: * collects comments contained in the given list
069: * @param list the ExtList with children and comments of this node
070: */
071: private Comment[] extractComments(ExtList list) {
072: final Comment[] c = (Comment[]) list.collect(Comment.class);
073: return c == null ? NO_COMMENTS : c;
074: }
075:
076: /**
077: * Get comments.
078: * @return the comments.
079: */
080:
081: public Comment[] getComments() {
082: return comments;
083: }
084:
085: /**
086: *@return the annotations.
087: */
088: public Annotation[] getAnnotations() {
089: return new Annotation[0];
090: }
091:
092: public int getAnnotationCount() {
093: return 0;
094: }
095:
096: /**
097: * Template Method. Prints DocComments if existing, calls
098: * prettyPrintMain and prints other Comments.
099: */
100:
101: public void prettyPrint(PrettyPrinter w) throws IOException {
102: int s = (comments != null) ? comments.length : 0;
103: int t = 0;
104: for (int i = 0; i < s; i += 1) {
105: Comment c = comments[i];
106: if (c.isPrefixed()) {
107: c.prettyPrint(w);
108: } else {
109: t += 1;
110: }
111: }
112: prettyPrintMain(w);
113: if (t > 0) {
114: for (int i = 0; i < s; i += 1) {
115: Comment c = comments[i];
116: if (!c.isPrefixed()) {
117: if (c instanceof SingleLineComment) {
118: w.scheduleComment((SingleLineComment) c);
119: } else {
120: c.prettyPrint(w);
121: }
122: }
123: }
124: }
125: }
126:
127: /**
128: * Prints main content of current node and all syntactical children.
129: * Hook method of prettyPrint; defaults to do nothing.
130: */
131: protected void prettyPrintMain(PrettyPrinter w) throws IOException {
132: }
133:
134: /** commented in interface SourceElement. The default equals
135: * method compares two elements by testing if they have the
136: * same type and calling the default equals method.
137: */
138: public boolean equalsModRenaming(SourceElement se,
139: NameAbstractionTable nat) {
140: return (this .getClass() == se.getClass());
141: }
142:
143: public int hashCode() {
144: int result = 17;
145: result = 37 * result + this .getClass().hashCode();
146: return result;
147: }
148:
149: public boolean equals(Object o) {
150: if (o == this )
151: return true;
152: if (!(o instanceof JavaProgramElement))
153: return false;
154:
155: return equalsModRenaming((JavaProgramElement) o,
156: NameAbstractionTableDisabled.INSTANCE);
157: }
158:
159: /** this is the default implementation of the signature, which is
160: * used to determine program similarity.
161: * @param ec TODO
162: */
163: public String reuseSignature(Services services, ExecutionContext ec) {
164: final String s = getClass().toString();
165: return s.substring(s.lastIndexOf('.') + 1, s.length());
166: }
167:
168: /** this class is used by method call. As in this case we do not
169: * want to abstract from names
170: */
171: static class NameAbstractionTableDisabled extends
172: NameAbstractionTable {
173:
174: public static final NameAbstractionTableDisabled INSTANCE = new NameAbstractionTableDisabled();
175:
176: public void add(SourceElement pe1, SourceElement pe2) {
177: }
178:
179: public boolean sameAbstractName(SourceElement pe1,
180: SourceElement pe2) {
181: return pe1.equals(pe2);
182: }
183: }
184:
185: public MatchConditions match(SourceData source,
186: MatchConditions matchCond) {
187: final ProgramElement src = source.getSource();
188: Debug.out("Program match start (template, source)", this , src);
189:
190: if (src.getClass() != getClass()) {
191: Debug
192: .out(
193: "Program match failed. Incompatible AST nodes (template, source)",
194: this , src);
195: Debug.out("Incompatible AST nodes (template, source)", this
196: .getClass(), src.getClass());
197: return null;
198: }
199: source.next();
200: return matchCond;
201: }
202:
203: }
|