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.rule.conditions;
012:
013: import de.uka.ilkd.key.java.ArrayOfExpression;
014: import de.uka.ilkd.key.java.ArrayOfProgramElement;
015: import de.uka.ilkd.key.java.Expression;
016: import de.uka.ilkd.key.java.Services;
017: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
018: import de.uka.ilkd.key.java.reference.ExecutionContext;
019: import de.uka.ilkd.key.java.reference.MethodName;
020: import de.uka.ilkd.key.java.reference.MethodReference;
021: import de.uka.ilkd.key.java.reference.ReferencePrefix;
022: import de.uka.ilkd.key.logic.op.LocationVariable;
023: import de.uka.ilkd.key.logic.op.ProgramMethod;
024: import de.uka.ilkd.key.logic.op.SVSubstitute;
025: import de.uka.ilkd.key.logic.op.SchemaVariable;
026: import de.uka.ilkd.key.logic.sort.NullSort;
027: import de.uka.ilkd.key.rule.VariableConditionAdapter;
028: import de.uka.ilkd.key.rule.inst.SVInstantiations;
029:
030: /**
031: * ensures that the given instantiation for the schemavariable denotes
032: * a static method. For determining the method the callee and the
033: * arguments of the method are needed as arguments.
034: */
035: public class StaticMethodCondition extends VariableConditionAdapter {
036:
037: private final boolean negation;
038: private final SchemaVariable caller;
039: private final SchemaVariable methname;
040: private final SchemaVariable args;
041:
042: /**
043: * the static reference condition checks if a suggested
044: * instantiation for a schema variable denotes a static method
045: * call. The flag negation allows to reuse this condition for
046: * ensuring non static references.
047: */
048: public StaticMethodCondition(boolean negation,
049: SchemaVariable caller, SchemaVariable methname,
050: SchemaVariable args) {
051: this .negation = negation;
052: this .caller = caller;
053: this .methname = methname;
054: this .args = args;
055: }
056:
057: private static ArrayOfExpression toArrayOfExpression(
058: ArrayOfProgramElement a) {
059: Expression[] result = new Expression[a.size()];
060: for (int i = 0; i < a.size(); i++) {
061: result[i] = (Expression) a.getProgramElement(i);
062: }
063: return new ArrayOfExpression(result);
064: }
065:
066: /**
067: * tests if the instantiation suggestions goes along with the static
068: * condition
069: * @param var the template Variable to be instantiated
070: * @param subst the SVSubstitute to be mapped to var
071: * @param svInst the SVInstantiations that are already known to be
072: * needed
073: * @return true iff condition is fulfilled
074: */
075: public boolean check(SchemaVariable var, SVSubstitute subst,
076: SVInstantiations svInst, Services services) {
077:
078: ReferencePrefix rp = (ReferencePrefix) svInst
079: .getInstantiation(caller);
080: MethodName mn = (MethodName) svInst.getInstantiation(methname);
081: ArrayOfProgramElement ape = (ArrayOfProgramElement) svInst
082: .getInstantiation(args);
083:
084: if (rp != null && mn != null && ape != null) {
085: ArrayOfExpression ar = toArrayOfExpression((ArrayOfProgramElement) svInst
086: .getInstantiation(args));
087: if (var == args) {
088: assert subst instanceof ArrayOfExpression : "wrong use of StaticMethodCondition";
089: ar = (ArrayOfExpression) subst;
090: }
091: ExecutionContext ec = svInst.getContextInstantiation()
092: .activeStatementContext();
093: MethodReference mr = new MethodReference(ar, mn, rp);
094: ProgramMethod method = null;
095: KeYJavaType prefixType = services.getTypeConverter()
096: .getKeYJavaType((Expression) rp, ec);
097: if ((rp instanceof LocationVariable)
098: && (((LocationVariable) rp).sort() instanceof NullSort)) {
099: return true;
100: }
101: if (ec != null) {
102: method = mr.method(services, prefixType, ec);
103: // we are only interested in the signature. The method
104: // must be declared in the static context.
105: } else { //no execution context
106: method = mr.method(services, prefixType, mr
107: .getMethodSignature(services, ec), prefixType);
108: }
109: if (method == null) {
110: return false;
111: }
112: return negation ^ method.isStatic();
113: }
114: return true;
115: }
116:
117: public String toString() {
118: return (negation ? "\\not " : "") + "\\staticMethodReference("
119: + caller + ", " + methname + ", " + args + ")";
120: }
121:
122: }
|