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