01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: /**
12: * Implements "inner renaming", i.e. renaming - if a new variable entering the
13: * globals causes a name clash - this "inner" variable, and leaving the clashing
14: * "outer" one untouched.
15: */package de.uka.ilkd.key.logic;
16:
17: import java.util.HashMap;
18:
19: import de.uka.ilkd.key.java.ProgramElement;
20: import de.uka.ilkd.key.java.Services;
21: import de.uka.ilkd.key.logic.op.LocationVariable;
22: import de.uka.ilkd.key.logic.op.ProgramVariable;
23: import de.uka.ilkd.key.proof.Goal;
24: import de.uka.ilkd.key.proof.ProgVarReplacer;
25:
26: public class InnerVariableNamer extends VariableNamer {
27:
28: public InnerVariableNamer(Services services) {
29: super (services);
30: }
31:
32: /**
33: * returns the maximum counter for the passed basename in the passed globals
34: * and the passed program
35: */
36: private int getMaxCounterInGlobalsAndProgram(String basename,
37: Globals globals, ProgramElement program,
38: PosInProgram posOfDeclaration) {
39: int maxInGlobals = getMaxCounterInGlobals(basename, globals);
40: int maxInProgram = getMaxCounterInProgram(basename, program,
41: posOfDeclaration);
42:
43: return (maxInGlobals > maxInProgram ? maxInGlobals
44: : maxInProgram);
45: }
46:
47: public ProgramVariable rename(ProgramVariable var, Goal goal,
48: PosInOccurrence posOfFind) {
49: ProgramElementName name = var.getProgramElementName();
50: BasenameAndIndex bai = getBasenameAndIndex(name);
51: Globals globals = wrapGlobals(goal.getGlobalProgVars());
52: map = new HashMap();
53:
54: //prepare renaming of inner var
55: final NameCreationInfo nci = getMethodStack(posOfFind);
56: ProgramElementName newname = createName(bai.basename,
57: bai.index, nci);
58: int newcounter = getMaxCounterInGlobalsAndProgram(bai.basename,
59: globals, getProgramFromPIO(posOfFind), null);
60: while (!isUniqueInGlobals(newname.toString(), globals)
61: || goal.proof().getServices().getNamespaces()
62: .lookupLogicSymbol(newname) != null) {
63: newcounter += 1;
64: newname = createName(bai.basename, newcounter, nci);
65: }
66:
67: ProgramVariable newvar = var;
68:
69: if (!newname.equals(name)) {
70: newvar = new LocationVariable(newname, var.getKeYJavaType());
71: map.put(var, newvar);
72: renamingHistory = map;
73: //execute renaming
74: ProgVarReplacer pvr = new ProgVarReplacer(map);
75: pvr.replace(goal);
76: }
77:
78: return newvar;
79: }
80: }
|