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.strategy.feature;
009:
010: import java.util.ArrayList;
011: import java.util.List;
012:
013: import de.uka.ilkd.key.java.JavaInfo;
014: import de.uka.ilkd.key.java.ProgramElement;
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.java.Statement;
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.statement.Throw;
020: import de.uka.ilkd.key.logic.PosInOccurrence;
021: import de.uka.ilkd.key.logic.PosInProgram;
022: import de.uka.ilkd.key.logic.ProgramPrefix;
023: import de.uka.ilkd.key.logic.Term;
024: import de.uka.ilkd.key.logic.op.Modality;
025: import de.uka.ilkd.key.logic.sort.Sort;
026: import de.uka.ilkd.key.proof.Goal;
027: import de.uka.ilkd.key.rule.RuleApp;
028: import de.uka.ilkd.key.rule.TacletApp;
029:
030: public class ThrownExceptionFeature extends BinaryFeature {
031:
032: public static Feature create(String[] blockedExceptions,
033: Services services) {
034: return new ThrownExceptionFeature(blockedExceptions, services);
035: }
036:
037: private final Sort[] filteredExceptions;
038:
039: /**
040: * creates a feature filtering first active throw statements where the
041: * thrown exception is of one of the given types (or their subtypes)
042: *
043: * @param p_filteredExceptions
044: * the String array with the types of the thrown exceptions
045: * @param services
046: * the Services
047: */
048: private ThrownExceptionFeature(String[] p_filteredExceptions,
049: Services services) {
050: final List filtered = new ArrayList();
051:
052: final JavaInfo javaInfo = services.getJavaInfo();
053:
054: for (int i = 0; i < p_filteredExceptions.length; i++) {
055: final KeYJavaType nullPointer = javaInfo
056: .getKeYJavaType(p_filteredExceptions[i]);
057: if (nullPointer != null) {
058: filtered.add(nullPointer.getSort());
059: }
060: }
061: filteredExceptions = (Sort[]) filtered
062: .toArray(new Sort[filtered.size()]);
063: }
064:
065: private boolean blockedExceptions(Sort excType) {
066: for (int i = 0; i < filteredExceptions.length; i++) {
067: if (excType.extendsTrans(filteredExceptions[i])) {
068: return true;
069: }
070: }
071: return false;
072: }
073:
074: protected boolean filter(RuleApp app, PosInOccurrence pos, Goal goal) {
075: return app instanceof TacletApp ? filter(pos.subTerm(), goal
076: .proof().getServices(), ((TacletApp) app)
077: .instantiations().getExecutionContext()) : false;
078: }
079:
080: protected boolean filter(Term term, Services services,
081: ExecutionContext ec) {
082: if (term.op() instanceof Modality) {
083: final ProgramElement fstActive = getFirstExecutableStatement(term);
084: return fstActive instanceof Throw
085: && blockedExceptions(((Throw) fstActive)
086: .getExpressionAt(0).getKeYJavaType(
087: services, ec).getSort());
088: }
089: return false;
090: }
091:
092: /**
093: * returns the first executable statement (often identical with the first
094: * active statement)
095: *
096: * @param term
097: * the Term with the program at top level
098: * @return the first executable statement
099: */
100: private ProgramElement getFirstExecutableStatement(Term term) {
101: if (term.javaBlock().isEmpty())
102: return null;
103:
104: final ProgramElement jb = term.javaBlock().program();
105: final ProgramElement fstActive;
106:
107: if (jb instanceof ProgramPrefix) {
108: final ProgramPrefix pp = ((ProgramPrefix) jb)
109: .getPrefixElementAt(((ProgramPrefix) jb)
110: .getPrefixLength() - 1);
111: fstActive = (Statement) PosInProgram.getProgramAt(pp
112: .getFirstActiveChildPos(), pp);
113: } else {
114: fstActive = jb;
115: }
116: return fstActive;
117: }
118:
119: }
|