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.visitor.Visitor;
015: import de.uka.ilkd.key.util.ExtList;
016:
017: /**
018: * Super constructor reference.
019: *
020: */
021:
022: public class SuperConstructorReference extends
023: SpecialConstructorReference implements ReferenceSuffix {
024:
025: /**
026: * Access path to enclosing class.
027: * As KeY normalises inner classes this should be always null and may be
028: * removed in future
029: */
030: protected final ReferencePrefix prefix;
031:
032: /**
033: * Super constructor reference.
034: */
035: public SuperConstructorReference() {
036: prefix = null;
037: }
038:
039: /**
040: * Super constructor reference.
041: * @param arguments an expression mutable list.
042: */
043: public SuperConstructorReference(Expression[] arguments) {
044: super (arguments);
045: this .prefix = null;
046: }
047:
048: /**
049: * Super constructor reference.
050: * @param accessPath a reference prefix.
051: * @param arguments an expression mutable list.
052: */
053:
054: public SuperConstructorReference(ReferencePrefix accessPath,
055: Expression[] arguments) {
056: super (arguments);
057: this .prefix = accessPath;
058: }
059:
060: /**
061: * Super constructor reference.
062: * @param accessPath a reference prefix.
063: * @param arguments an expression mutable list.
064: */
065:
066: public SuperConstructorReference(ReferencePrefix accessPath,
067: ArrayOfExpression arguments) {
068: super (arguments);
069: this .prefix = accessPath;
070: }
071:
072: /**
073: * Constructor for the transformation of COMPOST ASTs to KeY.
074: * @param children the children of this AST element as KeY classes.
075: * @param accessPath a ReferencePrefix of the array reference.
076: * May contain:
077: * several of Expression (as initializers of the array),
078: * Comments.
079: * Must contain:
080: * execution context
081: * MUST NOT CONTAIN: the ReferencePrefix for the accessPath because
082: * Expression and ReferencePrefix might not be disjunct.
083: */
084: public SuperConstructorReference(ExtList children,
085: ReferencePrefix accessPath, PositionInfo pi) {
086: super (children, pi);
087: this .prefix = accessPath;
088: }
089:
090: /**
091: * Constructor for the transformation of COMPOST ASTs to KeY.
092: * @param children the children of this AST element as KeY classes.
093: * @param accessPath a ReferencePrefix of the array reference.
094: * May contain:
095: * several of Expression (as initializers of the array),
096: * Comments.
097: * Must contain:
098: * execution context
099: * MUST NOT CONTAIN: the ReferencePrefix for the accessPath because
100: * Expression and ReferencePrefix might not be disjunct.
101: */
102: public SuperConstructorReference(ExtList children,
103: ReferencePrefix accessPath) {
104: super (children);
105: this .prefix = accessPath;
106: }
107:
108: /**
109: * Get reference prefix.
110: * @return the reference prefix.
111: */
112: public ReferencePrefix getReferencePrefix() {
113: return prefix;
114: }
115:
116: public SourceElement getFirstElement() {
117: return (prefix == null) ? this : prefix.getFirstElement();
118: }
119:
120: /** calls the corresponding method of a visitor in order to
121: * perform some action/transformation on this element
122: * @param v the Visitor
123: */
124: public void visit(Visitor v) {
125: v.performActionOnSuperConstructorReference(this );
126: }
127:
128: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
129: p.printSuperConstructorReference(this);
130: }
131: }
|