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: /** represents a name that is part of a program
011: */package de.uka.ilkd.key.logic;
012:
013: import org.apache.log4j.Logger;
014:
015: import de.uka.ilkd.key.java.*;
016: import de.uka.ilkd.key.java.annotation.Annotation;
017: import de.uka.ilkd.key.java.reference.MethodName;
018: import de.uka.ilkd.key.java.reference.ReferenceSuffix;
019: import de.uka.ilkd.key.java.visitor.Visitor;
020: import de.uka.ilkd.key.rule.MatchConditions;
021: import de.uka.ilkd.key.util.Debug;
022:
023: public class ProgramElementName extends Name implements
024: TerminalProgramElement, Label, ReferenceSuffix, MethodName {
025:
026: private final String qualifierString;
027: private final String shortName;
028: private final NameCreationInfo creationInfo;
029: private final Comment[] comments;
030:
031: static Logger logger = Logger.getLogger(ProgramElementName.class
032: .getName());
033:
034: /** create a new name
035: * @param name the String with the name of the program element
036: */
037: public ProgramElementName(String name) {
038: super (name);
039: this .qualifierString = "".intern();
040: this .shortName = name.intern();
041: this .creationInfo = null;
042: comments = new Comment[0];
043: }
044:
045: /** create a new name
046: * @param name the String with the name of the program element
047: */
048: public ProgramElementName(String name, Comment[] c) {
049: super (name);
050: this .qualifierString = "".intern();
051: this .shortName = name.intern();
052: this .creationInfo = null;
053: comments = c;
054: }
055:
056: public ProgramElementName(String name, NameCreationInfo creationInfo) {
057: super (name);
058: this .qualifierString = "".intern();
059: this .shortName = name.intern();
060: this .creationInfo = creationInfo;
061: comments = new Comment[0];
062: }
063:
064: public ProgramElementName(String name,
065: NameCreationInfo creationInfo, Comment[] c) {
066: super (name);
067: this .qualifierString = "".intern();
068: this .shortName = name.intern();
069: this .creationInfo = creationInfo;
070: comments = c;
071: }
072:
073: public ProgramElementName(String n, String q) {
074: super (q + "::" + n);
075: if ((q != "") & logger.isDebugEnabled()) {
076: logger.debug(q + "::" + n);
077: }
078: assert q != null && q.length() > 0 : "Tried to create qualified name with missing qualifier";
079:
080: this .qualifierString = q.intern();
081: this .shortName = n.intern();
082: this .creationInfo = null;
083: comments = new Comment[0];
084: }
085:
086: /** @return comments */
087: public Comment[] getComments() {
088: return comments;
089: }
090:
091: /**
092: * to be compatible to a ProgramElement
093: */
094: public SourceElement getFirstElement() {
095: return this ;
096: }
097:
098: /**
099: * to be compatible to a ProgramElement
100: */
101: public SourceElement getLastElement() {
102: return this ;
103: }
104:
105: public void prettyPrint(PrettyPrinter w) throws java.io.IOException {
106: w.printProgramElementName(this );
107: }
108:
109: /** calls the corresponding method of a visitor in order to
110: * perform some action/transformation on this element
111: * @param v the Visitor
112: */
113: public void visit(Visitor v) {
114: v.performActionOnProgramElementName(this );
115: }
116:
117: /**
118: Returns the start position of the primary token of this element.
119: To get the start position of the syntactical first token,
120: call the corresponding method of <CODE>getFirstElement()</CODE>.
121: @return the start position of the primary token.
122: */
123: public Position getStartPosition() {
124: return Position.UNDEFINED;
125: }
126:
127: /**
128: Returns the end position of the primary token of this element.
129: To get the end position of the syntactical first token,
130: call the corresponding method of <CODE>getLastElement()</CODE>.
131: @return the end position of the primary token.
132: */
133: public Position getEndPosition() {
134: return Position.UNDEFINED;
135: }
136:
137: /**
138: Returns the relative position (number of blank heading lines and
139: columns) of the primary token of this element.
140: To get the relative position of the syntactical first token,
141: call the corresponding method of <CODE>getFirstElement()</CODE>.
142: @return the relative position of the primary token.
143: */
144: public Position getRelativePosition() {
145: return Position.UNDEFINED;
146: }
147:
148: public PositionInfo getPositionInfo() {
149: return PositionInfo.UNDEFINED;
150: }
151:
152: /** equals modulo renaming is described in the corresponding
153: * comment in class SourceElement. The ProgramElementName has to
154: * check if an abstract name has been assigned and if, if both
155: * elements are assigned to the same name, otherwise the names
156: * have to be equal
157: */
158: public boolean equalsModRenaming(SourceElement se,
159: NameAbstractionTable nat) {
160: if (!(se instanceof ProgramElementName)) {
161: return false;
162: }
163: return nat.sameAbstractName(this , se);
164: }
165:
166: public String getQualifier() {
167: return qualifierString;
168: }
169:
170: public String getProgramName() {
171: return shortName;
172: }
173:
174: public NameCreationInfo getCreationInfo() {
175: return creationInfo;
176: }
177:
178: /**
179: *@return the annotations.
180: */
181: public Annotation[] getAnnotations() {
182: return new Annotation[0];
183: }
184:
185: public int getAnnotationCount() {
186: return 0;
187: }
188:
189: public MatchConditions match(SourceData source,
190: MatchConditions matchCond) {
191: final ProgramElement src = source.getSource();
192: if (this .equals(src)) {
193: source.next();
194: return matchCond;
195: } else {
196: Debug.out("Program match failed (pattern, source)", this,
197: src);
198: return null;
199: }
200: }
201: }
|