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.abstraction.PrimitiveType;
016: import de.uka.ilkd.key.java.visitor.Visitor;
017: import de.uka.ilkd.key.util.ExtList;
018:
019: /**
020: * Array length reference. As a length reference is int-valued,
021: * and hence it is no valid prefix.
022: * @author AL
023: */
024:
025: public class ArrayLengthReference extends JavaNonTerminalProgramElement
026: implements Reference, Expression, ReferenceSuffix {
027:
028: /**
029: * Reference prefix. It must evaluate to an ArrayType.
030: */
031: protected final ReferencePrefix prefix;
032:
033: /**
034: * Array length reference.
035: */
036: public ArrayLengthReference() {
037: prefix = null;
038: }
039:
040: /**
041: * Constructor for the transformation of COMPOST ASTs to KeY.
042: * @param children the children of this AST element as KeY classes.
043: * May contain:
044: * a ReferencePrefix (for the array length),
045: * Comments
046: */
047: public ArrayLengthReference(ExtList children) {
048: super (children);
049: prefix = (ReferencePrefix) children.get(ReferencePrefix.class);
050: }
051:
052: /**
053: * Returns the number of children of this node.
054: * @return an int giving the number of children of this node
055: */
056:
057: public int getChildCount() {
058: return (prefix != null) ? 1 : 0;
059: }
060:
061: /**
062: * Returns the child at the specified index in this node's "virtual"
063: * child array
064: * @param index an index into this node's "virtual" child array
065: * @return the program element at the given position
066: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
067: * of bounds
068: */
069: public ProgramElement getChildAt(int index) {
070: if (prefix != null && index == 0)
071: return prefix;
072: throw new ArrayIndexOutOfBoundsException();
073: }
074:
075: public KeYJavaType getKeYJavaType(Services javaServ) {
076: return javaServ.getJavaInfo().getKeYJavaType(
077: PrimitiveType.JAVA_INT);
078: }
079:
080: public KeYJavaType getKeYJavaType(Services javaServ,
081: ExecutionContext ec) {
082: return getKeYJavaType(javaServ);
083: }
084:
085: /**
086: * Get reference prefix.
087: * @return the reference prefix.
088: */
089: public ReferencePrefix getReferencePrefix() {
090: return prefix;
091: }
092:
093: public SourceElement getFirstElement() {
094: return (prefix == null) ? this : prefix.getFirstElement();
095: }
096:
097: /** calls the corresponding method of a visitor in order to
098: * perform some action/transformation on this element
099: * @param v the Visitor
100: */
101: public void visit(Visitor v) {
102: v.performActionOnArrayLengthReference(this );
103: }
104:
105: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
106: p.printArrayLengthReference(this);
107: }
108:
109: }
|