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: package de.uka.ilkd.key.visualdebugger.executiontree;
009:
010: import java.util.LinkedList;
011:
012: import de.uka.ilkd.key.logic.ListOfTerm;
013: import de.uka.ilkd.key.logic.Term;
014: import de.uka.ilkd.key.logic.op.ListOfProgramVariable;
015: import de.uka.ilkd.key.logic.op.ProgramMethod;
016:
017: /**
018: * An instance of this specialised node class is used if a node in an execution
019: * tree refers to an invocation of a method. In these cases it is useful to
020: * extract and cache additional information for later inspection like
021: * <ul>
022: * <li> the invoked method (after dynamic dispatch) </li>
023: * <li> parameter names and their values</li>
024: * </ul>
025: *
026: * FIXME: the copy method creates insane trees (I do currently no understand
027: * what ITNodes are, but most probably the copy method brings ETNodes and
028: * ITNodes out of sync), up to now I am not sure which behaviour of copy has
029: * been wanted. This bug applies to all subclasses as well.
030: */
031: public class ETMethodInvocationNode extends ETNode {
032:
033: /** the method that has been invoked */
034: private final ProgramMethod method;
035:
036: /**
037: * TODDO don't know yet why and if necessary to keep this
038: */
039: private final Term methodReference;
040:
041: /**
042: * the program variables representing the methods parameters TODO: check if
043: * order is the same as in method signature and if yes comment it here!
044: */
045: private final ListOfProgramVariable parameters;
046:
047: /**
048: * the values of the parameters at the point of method invocation
049: */
050: private final ListOfTerm values;
051:
052: /**
053: * creates an execution tree node referring to a method invocation
054: *
055: * @param bc
056: * TODO ???
057: * @param itNodes
058: * TODO ???
059: * @param method
060: * the ProgramMethod which is invoked
061: * @param methodReference
062: * TODO ????
063: * @param parameters
064: * ListOfProgramVariable enumerating the method parameters
065: * @param values
066: * ListOfTerm enumerating the values of the paramters at the
067: * time when the method invocation occurred
068: * @param parent
069: * the direct ancestor node of this node
070: */
071: public ETMethodInvocationNode(ListOfTerm bc, LinkedList itNodes,
072: ProgramMethod method, Term methodReference,
073: ListOfProgramVariable parameters, ListOfTerm values,
074: ETNode parent) {
075: super (bc, itNodes, parent);
076: this .method = method;
077: this .methodReference = methodReference;
078: this .parameters = parameters;
079: this .values = values;
080:
081: }
082:
083: /**
084: * creates an execution tree node referring to a method invocation
085: *
086: * @param bc
087: * TODO ???
088: * @param method
089: * the ProgramMethod which is invoked
090: * @param methodReference
091: * TODO ????
092: * @param parameters
093: * ListOfProgramVariable enumerating the method parameters
094: * @param values
095: * ListOfTerm enumerating the values of the paramters at the
096: * time when the method invocation occurred
097: * @param parent
098: * the direct ancestor node of this node
099: */
100: public ETMethodInvocationNode(ListOfTerm bc, ProgramMethod method,
101: Term methodReference, ListOfProgramVariable parameters,
102: ListOfTerm values, ETNode parent) {
103: super (bc, parent);
104: this .method = method;
105: this .methodReference = methodReference;
106: this .parameters = parameters;
107: this .values = values;
108: }
109:
110: /**
111: * returns the invoked method
112: *
113: * @return the ProgramMethod representing the invoked method
114: */
115: public ProgramMethod getMethod() {
116: return method;
117: }
118:
119: public Term getMethodReference() {
120: return methodReference;
121: }
122:
123: /**
124: * the program variables representing the method parameters
125: *
126: * @return the program variables representing the method parameters
127: */
128: public ListOfProgramVariable getParameters() {
129: return parameters;
130: }
131:
132: /**
133: * the symbolic values of the method paramters
134: *
135: * @return the symbolic values of the method parameters
136: */
137: public ListOfTerm getValues() {
138: return values;
139: }
140:
141: /**
142: * creates a shallow copy of this node and attaches it to node <tt>p</tt>
143: * FIXME: FIX this method as it creates not well linked trees Problems: 1)
144: * the children of this node are not linked to their new parent -->
145: * malformed tree 2) the children are not copied themselves and linking
146: * would destroy the old tree
147: *
148: */
149: public ETNode copy(ETNode p) {
150: final ETMethodInvocationNode copy = new ETMethodInvocationNode(
151: this .getBC(), (LinkedList) this .getITNodes().clone(),
152: this .method, this .methodReference, this .parameters,
153: this .values, p);
154: copy.setChildren((LinkedList) this.getChildrenList().clone());
155: return copy;
156: }
157:
158: }
|