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 }