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: // This file is taken from the RECODER library, which is protected by the LGPL,
012: // and modified.
013: /** This class is part of the AST RECODER builds when it parses and resolves Java
014: * programs with meta constructs and schema variables. It is transformed by Recoder2KeY
015: * to a subclass of ...rule.metaconstruct.ProgramMetaConstruct.
016: */package de.uka.ilkd.key.java.recoderext;
017:
018: import java.util.Iterator;
019: import java.util.List;
020: import java.util.Vector;
021:
022: import recoder.java.ProgramElement;
023: import recoder.java.SourceVisitor;
024: import recoder.java.Statement;
025: import recoder.java.StatementContainer;
026: import recoder.java.statement.JavaStatement;
027: import de.uka.ilkd.key.logic.op.ProgramSV;
028:
029: public class RKeYMetaConstruct extends JavaStatement implements
030: StatementContainer, KeYRecoderExtension {
031:
032: /**
033: Child
034: */
035: protected Statement child = null;
036: protected String name = "";
037:
038: /** schemavariable needed by meta construct */
039: private List sv = new Vector(); //of ProgramVariableSVWrapper
040:
041: /**
042: Loop statement.
043: @param proto a loop statement.
044: */
045:
046: protected RKeYMetaConstruct(RKeYMetaConstruct proto) {
047: super (proto);
048: if (proto.child != null) {
049: child = (Statement) proto.child.deepClone();
050: }
051: }
052:
053: public RKeYMetaConstruct() {
054: }
055:
056: /**
057: Make parent role valid.
058: */
059: public void makeParentRoleValid() {
060: super .makeParentRoleValid();
061: if (child != null) {
062: child.setStatementContainer(this );
063: }
064: }
065:
066: /**
067: Returns the number of children of this node.
068: @return an int giving the number of children of this node
069: */
070: public int getChildCount() {
071: int result = 0;
072: if (child != null)
073: result++;
074: return result;
075: }
076:
077: /**
078: Returns the child at the specified index in this node's "virtual"
079: child array
080: @param index an index into this node's "virtual" child array
081: @return the program element at the given position
082: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
083: of bounds
084: */
085: public ProgramElement getChildAt(int index) {
086: if (child != null) {
087: if (index == 0)
088: return child;
089: }
090: throw new ArrayIndexOutOfBoundsException();
091: }
092:
093: public int getChildPositionCode(ProgramElement child0) {
094: // role 0: child
095: if (child0 == child) {
096: return 0;
097: }
098: return -1;
099: }
100:
101: /**
102: * Replace a single child in the current node.
103: * The child to replace is matched by identity and hence must be known
104: * exactly. The replacement element can be null - in that case, the child
105: * is effectively removed.
106: * The parent role of the new child is validated, while the
107: * parent link of the replaced child is left untouched.
108: * @param p the old child.
109: * @param q the new child.
110: * @return true if a replacement has occured, false otherwise.
111: * @exception ClassCastException if the new child cannot take over
112: * the role of the old one.
113: */
114:
115: public boolean replaceChild(ProgramElement p, ProgramElement q) {
116: if (child == p) {
117: Statement r = (Statement) q;
118: child = r;
119: if (r != null) {
120: r.setStatementContainer(this );
121: }
122: return true;
123: }
124: return false;
125: }
126:
127: /**
128: * sets a String name of this meta construct like 'unwind-loop'
129: * @param s the String
130: */
131: public void setName(String s) {
132: name = s;
133: }
134:
135: /**
136: * returns a String name of this meta construct.
137: */
138: public String getName() {
139: return name;
140: }
141:
142: /**
143: Get child.
144: @return the statement.
145: */
146:
147: public Statement getChild() {
148: return child;
149: }
150:
151: /**
152: Set child.
153: @param statement a statement.
154: */
155:
156: public void setChild(Statement statement) {
157: child = statement;
158: }
159:
160: /**
161: * first schemavariable needed by the metaconstruct
162: * @param sv an SVWrapper containing the first Schemavariable
163: */
164:
165: public void setSV(SVWrapper sv) {
166: this .sv.add(0, sv);
167: }
168:
169: public void addSV(SVWrapper svw) {
170: this .sv.add(svw);
171: }
172:
173: /**
174: * first schemavariable needed by the metaconstruct
175: * @return first schemavariable needed by the metaconstruct
176: */
177: public SVWrapper getFirstSV() {
178: return (SVWrapper) sv.get(0);
179: }
180:
181: public ProgramSV[] getSV() {
182: ProgramSV[] res = new ProgramSV[sv.size()];
183: Iterator it = sv.iterator();
184: int i = 0;
185: while (it.hasNext()) {
186: res[i++] = (ProgramSV) ((SVWrapper) it.next()).getSV();
187: }
188: return res;
189: }
190:
191: /**
192: Get the number of statements in this container.
193: @return the number of statements.
194: */
195:
196: public int getStatementCount() {
197: return (child != null) ? 1 : 0;
198: }
199:
200: /*
201: Return the statement at the specified index in this node's
202: "virtual" statement array.
203: @param index an index for a statement.
204: @return the statement with the given index.
205: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
206: of bounds.
207: */
208:
209: public Statement getStatementAt(int index) {
210: if (child != null && index == 0) {
211: return child;
212: }
213: throw new ArrayIndexOutOfBoundsException();
214: }
215:
216: //don't think we need it
217: public void accept(SourceVisitor v) {
218: }
219:
220: //???
221: public Object deepClone() {
222: return null;
223: }
224:
225: }
|