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.soundness;
012:
013: import de.uka.ilkd.key.java.*;
014: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
015: import de.uka.ilkd.key.java.statement.JumpStatement;
016: import de.uka.ilkd.key.java.statement.Return;
017: import de.uka.ilkd.key.java.statement.Throw;
018: import de.uka.ilkd.key.logic.Namespace;
019: import de.uka.ilkd.key.logic.op.ListOfIProgramVariable;
020: import de.uka.ilkd.key.logic.op.LocationVariable;
021: import de.uka.ilkd.key.logic.op.ProgramVariable;
022: import de.uka.ilkd.key.logic.op.SchemaVariable;
023: import de.uka.ilkd.key.rule.ListOfTacletApp;
024: import de.uka.ilkd.key.rule.SLListOfTacletApp;
025: import de.uka.ilkd.key.util.ExtList;
026:
027: /**
028: * Abstract class that provides some methods both the statement and the
029: * expression skolem builder need
030: */
031: public abstract class StatementExpressionSkolemBuilder extends
032: AbstractPVPrefixSkolemBuilder {
033:
034: private final Namespace skolemVariables = new Namespace();
035: private ListOfTacletApp taclets = SLListOfTacletApp.EMPTY_LIST;
036:
037: private final JumpStatementPrefixes jumpStatementPrefixes;
038:
039: public StatementExpressionSkolemBuilder(SkolemSet p_oriSkolemSet,
040: ProgramVariablePrefixes p_prefixes,
041: JumpStatementPrefixes p_jumpStatementPrefixes,
042: Services p_services) {
043: super (p_oriSkolemSet, p_prefixes, p_services);
044:
045: jumpStatementPrefixes = p_jumpStatementPrefixes;
046: }
047:
048: protected JumpStatementPrefixes getJumpStatementPrefixes() {
049: return jumpStatementPrefixes;
050: }
051:
052: protected ListOfStatement getJumpStatementPrefix(SchemaVariable p) {
053: ListOfStatement res = getJumpStatementPrefixes().getPrefix(p);
054: if (res == null)
055: res = SLListOfStatement.EMPTY_LIST;
056: return res;
057: }
058:
059: protected ListOfTacletApp getTaclets() {
060: return taclets;
061: }
062:
063: protected void addVocabulary(SkolemSymbolTacletFactory p_factory) {
064: // We only have to add variables and taclets, as no other symbols are
065: // currently created by the concerned factories
066: skolemVariables.add(p_factory.getVariables());
067: this .taclets = taclets.prepend(p_factory.getTaclets());
068: }
069:
070: protected Namespace getVariables() {
071: return skolemVariables;
072: }
073:
074: protected class StatementSymbolArgBuilder {
075:
076: private final SchemaVariable sv;
077: private ListOfIProgramVariable pvp;
078: private ArrayOfStatement jt;
079:
080: StatementSymbolArgBuilder(SchemaVariable p_sv) {
081: sv = p_sv;
082: pvp = getProgramVariablePrefix(sv);
083: jt = createJumpTable();
084: }
085:
086: ListOfIProgramVariable getInfluencingPVs() {
087: return pvp;
088: }
089:
090: ArrayOfStatement getJumpTable() {
091: return jt;
092: }
093:
094: private ArrayOfStatement createJumpTable() {
095: ExtList res = new ExtList();
096:
097: // try { // <-- why this??
098: {
099: KeYJavaType th = getJavaInfo().getTypeByClassName(
100: "java.lang.Throwable");
101: ProgramVariable v = new LocationVariable(
102: createUniquePEName("th"), th);
103:
104: JumpStatement js = new Throw(v);
105:
106: res.add(js);
107: pvp = pvp.prepend(v);
108: getVariables().add(v);
109: }
110: // } catch ( RuntimeException e ) {}
111:
112: IteratorOfStatement it = getJumpStatementPrefix(sv)
113: .iterator();
114: Statement s;
115: while (it.hasNext()) {
116: s = it.next();
117:
118: if (s instanceof Return) {
119: Expression e = ((Return) s).getExpression();
120: if (e instanceof SchemaVariable) {
121: // this one should already have been instantiated
122: ProgramElement pe = (ProgramElement) getOriginalSkolemSet()
123: .getInstantiations().getInstantiation(
124: (SchemaVariable) e);
125:
126: if (pe != null) {
127: ExtList children = new ExtList();
128: children.add(pe);
129: s = new Return(children);
130: }
131: }
132: }
133:
134: res.add(s);
135: }
136:
137: return new ArrayOfStatement((Statement[]) res
138: .collect(Statement.class));
139: }
140:
141: }
142: }
|