001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package escjava.tc;
004
005 import java.util.Enumeration;
006 import java.util.Hashtable;
007
008 import javafe.ast.*;
009 import escjava.ast.GhostDeclPragma;
010 import escjava.ast.ModelDeclPragma;
011 import escjava.ast.TagConstants;
012 import escjava.ast.Utils;
013
014 import javafe.tc.*;
015 import javafe.tc.TypeSig;
016
017 /**
018 * This class overrides {@link EnvForTypeSig} so that it "sees" ghost and model
019 * fields if {@link escjava.tc.FlowInsensitiveChecks#inAnnotation} is
020 * <code>true</code>.
021 */
022
023 public class GhostEnv extends EnvForTypeSig
024 {
025 // Creation
026
027 public GhostEnv(/*@ non_null */ Env parent,
028 /*@ non_null */ TypeSig peervar,
029 boolean staticContext) {
030 super(parent, peervar, staticContext);
031 }
032
033 // Current/enclosing instances
034
035 /**
036 * Returns a new {@link Env} that acts the same as us, except that its current
037 * instance (if any) is not accessible.
038 *
039 * @note This routine is somewhat inefficient and should be avoided unless an
040 * unknown environment needs to be coerced in this way.
041 */
042 public Env asStaticContext() {
043 return new GhostEnv(parent, peervar, true);
044 }
045
046 // Debugging functions
047
048 /**
049 * Display information about an {@link Env} to {@link System#out}. This function
050 * is intended only for debugging use.
051 */
052 public void display() {
053 parent.display();
054 System.out.println("[[ extended with the (ghost) "
055 + (staticContext ? "static" : "complete")
056 + " bindings of type "
057 + peervar.getExternalName() + " ]]");
058 FieldDeclVec fdv = ((escjava.tc.TypeSig)peervar).jmlFields;
059 for (int i=0; i<fdv.size(); ++i) {
060 System.out.println(" " + fdv.elementAt(i).id);
061 }
062
063 }
064
065 // Code to locate our ghost and model fields by name
066
067 /**
068 * Attempts to find a ghost or model field that belongs
069 * to us (including supertypes) with
070 * name <code>n</code> that is not equal to <code>excluded</code>, which may
071 * be <code>null</code>.
072 *
073 * @param n the name of the ghost field to get.
074 * @param excluded a field declaration to avoid.
075 * @return the ghost field declaration if successful, otherwise
076 * <code>null</code>.
077 */
078 public FieldDecl getGhostField(String n, FieldDecl excluded) {
079 FieldDeclVec fdv = peervar.getFields(false);
080 for (int i=0; i<fdv.size(); ++i) {
081 FieldDecl f = fdv.elementAt(i);
082 if (!f.id.toString().equals(n))
083 continue;
084
085 if (f != excluded)
086 return f;
087 }
088
089 return null;
090 }
091
092 static public boolean isStatic(FieldDecl d) {
093 boolean isStatic = d.parent instanceof InterfaceDecl;
094 if (Modifiers.isStatic(d.modifiers)) isStatic = true;
095 if (Utils.findModifierPragma(d,
096 TagConstants.INSTANCE) != null) isStatic = false;
097 return isStatic;
098 }
099
100 // Misc. routines
101
102 /**
103 * Determines if a field is a ghost (not model or Java) field
104 *
105 * @return true if the FieldDecl <code>field</code> a ghost
106 * field (and not a model or Java field).
107 *
108 */
109 //@ requires field != null;
110 public static boolean isGhostField(FieldDecl field) {
111 TypeDecl d = field.getParent();
112 // special fields like "length" can't be ghost fields
113 if (d == null)
114 return false;
115
116 return Utils.findModifierPragma(field.pmodifiers,
117 TagConstants.GHOST) != null;
118 /*
119 TypeDeclElemVec elems = d.elems;
120 for (int i = 0; i < elems.size(); i++) {
121 TypeDeclElem elem = elems.elementAt(i);
122 if (elem instanceof GhostDeclPragma) {
123 FieldDecl ghost = ((GhostDeclPragma)elem).decl;
124 if (field == ghost)
125 return true;
126 }
127 }
128
129 return false;
130 */
131 }
132
133 /**
134 * Override to make ghost fields visible if {@link
135 * escjava.tc.FlowInsensitiveChecks#inAnnotation} is <code>true</code>.
136 */
137 protected boolean hasField(Identifier id) {
138 if (peervar.hasField(id))
139 return true;
140
141 if (!FlowInsensitiveChecks.inAnnotation)
142 return false;
143
144 return (getGhostField(id.toString(), null) != null);
145 }
146
147 public FieldDeclVec getFields(boolean allFields) {
148 FieldDeclVec fdv = FieldDeclVec.make();
149 fdv.append(super.getFields(allFields));
150 if (!(peervar instanceof escjava.tc.TypeSig)) return fdv;
151 escjava.tc.TypeSig ts = (escjava.tc.TypeSig)peervar;
152 fdv.append(ts.jmlFields);
153 if (!allFields) return fdv;
154 fdv.append(ts.jmlHiddenFields);
155 fdv.append(ts.jmlDupFields);
156 return fdv;
157 }
158
159 } // end of class GhostEnv
160
161 /*
162 * Local Variables:
163 * Mode: Java
164 * fill-column: 85
165 * End:
166 */