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.expression;
012:
013: import de.uka.ilkd.key.java.*;
014: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
015: import de.uka.ilkd.key.java.reference.ExecutionContext;
016: import de.uka.ilkd.key.java.visitor.Visitor;
017: import de.uka.ilkd.key.logic.sort.ArraySortImpl;
018: import de.uka.ilkd.key.logic.sort.Sort;
019: import de.uka.ilkd.key.util.ExtList;
020:
021: /**
022: * An ArrayInitializer is a valid expression exclusively for initializing
023: * ArrayTypes. Any other expressions are suited for any expression node.
024: * These rules could have been expressed by appropriate types, but these
025: * solutions would require a couple of new interfaces which did not seem
026: * adequate.
027: * The parent expression is either another ArrayInitializer (nested blocks)
028: * or a VariableDeclaration.
029: */
030:
031: public class ArrayInitializer extends JavaNonTerminalProgramElement
032: implements Expression, ExpressionContainer {
033:
034: /**
035: * Children.
036: */
037:
038: protected final ArrayOfExpression children;
039:
040: /**
041: * Array initializer.
042: * @param list with all children.
043: * May contain:
044: * several of Expression (as the initializing expression)
045: * Comments
046: */
047:
048: public ArrayInitializer(ExtList list) {
049: super (list);
050: this .children = new ArrayOfExpression((Expression[]) list
051: .collect(Expression.class));
052: }
053:
054: /**
055: * Returns the number of children of this node.
056: * @return an int giving the number of children of this node
057: */
058:
059: public int getChildCount() {
060: return (children != null) ? children.size() : 0;
061: }
062:
063: /**
064: * Returns the child at the specified index in this node's "virtual"
065: * child array
066: * @param index an index into this node's "virtual" child array
067: * @return the program element at the given position
068: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
069: * of bounds
070: */
071:
072: public ProgramElement getChildAt(int index) {
073: if (children != null) {
074: return children.getExpression(index);
075: }
076: throw new ArrayIndexOutOfBoundsException();
077: }
078:
079: /**
080: * Get the number of expressions in this container.
081: * @return the number of expressions.
082: */
083:
084: public int getExpressionCount() {
085: return (children != null) ? children.size() : 0;
086: }
087:
088: /*
089: Return the expression at the specified index in this node's
090: "virtual" expression array.
091: @param index an index for an expression.
092: @return the expression with the given index.
093: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
094: of bounds.
095: */
096:
097: public Expression getExpressionAt(int index) {
098: if (children != null) {
099: return children.getExpression(index);
100: }
101: throw new ArrayIndexOutOfBoundsException();
102: }
103:
104: /** calls the corresponding method of a visitor in order to
105: * perform some action/transformation on this element
106: * @param v the Visitor
107: */
108: public void visit(Visitor v) {
109: v.performActionOnArrayInitializer(this );
110: }
111:
112: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
113: p.printArrayInitializer(this );
114: }
115:
116: /**
117: * Get arguments.
118: * @return the wrapped argument array
119: */
120: public ArrayOfExpression getArguments() {
121: return children;
122: }
123:
124: public KeYJavaType getKeYJavaType(Services javaServ,
125: ExecutionContext ec) {
126: Expression i = this ;
127: int n = 0;
128: Sort s = null;
129: for (; i instanceof ArrayInitializer
130: && ((ArrayInitializer) i).getChildCount() != 0; i = ((ArrayInitializer) i)
131: .getExpressionAt(0)) {
132: n++;
133: }
134: s = i.getKeYJavaType(javaServ, ec).getSort();
135: final JavaInfo javaInfo = javaServ.getJavaInfo();
136: return javaInfo.getKeYJavaType(ArraySortImpl
137: .getArraySortForDim(s, n, javaInfo
138: .getJavaLangObjectAsSort(), javaInfo
139: .getJavaLangCloneableAsSort(), javaInfo
140: .getJavaIoSerializableAsSort()));
141: }
142:
143: }
|