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     */