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                                     /*@non_null*/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    }