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.reference;
012:
013: import de.uka.ilkd.key.java.*;
014: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
015: import de.uka.ilkd.key.java.visitor.Visitor;
016: import de.uka.ilkd.key.util.ExtList;
017:
018: /**
019: * Meta class reference.
020: *
021: */
022:
023: public class MetaClassReference extends JavaNonTerminalProgramElement
024: implements Reference, Expression, ReferencePrefix,
025: ReferenceSuffix, TypeReferenceContainer {
026:
027: /**
028: * Type reference.
029: */
030: protected final TypeReference typeReference;
031:
032: /**
033: * Meta class reference.
034: */
035: public MetaClassReference() {
036: typeReference = null;
037: }
038:
039: /**
040: * Meta class reference.
041: * @param reference a type reference.
042: */
043: public MetaClassReference(TypeReference reference) {
044: typeReference = reference;
045: }
046:
047: /**
048: * Constructor for the transformation of COMPOST ASTs to KeY.
049: * @param children the children of this AST element as KeY classes.
050: * May contain:
051: * a TypeReference (as reference for the meta class),
052: * Comments
053: */
054: public MetaClassReference(ExtList children) {
055: super (children);
056: typeReference = (TypeReference) children
057: .get(TypeReference.class);
058: }
059:
060: /**
061: * Returns the number of children of this node.
062: * @return an int giving the number of children of this node
063: */
064: public int getChildCount() {
065: return (typeReference != null) ? 1 : 0;
066: }
067:
068: /**
069: * Returns the child at the specified index in this node's "virtual"
070: * child array
071: * @param index an index into this node's "virtual" child array
072: * @return the program element at the given position
073: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
074: * of bounds
075: */
076: public ProgramElement getChildAt(int index) {
077: if (typeReference != null) {
078: if (index == 0)
079: return typeReference;
080: }
081: throw new ArrayIndexOutOfBoundsException();
082: }
083:
084: /**
085: * Get reference prefix.
086: * @return the reference prefix.
087: */
088: public ReferencePrefix getReferencePrefix() {
089: return typeReference;
090: }
091:
092: /**
093: * Get the number of type references in this container.
094: * @return the number of type references.
095: */
096: public int getTypeReferenceCount() {
097: return (typeReference != null) ? 1 : 0;
098: }
099:
100: /*
101: Return the type reference at the specified index in this node's
102: "virtual" type reference array.
103: @param index an index for a type reference.
104: @return the type reference with the given index.
105: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
106: of bounds.
107: */
108:
109: public TypeReference getTypeReferenceAt(int index) {
110: if (typeReference != null && index == 0) {
111: return typeReference;
112: }
113: throw new ArrayIndexOutOfBoundsException();
114: }
115:
116: /**
117: * Get type reference.
118: * @return the type reference.
119: */
120: public TypeReference getTypeReference() {
121: return typeReference;
122: }
123:
124: public SourceElement getFirstElement() {
125: return (typeReference == null) ? this : typeReference
126: .getFirstElement();
127: }
128:
129: /** calls the corresponding method of a visitor in order to
130: * perform some action/transformation on this element
131: * @param v the Visitor
132: */
133: public void visit(Visitor v) {
134: v.performActionOnMetaClassReference(this );
135: }
136:
137: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
138: p.printMetaClassReference(this );
139: }
140:
141: public ReferencePrefix setReferencePrefix(ReferencePrefix r) {
142: return this ;
143: }
144:
145: public KeYJavaType getKeYJavaType(Services javaServ,
146: ExecutionContext ec) {
147: throw new IllegalStateException(
148: "Metaclass references are not supported by KeY as"
149: + "\'java.lang.Class\' is not part of the Java Card standard");
150: }
151:
152: }
|