    001    package escjava.tc;
    002    import javafe.ast.TypeDecl;
    003    import javafe.ast.CompilationUnit;
    004    import javafe.ast.FieldDeclVec;
    005    import javafe.ast.Identifier;
    006    import javafe.ast.FieldDecl;
    007    import javafe.tc.LookupException;
    008
    009    public class TypeSig extends javafe.tc.TypeSig {
    010
    011        //@ requires \nonnullelements(packageName);
    012        public TypeSig(/*@ non_null @*/ String[] packageName,
    013                       /*@ non_null */ String simpleName,
    014                       javafe.tc.TypeSig enclosingType,
    015                       TypeDecl decl,
    016                       CompilationUnit CU) {
    017            super(packageName,simpleName,enclosingType,decl,CU);
    018        }
    019
    020        public TypeSig(String simpleName,
    021                    /*@ non_null */ javafe.tc.Env enclosingEnv,
    022                    /*@ non_null */ TypeDecl decl) {
    023            super(simpleName,enclosingEnv,decl);
    024        }
    025
    026        public FieldDeclVec jmlFields;
    027        public FieldDeclVec jmlHiddenFields;
    028        public FieldDeclVec jmlDupFields;
    029
    030        public boolean hasField(Identifier id) {
    031            // FIXME: jmlFIelds can be null for a JMLDataGroup
    032            prep();
    033            if (FlowInsensitiveChecks.inAnnotation && jmlFields != null) {
    034                for (int i=0; i<jmlFields.size(); ++i) {
    035                    if (jmlFields.elementAt(i).id.equals(id)) return true;
    036                }
    037            }
    038            return super.hasField(id);
    039        }
    040
    041            //@ also
    042            //@   requires caller != null;
    043        public FieldDecl lookupField(Identifier id,
    044                                     javafe.tc.TypeSig caller)
    045                    throws LookupException {
    046            FieldDecl r = null;
    047            prep();
    048            // FIXME: jmlFIelds can be null for a JMLDataGroup
    049            if (FlowInsensitiveChecks.inAnnotation && jmlFields != null) {
    050                for (int i=0; i<jmlFields.size(); ++i) {
    051                    if (jmlFields.elementAt(i).id.equals(id)) {
    052                        if (r == null) r = jmlFields.elementAt(i);
    053                        else throw new LookupException( LookupException.AMBIGUOUS );
    054                    }
    055                }
    056                for (int i=0; i<jmlDupFields.size(); ++i) {
    057                    if (jmlDupFields.elementAt(i).id.equals(id)) {
    058                        throw new LookupException( LookupException.AMBIGUOUS );
    059                    }
    060                }
    061            }
    062            if (r != null) return r;
    063            return super.lookupField(id,caller);
    064        }
    065    }