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 peer, 029 boolean staticContext) { 030 super(parent, peer, 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, peer, 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 + peer.getExternalName() + " ]]"); 058 FieldDeclVec fdv = ((escjava.tc.TypeSig)peer).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 = peer.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 (peer.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 (!(peer instanceof escjava.tc.TypeSig)) return fdv; 151 escjava.tc.TypeSig ts = (escjava.tc.TypeSig)peer; 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 */