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: package de.uka.ilkd.key.logic;
09:
10: import java.util.HashMap;
11: import java.util.Map;
12:
13: import de.uka.ilkd.key.java.JavaInfo;
14: import de.uka.ilkd.key.logic.op.Function;
15: import de.uka.ilkd.key.logic.op.ProgramVariable;
16: import de.uka.ilkd.key.logic.op.RigidFunction;
17: import de.uka.ilkd.key.logic.sort.ArrayOfSort;
18: import de.uka.ilkd.key.logic.sort.Sort;
19:
20: public class AtPreNamespace extends Namespace {
21:
22: private final Map atPreMapping;
23: private final JavaInfo javaInfo;
24:
25: public AtPreNamespace(Namespace parent, JavaInfo ji) {
26: super (parent);
27: this .javaInfo = ji;
28: this .atPreMapping = new HashMap();
29: }
30:
31: public Named lookup(Name name) {
32: Named n = super .lookup(name);
33: if (n == null && name.toString().endsWith("@pre")) {
34: Name atPostName = new Name(name.toString().substring(0,
35: name.toString().length() - 4));
36: Named atPost = (Named) super .lookup(atPostName);
37: if (atPost == null) {
38: if (atPostName.toString().indexOf("::") >= 0) {
39: atPost = javaInfo.getAttribute(atPostName
40: .toString());
41: }
42: if (atPost == null) {
43: return null;
44: }
45: }
46:
47: n = (Named) atPreMapping.get(atPost);
48: if (n == null) {
49: if (atPost instanceof ProgramVariable) {
50: ProgramVariable pv = (ProgramVariable) atPost;
51: final Sort[] argSorts;
52: if (pv.isMember() && !pv.isStatic()) {
53: argSorts = new Sort[] { pv.getContainerType()
54: .getSort() };
55: if (argSorts[0] == null) { // in the case of array length
56: argSorts[0] = javaInfo
57: .getJavaLangObjectAsSort();
58: }
59: } else {
60: argSorts = new Sort[0];
61: }
62: n = createAtPreFunction(name, pv.sort(),
63: new ArrayOfSort(argSorts));
64: } else if (atPost instanceof Function) {
65: n = createAtPreFunction(name, ((Function) atPost)
66: .sort(), ((Function) atPost).argSort());
67: }
68: atPreMapping.put(atPost, n);
69: }
70: }
71: return n;
72: }
73:
74: /**
75: * @param name
76: * @param atPost
77: * @param argsort
78: * @return
79: */
80: private Named createAtPreFunction(Name name, Sort sort,
81: ArrayOfSort argsort) {
82: return new RigidFunction(name, sort, argsort);
83: }
84:
85: public Map getAtPreMapping() {
86: return atPreMapping;
87: }
88:
89: }
|