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: package de.uka.ilkd.key.java.reference;
011:
012: import de.uka.ilkd.key.java.JavaNonTerminalProgramElement;
013: import de.uka.ilkd.key.java.PrettyPrinter;
014: import de.uka.ilkd.key.java.ProgramElement;
015: import de.uka.ilkd.key.java.Reference;
016: import de.uka.ilkd.key.java.visitor.Visitor;
017: import de.uka.ilkd.key.util.Debug;
018: import de.uka.ilkd.key.util.ExtList;
019:
020: public class ExecutionContext extends JavaNonTerminalProgramElement
021: implements IExecutionContext, Reference {
022:
023: /**
024: * the class context
025: */
026: protected final TypeReference classContext;
027:
028: /**
029: * the reference to the active object
030: */
031: protected final ReferencePrefix runtimeInstance;
032:
033: /**
034: * creates an execution context reference
035: * @param classContext the TypeReference refering to the next enclosing
036: * class
037: * @param runtimeInstance a ReferencePrefix to the object that
038: * is currently active/executed
039: */
040: public ExecutionContext(TypeReference classContext,
041: ReferencePrefix runtimeInstance) {
042: if (classContext == null)
043: Debug.printStackTrace();
044: this .classContext = classContext;
045: this .runtimeInstance = runtimeInstance;
046: }
047:
048: /**
049: * creates an execution context reference
050: * @param children an ExtList with the required children of the execution
051: * context
052: */
053: public ExecutionContext(ExtList children) {
054: this .classContext = (TypeReference) children
055: .get(TypeReference.class);
056: if (classContext == null) {
057: System.out.println("||||" + children);
058: Debug.printStackTrace();
059: }
060:
061: children.remove(this .classContext);
062: this .runtimeInstance = (ReferencePrefix) children
063: .get(ReferencePrefix.class);
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 count = 0;
072: if (classContext != null)
073: count++;
074: if (runtimeInstance != null)
075: count++;
076: return count;
077: }
078:
079: /**
080: * Returns the child at the specified index in this node's "virtual"
081: * child array.
082: * @param index an index into this node's "virtual" child array
083: * @return the program element at the given position
084: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
085: * of bounds
086: */
087: public ProgramElement getChildAt(int index) {
088: if (classContext != null) {
089: if (index == 0)
090: return classContext;
091: index--;
092: }
093: if (runtimeInstance != null) {
094: if (index == 0)
095: return runtimeInstance;
096: index--;
097: }
098: throw new ArrayIndexOutOfBoundsException();
099: }
100:
101: /**
102: * returns the type reference to the next enclosing class
103: * @return the type reference to the next enclosing class
104: */
105: public TypeReference getTypeReference() {
106: return classContext;
107: }
108:
109: /**
110: * returns the runtime instance object
111: * @return the runtime instance object
112: */
113: public ReferencePrefix getRuntimeInstance() {
114: return runtimeInstance;
115: }
116:
117: /** calls the corresponding method of a visitor in order to
118: * perform some action/transformation on this element
119: * @param v the Visitor
120: */
121: public void visit(Visitor v) {
122: v.performActionOnExecutionContext(this );
123: }
124:
125: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
126: p.printExecutionContext(this );
127: }
128:
129: public String toString() {
130: return "Context: " + classContext + " Instance: "
131: + runtimeInstance;
132: }
133:
134: }
|