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: package de.uka.ilkd.key.logic.op;
011:
012: import java.io.IOException;
013:
014: import de.uka.ilkd.key.java.*;
015: import de.uka.ilkd.key.java.abstraction.ArrayType;
016: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
017: import de.uka.ilkd.key.java.abstraction.Type;
018: import de.uka.ilkd.key.java.annotation.Annotation;
019: import de.uka.ilkd.key.java.reference.*;
020: import de.uka.ilkd.key.logic.ProgramElementName;
021: import de.uka.ilkd.key.logic.ProgramInLogic;
022: import de.uka.ilkd.key.logic.Term;
023: import de.uka.ilkd.key.logic.sort.Sort;
024: import de.uka.ilkd.key.rule.MatchConditions;
025: import de.uka.ilkd.key.util.Debug;
026: import de.uka.ilkd.key.util.ExtList;
027:
028: public abstract class ProgramVariable extends TermSymbol implements
029: SourceElement, ProgramElement, Expression, ReferencePrefix,
030: IProgramVariable, ParsableVariable, ReferenceSuffix,
031: ProgramInLogic {
032:
033: // attention: this counter is used to get a unique variable name, once the
034: // names are unique the counter should be removed %%%%
035: private static long COUNTER = 0;
036: private long id;
037: private final KeYJavaType type;
038: private final boolean isStatic;
039: private final boolean isModel;
040: private final boolean isGhost;
041:
042: // the type where this program variable is declared if and only if
043: // the program variable denotes a field
044: private final KeYJavaType containingType;
045:
046: protected ProgramVariable(ProgramElementName name, Sort s,
047: KeYJavaType t, KeYJavaType containingType,
048: boolean isStatic, boolean isModel, boolean isGhost) {
049: super (name, s);
050: this .type = t;
051: this .containingType = containingType;
052: this .isStatic = isStatic;
053: this .isModel = isModel;
054: this .isGhost = isGhost;
055: // remove this as soon as possible %%%
056: id = COUNTER;
057: COUNTER++;
058: }
059:
060: /** returns unique id %%%% HACK */
061: public long id() {
062: return id;
063: }
064:
065: /** returns sort */
066: public Sort sort() {
067: return super .sort() == null ? type.getSort() : super .sort();
068: }
069:
070: /** @return arity of the Variable as int */
071: public int arity() {
072: return 0;
073: }
074:
075: /** @return name of the ProgramVariable */
076: public ProgramElementName getProgramElementName() {
077: return (ProgramElementName) name();
078: }
079:
080: /** toString */
081: public String toString() {
082: return name().toString();
083: }
084:
085: /**
086: * returns true if the program variable has been declared as static
087: */
088: public boolean isStatic() {
089: return isStatic;
090: }
091:
092: public boolean isModel() {
093: return isModel;
094: }
095:
096: /**
097: * returns true if the program variable has been declared as ghost
098: */
099: public boolean isGhost() {
100: return isGhost;
101: }
102:
103: /**
104: * returns true if the program variable is a member
105: */
106: public boolean isMember() {
107: return containingType != null;
108: }
109:
110: /**
111: * returns the KeYJavaType where the program variable is declared or
112: * null if the program variable denotes not a field
113: */
114: public KeYJavaType getContainerType() {
115: return containingType;
116: }
117:
118: public SourceElement getFirstElement() {
119: return this ;
120: }
121:
122: public SourceElement getLastElement() {
123: return this ;
124: }
125:
126: public Comment[] getComments() {
127: return new Comment[0];
128: }
129:
130: /** calls the corresponding method of a visitor in order to
131: * perform some action/transformation on this element
132: * @param v the Visitor
133: */
134: public void visit(de.uka.ilkd.key.java.visitor.Visitor v) {
135: v.performActionOnProgramVariable(this );
136: }
137:
138: /** the recoder pretty printer */
139: public void prettyPrint(PrettyPrinter w) throws IOException {
140: w.printProgramVariable(this );
141: }
142:
143: /**
144: * Returns the start position of the primary token of this element.
145: * To get the start position of the syntactical first token,
146: * call the corresponding method of <CODE>getFirstElement()</CODE>.
147: * @return the start position of the primary token.
148: */
149: public Position getStartPosition() {
150: return Position.UNDEFINED;
151: }
152:
153: /**
154: * Returns the end position of the primary token of this element.
155: * To get the end position of the syntactical first token,
156: * call the corresponding method of <CODE>getLastElement()</CODE>.
157: * @return the end position of the primary token.
158: */
159: public Position getEndPosition() {
160: return Position.UNDEFINED;
161: }
162:
163: /**
164: * Returns the relative position (number of blank heading lines and
165: * columns) of the primary token of this element.
166: * To get the relative position of the syntactical first token,
167: * call the corresponding method of <CODE>getFirstElement()</CODE>.
168: *
169: * @return the relative position of the primary token.
170: */
171: public Position getRelativePosition() {
172: return Position.UNDEFINED;
173: }
174:
175: public PositionInfo getPositionInfo() {
176: return PositionInfo.UNDEFINED;
177: }
178:
179: public KeYJavaType getKeYJavaType() {
180: return type;
181: }
182:
183: public KeYJavaType getKeYJavaType(Services javaServ) {
184: return getKeYJavaType();
185: }
186:
187: public KeYJavaType getKeYJavaType(Services javaServ,
188: ExecutionContext ec) {
189: return getKeYJavaType();
190: }
191:
192: /**
193: *@return the annotations.
194: */
195: public Annotation[] getAnnotations() {
196: return new Annotation[0];
197: }
198:
199: public int getAnnotationCount() {
200: return 0;
201: }
202:
203: /**
204: * We do not have a prefix, so fake it!
205: * This way we implement ReferencePrefix
206: * @author VK
207: */
208: public ReferencePrefix getReferencePrefix() {
209: return null;
210: }
211:
212: public ReferencePrefix setReferencePrefix(ReferencePrefix r) {
213: return this ;
214: }
215:
216: /** equals modulo renaming is described in the corresponding
217: * comment in class SourceElement. In this case two
218: * programvariables are considered to be equal if they are
219: * assigned to the same abstract name or if they are the same
220: * object.
221: */
222: public boolean equalsModRenaming(SourceElement se,
223: NameAbstractionTable nat) {
224: return nat.sameAbstractName(this , se);
225: }
226:
227: public Expression convertToProgram(Term t, ExtList l) {
228: if (isStatic()) {
229: return new FieldReference(this , new TypeRef(
230: getContainerType()));
231: } else {
232: return this ;
233: }
234: }
235:
236: public String proofToString() {
237: final Type javaType = type.getJavaType();
238: final String typeName;
239: if (javaType instanceof ArrayType) {
240: typeName = ((ArrayType) javaType)
241: .getAlternativeNameRepresentation();
242: } else {
243: typeName = javaType.getFullName();
244: }
245: return typeName + " " + name() + ";\n";
246: }
247:
248: public boolean isImplicit() {
249: return getProgramElementName().getProgramName().startsWith("<");
250: }
251:
252: /* (non-Javadoc)
253: * @see de.uka.ilkd.key.logic.op.Location#mayBeAliasedBy(de.uka.ilkd.key.logic.op.Location)
254: */
255: public boolean mayBeAliasedBy(Location loc) {
256: return loc instanceof SortedSchemaVariable || loc == this ;
257: }
258:
259: public MatchConditions match(SourceData source,
260: MatchConditions matchCond) {
261: final ProgramElement src = source.getSource();
262: source.next();
263: if (src == this ) {
264: return matchCond;
265: } else {
266: Debug
267: .out(
268: "Program match failed. Not same program variable (pattern, source)",
269: this, src);
270: return null;
271: }
272: }
273: }
|