    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package javafe.tc;
    004
    005    import java.util.Hashtable;
    006
    007    import javafe.ast.*;
    008    import javafe.util.*;
    009
    010    /**
    011     * Does disambiguation and flow insensitive checks on a type
    012     * declaration.
    013     */
    014
    015    public class FlowInsensitiveChecks
    016    {
    017        static public FlowInsensitiveChecks inst = new FlowInsensitiveChecks();
    018        static public FlowInsensitiveChecks inst() { return inst; }
    019
    020        /**
    021         * Controls whether or not implicit super-calls in constructors
    022         * are made explicit.  By default they are.
    023         */
    024        public static boolean dontAddImplicitConstructorInvocations = false;
    025
    026        // Use this to get an instance in order to get proper derived behavior.
    027        protected FlowInsensitiveChecks() { }
    028
    029        /**
    030         * Factory method so subclasses can override.
    031         */
    032        //@ requires s != null;
    033        //@ ensures \result != null;
    034        protected EnvForTypeSig makeEnvForTypeSig(TypeSig s,
    035                                                  boolean staticContext) {
    036            return s.getEnv(staticContext);
    037        }
    038
    039
    040        ///////////////////////////////////////////////////////////////////////
    041        //                                                                   //
    042        // Information that remains the same during processing of entire     //
    043        // type decl.                                                        //
    044        //                                                                   //
    045        ///////////////////////////////////////////////////////////////////////
    046
    047        //@ invariant sig != null ==> rootIEnv != null && rootSEnv != null;
    048        /*@ spec_public */ protected TypeSig sig;
    049
    050        // Inv: rootIEnv.peer == sig; !rootIEnv.staticContext
    051        /*@ spec_public */ protected EnvForTypeSig rootIEnv;
    052
    053        // Inv: rootIEnv.peer == sig; !rootIEnv.staticContext
    054        /*@ spec_public */ protected EnvForTypeSig rootSEnv;
    055
    056
    057        ///////////////////////////////////////////////////////////////////////
    058        //                                                                   //
    059        // Information that changes for the processing of each member of     //
    060        // the decl.                                                         //
    061        //                                                                   //
    062        ///////////////////////////////////////////////////////////////////////
    063
    064        //* Cannot access fields defined later?
    065        protected boolean leftToRight;
    066
    067        //* Type for return statements.
    068        protected Type returnType;
    069
    070
    071        ///////////////////////////////////////////////////////////////////////
    072        // Information that changes within a member in a stack-like          //
    073        // manner.                                                           //
    074        ///////////////////////////////////////////////////////////////////////
    075
    076        //@ invariant allowedExceptions != null;
    077        protected TypeSigVec allowedExceptions = TypeSigVec.make();
    078
    079        //@ invariant enclosingLabels != null;
    080        protected StmtVec enclosingLabels = StmtVec.make();
    081
    082        // -------------------------------------------------------------
    083        /**
    084         * Moves <code>s</code> into implementation checked state.
    085         *
    086         */
    087        //@ requires (* <code>s</code> is in prepped state.*);
    088        //@ requires s.state >= TypeSig.PREPPED;
    089        public void checkTypeDeclaration(/*@ non_null @*/ TypeSig s) {
    090            Assert.precondition(s.state >= TypeSig.PREPPED);
    091
    092            // Set up variables for entire traversal:
    093            rootSEnv = makeEnvForTypeSig(s, true);
    094            rootIEnv = makeEnvForTypeSig(s, false);
    095            sig = s;
    096
    097            TypeDecl d = s.getTypeDecl();
    098
    099            // Process each member declaration
    100            for(int i = 0, sz = d.elems.size(); i < sz; i++) {
    101                TypeDeclElem e = d.elems.elementAt(i);
    102                checkTypeDeclElem(e);
    103            }
    104
    105            // Process ModifierPragmas
    106            checkModifierPragmaVec(d.pmodifiers, d, rootSEnv);
    107
    108            sig = null;
    109        }
    110
    111        // -------------------------------------------------------------
    112
    113        /**
    114         * Moves <code>fd</code> into implementation checked state.
    115         *
    116         */
    117        //@ requires (* <code>fd</code> is in prepped state. *);
    118        //@ modifies sig, rootSEnv, rootIEnv;
    119        public void checkFieldDecl(/*@ non_null @*/ FieldDecl fd) {
    120            /*
    121             * Special case for free-floating fields like length.
    122             *
    123             * Such fields must not have any modifier pragmas or an initializer.
    124             */
    125            if (fd.parent==null) {
    126                Assert.notFalse(fd.pmodifiers == null,   //@ nowarn Pre;
    127                                "Free-floating FieldDecls may not have any ModifierPragmas");
    128                Assert.notFalse(fd.init == null,         //@ nowarn Pre;
    129                                "Free-floating FieldDecls may not have initializers");
    130
    131                return;         // No other works needs to be done
    132            }
    133
    134
    135            TypeSig sig = TypeSig.getSig(fd.parent);
    136            if (sig.state < TypeSig.CHECKED) {
    137                // Type check this decl
    138
    139                // Info.out("[Pre-checking "+Types.printName(sig)+"."+fd.id+"]");
    140                sig.prep();
    141
    142                // Set up variables for entire traversal
    143                rootSEnv = makeEnvForTypeSig(sig, true);
    144                rootIEnv = makeEnvForTypeSig(sig, false);
    145                this.sig = sig;
    146
    147                checkTypeDeclElem(fd);
    148            }
    149            this.sig = null;
    150        }
    151
    152        //------------------------------------------------------------
    153
    154        // @note e must already have been prepped!
    155        //@ requires e != null && sig != null;
    156        //@ requires sig.state >= TypeSig.PREPPED;
    157        protected void checkTypeDeclElem(TypeDeclElem e) {
    158
    159            Assert.notNull(sig);
    160            Assert.notFalse(sig.state>= TypeSig.PREPPED);
    161            TypeDecl d = sig.getTypeDecl();
    162            boolean specOnly = d.specOnly;
    163
    164            switch (e.getTag()) {
    165
    166                case TagConstants.FIELDDECL: {
    167                    FieldDecl fd = (FieldDecl)e;
    168
    169                    // Process ModifierPragmas
    170                    Env rootEnv = Modifiers.isStatic(fd.modifiers) ? rootSEnv : rootIEnv;
    171                    checkModifierPragmaVec(fd.pmodifiers, fd, rootEnv);
    172                    checkTypeModifiers(rootEnv, fd.type);
    173
    174                    // Resolve the initializer of a field decl
    175                    if (fd.init != null) {
    176                        leftToRight = true;
    177                        allowedExceptions.removeAllElements();
    178                        Assert.notFalse(allowedExceptions.size() == 0);
    179                        fd.init = checkInit(rootEnv, fd.init, fd.type);
    180                    }
    181                    else if (Modifiers.isFinal(fd.modifiers) && !specOnly) {
    182                        // Removed for 1.1:
    183                        //  ErrorSet.caution(fd.locId,
    184                        //    "Final variables must be initialized");
    185                    }
    186                    break;
    187                }
    188
    189                case TagConstants.METHODDECL:
    190                case TagConstants.CONSTRUCTORDECL: {
    191                    RoutineDecl rd = (RoutineDecl) e;
    192                    Env rootEnv = Modifiers.isStatic(rd.modifiers)
    193                        ? rootSEnv : rootIEnv;
    194
    195                    // First do method/constructor specific stuff
    196                    if(rd instanceof MethodDecl) {
    197
    198                        MethodDecl md = (MethodDecl) e;
    199
    200                        checkTypeModifiers(rootEnv, md.returnType);
    201
    202                        returnType = md.returnType;
    203
    204                        if (md.body != null && !specOnly) {
    205
    206                            if(Modifiers.isAbstract(md.modifiers))
    207                                ErrorSet.error(md.loc,
    208                                               "An abstract method cannot include a body");
    209                            if(Modifiers.isNative(md.modifiers))
    210                                ErrorSet.error(md.loc,
    211                                               "A native method cannot include a body");
    212                        } else {
    213    /* We allow any method to have no body -- DRCok
    214                            if(!Modifiers.isAbstract(md.modifiers)
    215                               && !Modifiers.isNative(md.modifiers) && !specOnly)
    216                                ErrorSet.error(md.loc,
    217                                               "Method must include a body unless "
    218                                               +"it is declared abstract or native");
    219    */
    220                        }
    221                    } else {
    222                        // Constructor
    223                        ConstructorDecl cd = (ConstructorDecl)rd;
    224
    225                        // Was checked in parser
    226                        Assert.notFalse(!(d instanceof InterfaceDecl)); //@ nowarn Pre;
    227
    228                        // Modifiers were checked when we prep'ed the constructed
    229                        returnType = Types.voidType;
    230
    231                        // Check if we need to add an implicit constructor invocation
    232                        //@ assume !specOnly ==> cd.body != null;
    233                        if(!dontAddImplicitConstructorInvocations && !specOnly &&
    234                            cd.body != null && // FIXME - we've broken the assumption above by allowing spec files - need to fix that uniformly
    235                            !(cd.body.stmts.size() > 0
    236                              && cd.body.stmts.elementAt(0) instanceof
    237                              ConstructorInvocation)) {
    238                            // no explicit constructor invocation
    239                            if(sig != Types.javaLangObject()) {
    240                                // add implicit constructor invocation
    241
    242                                ExprVec args = ExprVec.make();
    243                                ConstructorInvocation ci
    244                                    = ConstructorInvocation.make(true, null, Location.NULL,
    245                                                                 cd.body.locOpenBrace,
    246                                                                 cd.body.locOpenBrace, args);
    247                                cd.body.stmts.insertElementAt(ci, 0);
    248                            }
    249                        }
    250                    }
    251
    252                    // Now do stuff common to methods and constructors.
    253
    254                    leftToRight = false;
    255                    enclosingLabels.removeAllElements();
    256
    257                    allowedExceptions.removeAllElements();
    258                    for(int j=0; j<rd.raises.size(); j++) {
    259                        TypeName n = rd.raises.elementAt(j);
    260                        rootEnv.resolveType(sig,n);
    261                        checkTypeModifiers(rootEnv, n);
    262                        allowedExceptions.addElement(TypeSig.getSig(n));
    263                    }
    264
    265                    Env env = new EnvForEnclosedScope(rootEnv);
    266                    for(int j = 0; j < rd.args.size(); j++) {
    267                        FormalParaDecl formal = rd.args.elementAt(j);
    268                        PrepTypeDeclaration.inst.
    269                            checkModifiers(formal.modifiers, Modifiers.ACC_FINAL,
    270                                           formal.getStartLoc(), "formal parameter");
    271                        checkModifierPragmaVec(formal.pmodifiers, formal, rootEnv);
    272
    273                        env = new EnvForLocals(env, formal);
    274                        checkTypeModifiers(env, formal.type);
    275                    }
    276
    277                    // Process ModifierPragmas
    278                    checkModifierPragmaVec(rd.pmodifiers, rd, env);
    279
    280                    if (rd.body != null) {
    281                        checkStmt(env, rd.body);
    282                    }
    283
    284                    break;
    285                }
    286
    287                case TagConstants.INITBLOCK: {
    288                    InitBlock si = (InitBlock) e;
    289                    PrepTypeDeclaration.inst.
    290                        checkModifiers(si.modifiers, Modifiers.ACC_STATIC,
    291                                       si.getStartLoc(), "initializer body");
    292                    Env rootEnv = Modifiers.isStatic(si.modifiers) ? rootSEnv : rootIEnv;
    293                    returnType = null;
    294                    checkStmt(new EnvForEnclosedScope(rootEnv), si.block);
    295                    break;
    296                }
    297
    298                case TagConstants.CLASSDECL:
    299                case TagConstants.INTERFACEDECL: {
    300                    TypeSig.getSig((TypeDecl)e).typecheck();
    301                    break;
    302                }
    303
    304                default:
    305                    if(e instanceof TypeDeclElemPragma)
    306                        checkTypeDeclElemPragma((TypeDeclElemPragma)e);
    307                    else
    308                        Assert.fail("Switch fall-through (" + e.getTag() + ")");
    309            }
    310        }
    311
    312
    313        /**
    314         * Typecheck a statement in a given environment then return the environment in
    315         * effect for statements that follow the given statement.
    316         *
    317         * <p> (The returned environment will be the same as the one passed in unless the
    318         * statement is a declaration.)
    319         *
    320         * </p>
    321         */
    322        //@ requires e != null && s != null;
    323        //@ requires !(e instanceof EnvForCU);
    324        //@ requires sig != null;
    325        //@ ensures \result != null;
    326        //@ ensures !(\result instanceof EnvForCU);
    327        protected Env checkStmt(Env e, Stmt s) {
    328
    329
    330            switch (s.getTag()) {
    331
    332                /*
    333                 * Handle declarations first:
    334                 */
    335
    336                case TagConstants.VARDECLSTMT: {
    337                    LocalVarDecl x = ((VarDeclStmt)s).decl;
    338                    e.resolveType(sig,x.type);
    339                    checkTypeModifiers(e, x.type);
    340                    PrepTypeDeclaration.inst.
    341                        checkModifiers(x.modifiers, Modifiers.ACC_FINAL,
    342                                       x.locId, "local variable");
    343                    checkModifierPragmaVec(x.pmodifiers, x, e);
    344
    345                    Env newEnv = new EnvForLocals(e,x);
    346                    if (x.init != null)
    347                        x.init = checkInit(newEnv, x.init, x.type);
    348                    return newEnv;
    349                }
    350
    351                case TagConstants.CLASSDECLSTMT: {
    352                    ClassDeclStmt cds = (ClassDeclStmt)s;
    353
    354                    // Create and check TypeSig for declared type:
    355                    // Note: this code was altered to pass the new environment including the
    356                    // new class into the TypeSig for the class.  Without that change, uses of
    357                    // the class name inside the class were not resolved.  I'm not sure that
    358                    // this is correct for all matters of scope and name visibility, but it
    359                    // solves this problem.  -- DRCok 10/2/2003
    360                    Env newenv = new EnvForLocalType(e, cds.decl);
    361                    TypeSig T = Types.makeTypeSig(cds.decl.id.toString(), newenv, cds.decl);
    362                    T.typecheck();
    363
    364                    return newenv;
    365                }
    366
    367
    368                    /*
    369                     * Next handle switch statement & associated statements; it needs
    370                     * special treatment to deal with labels properly.
    371                     */
    372
    373                case TagConstants.SWITCHLABEL:
    374                    Assert.precondition("Switch label passed to checkStmt!");
    375
    376
    377                case TagConstants.SWITCHSTMT: {
    378                    SwitchStmt c = (SwitchStmt)s;
    379                    c.expr = checkExpr(e, c.expr);
    380                    Env env = e;
    381
    382                    // Now do special handling of the following block with case stmts
    383
    384                    Type switchType = getType(c.expr);
    385                    if (!Types.isIntegralType(switchType)||Types.isLongType(switchType)) {
    386                        ErrorSet.error(c.expr.getStartLoc(),
    387                                       "The type of a switch expression must be char,"
    388                                       + " byte, short, or int.");
    389                        switchType = Types.intType;
    390                    }
    391
    392
    393                    // What case values encountered so far.
    394                    Hashtable switchValues = new Hashtable();
    395
    396                    boolean defaultEncountered = false;
    397                    enclosingLabels.addElement(c);
    398
    399                    for(int i = 0, sz = c.stmts.size(); i < sz; i++) {
    400                        Stmt stmt = c.stmts.elementAt(i);
    401
    402                        if (stmt.getTag() == TagConstants.SWITCHLABEL) {
    403                            SwitchLabel x = (SwitchLabel)stmt;
    404                            if (x.expr != null) {
    405                                x.expr = checkExpr(env, x.expr);
    406                                Object val = ConstantExpr.eval(x.expr);
    407                                // System.out.println("At "+Location.toString(x.expr.getStartLoc()));
    408
    409                                if(val == null)
    410                                    ErrorSet.error(x.loc, "Non-constant value in switch label");
    411                                else if(!ConstantExpr.
    412                                         constantValueFitsIn(val, (PrimitiveType)switchType))
    413                                    ErrorSet.error(x.loc,
    414                                                   "Case label value (" + val
    415                                                   +") not assignable to "
    416                                                   +"the switch expression type "
    417                                                   +Types.printName(switchType));
    418                                else {
    419                                    // Check if it is a duplicate
    420                                    // val may be Integer or Long, convert to Long for
    421                                    // duplicate checking
    422                                    Assert.notFalse(val instanceof Long    //@ nowarn Pre;
    423                                                    || val instanceof Integer);
    424                                    Long valLong = new Long(ConstantExpr.getLongConstant(val));
    425                                    if(switchValues.containsKey(valLong)) {
    426                                            // Point to dup label - FIXME
    427                                        ErrorSet.error(x.loc,
    428                                                       "Duplicate case label "+val
    429                                                       +" in switch statement");
    430                                    } else {
    431                                        switchValues.put(valLong,valLong);
    432                                    }
    433                                }
    434                            } else {
    435                                // this is default
    436                                if(defaultEncountered)
    437                                            // Point to dup label - FIXME
    438                                    ErrorSet.error(x.loc,
    439                                                   "Duplicate default label in switch statement");
    440                                else
    441                                    defaultEncountered = true;
    442                            }
    443
    444                        } else
    445                            env = checkStmt(env, stmt);
    446                    }
    447
    448                    enclosingLabels.pop();
    449                    return e;
    450                }
    451
    452
    453                    /*
    454                     * Finally handle remaining statements.
    455                     */
    456
    457                case TagConstants.BREAKSTMT:
    458                case TagConstants.CONTINUESTMT: {
    459                    BranchStmt bs = (BranchStmt)s;
    460                    Stmt dest = null;
    461                    int size = enclosingLabels.size();
    462
    463                    String expectedStmtKind =
    464                        s.getTag() == TagConstants.BREAKSTMT ? "switch, while, do, or for"
    465                        : "while, do or for" ;
    466
    467                    for(int i=size-1; i>=0 && dest==null; i--) {
    468                        Stmt ati = enclosingLabels.elementAt(i);
    469                        Stmt target
    470                            = ati instanceof LabelStmt ? ((LabelStmt)ati).stmt : ati;
    471
    472                        // continue target must be a loop statement
    473                        // unlabelled break target must be a loop or switch
    474                        // labelled break can be any statement
    475
    476                        boolean loopTarget =
    477                            (target instanceof ForStmt)
    478                            || (target instanceof WhileStmt)
    479                            || (target instanceof DoStmt);
    480
    481                        boolean validTarget =
    482                            loopTarget
    483                            || (s.getTag() == TagConstants.BREAKSTMT
    484                                && (target instanceof SwitchStmt
    485                                    || bs.label != null));
    486
    487                        if(bs.label == null) {
    488                            if(validTarget)
    489                                dest = target;
    490                            else
    491                                continue;
    492                        } else if(ati instanceof LabelStmt
    493                                   && ((LabelStmt)ati).label == bs.label) {
    494                            if(!validTarget)
    495                                ErrorSet.caution(bs.loc,
    496                                                 "Enclosing statement labelled '"
    497                                                 +bs.label+"' is not a "
    498                                                 +expectedStmtKind+" statement");
    499                            // just give a warning and continue, since javac accepts this
    500                            dest = target;
    501                        }
    502                        // else continue
    503                    }
    504
    505                    if(dest == null) {
    506                        ErrorSet.error(bs.loc,
    507                                       bs.label == null
    508                                       ? "No enclosing unlabelled "+expectedStmtKind+" statement"
    509                                       : "No enclosing "+expectedStmtKind+" statement labelled '"+bs.label+"'");
    510                    } else
    511                        setBranchLabel(bs, dest);
    512
    513                    return e;
    514                }
    515
    516                case TagConstants.SKIPSTMT:
    517                    return e;
    518
    519                case TagConstants.RETURNSTMT: {
    520                    ReturnStmt rs = (ReturnStmt)s;
    521
    522                    if(rs.expr != null)
    523                        rs.expr = checkExpr(e, rs.expr);
    524
    525                    if(returnType == null)
    526                        ErrorSet.error(rs.loc,
    527                                       "Returns are not allowed in a static initializer");
    528                    else {
    529                        if(rs.expr != null) {
    530                            Type res = getType(rs.expr);
    531
    532                            if(Types.isSameType(returnType, Types.voidType))
    533                                ErrorSet.error(rs.loc,
    534                                               "This routine is not expected to return a value");
    535                            else if(!assignmentConvertable(rs.expr, returnType)) {
    536                                if (!Types.isErrorType(res))
    537                                    ErrorSet.error(rs.loc,
    538                                                "Cannot convert "+Types.printName(res)
    539                                                +" to return type "+Types.printName(returnType));
    540                            }
    541                        } else {
    542                            if(!Types.isSameType(returnType, Types.voidType))
    543                                ErrorSet.error(rs.loc, "This routine must return a value");
    544                        }
    545                    }
    546                    return e;
    547                }
    548
    549                case TagConstants.THROWSTMT: {
    550                    ThrowStmt t = (ThrowStmt)s;
    551                    t.expr = checkExpr(e, t.expr);
    552                    Type res = getType(t.expr);
    553
    554                    if(!Types.isSubclassOf(res, Types.javaLangThrowable())) {
    555                        ErrorSet.error(t.loc,
    556                                        "Cannot throw values of type "+Types.printName(res));
    557                    } else {
    558
    559                        if (Types.isCheckedException(res)) {
    560
    561                            // Must be caught by try or throws clause
    562                            for(int i=0; i<allowedExceptions.size(); i++) {
    563                                if(Types.isSubclassOf(res, allowedExceptions.elementAt(i)))
    564                                    // is ok
    565                                    return e;
    566                            }
    567                            // Not caught
    568                            ErrorSet.error(t.loc,
    569                                            "Exception must be caught by an enclosing try "
    570                                            +"or throws clause");
    571                        }
    572                    }
    573                    return e;
    574                }
    575
    576                case TagConstants.BLOCKSTMT:
    577                    checkStmtVec(e, ((GenericBlockStmt)s).stmts);
    578                    return e;
    579
    580                case TagConstants.WHILESTMT: {
    581                    WhileStmt w = (WhileStmt)s;
    582                    w.expr = checkExpr(e, w.expr, Types.booleanType);
    583                    enclosingLabels.addElement(w);
    584                    checkStmt(e, w.stmt);
    585                    enclosingLabels.pop();
    586                    return e;
    587                }
    588
    589                case TagConstants.DOSTMT: {
    590                    DoStmt d = (DoStmt)s;
    591                    d.expr = checkExpr(e, d.expr, Types.booleanType);
    592                    enclosingLabels.addElement(d);
    593                    checkStmt(e, d.stmt);
    594                    enclosingLabels.pop();
    595                    return e;
    596                }
    597
    598                case TagConstants.IFSTMT: {
    599                    IfStmt i = (IfStmt)s;
    600                    i.expr = checkExpr(e, i.expr, Types.booleanType);
    601                    checkStmt(e, i.thn);
    602                    checkStmt(e, i.els);
    603                    return e;
    604                }
    605
    606                case TagConstants.SYNCHRONIZESTMT: {
    607                    SynchronizeStmt ss = (SynchronizeStmt)s;
    608                    ss.expr = checkExpr(e, ss.expr, Types.javaLangObject());
    609                    checkStmt(e, ss.stmt);
    610                    return e;
    611                }
    612
    613                case TagConstants.EVALSTMT: {
    614                    EvalStmt v = (EvalStmt) s;
    615                    v.expr = checkExpr(e, v.expr);
    616                    return e;
    617                }
    618
    619                case TagConstants.LABELSTMT: {
    620                    LabelStmt ls = (LabelStmt)s;
    621                    for(int i=0; i<enclosingLabels.size(); i++) {
    622                        Stmt enclosing = enclosingLabels.elementAt(i);
    623                        if(enclosing instanceof LabelStmt
    624                            && ((LabelStmt)enclosing).label == ls.label)
    625                            ErrorSet.error(ls.locId,
    626                                           "Label '"+ls.label+"' already used in this scope");
    627                                    // FIXME - point to dup
    628                    }
    629
    630                    enclosingLabels.addElement(ls);
    631                    checkStmt(e, ls.stmt);
    632                    enclosingLabels.pop();
    633
    634                    return e;
    635                }
    636
    637                case TagConstants.TRYFINALLYSTMT: {
    638                    TryFinallyStmt tf = (TryFinallyStmt)s;
    639                    checkStmt(e, tf.tryClause);
    640                    checkStmt(e, tf.finallyClause);
    641                    return e;
    642                }
    643
    644                case TagConstants.TRYCATCHSTMT: {
    645                    TryCatchStmt tc = (TryCatchStmt)s;
    646                    TypeSigVec newExceptions = allowedExceptions.copy();
    647
    648                    // add all catch clause exceptions to allowedExceptions
    649                    for(int i=0; i<tc.catchClauses.size(); i++) {
    650                        CatchClause c = tc.catchClauses.elementAt(i);
    651                        Type t = c.arg.type;
    652                        e.resolveType(sig,t);
    653                        checkTypeModifiers(e, t);
    654                        if(!Types.isSubclassOf(t, Types.javaLangThrowable()))
    655                            ErrorSet.error(c.loc,
    656                                            "Declared type of a catch formal parameter "
    657                                            +"must be a subclass of java.lang.Throwable");
    658                        else {
    659                            if (t instanceof TypeName) {
    660                                t = TypeSig.getSig((TypeName)t);
    661                            }
    662                            newExceptions.addElement((TypeSig)t);
    663                        }
    664                        PrepTypeDeclaration.inst.checkModifiers(c.arg.modifiers,
    665                                                                Modifiers.ACC_FINAL,
    666                                                                c.arg.getStartLoc(),
    667                                                                "formal parameter");
    668
    669                        EnvForLocals subenv = new EnvForLocals(e, c.arg, false);
    670                        checkStmt(subenv, c.body);
    671                    }
    672
    673                    TypeSigVec oldExceptions = allowedExceptions;
    674                    allowedExceptions = newExceptions;
    675                    checkStmt(e, tc.tryClause);
    676                    allowedExceptions = oldExceptions;
    677
    678                    return e;
    679                }
    680
    681                case TagConstants.FORSTMT: {
    682                    ForStmt f = (ForStmt) s;
    683                    Env se = checkStmtVec(e, f.forInit);
    684                    checkForLoopAfterInit(se, f);
    685                    return e;
    686                }
    687
    688                case TagConstants.CONSTRUCTORINVOCATION: {
    689                    ConstructorInvocation ci = (ConstructorInvocation)s;
    690
    691                    TypeSig calleeSig =
    692                        ci.superCall
    693                        ? TypeSig.getSig(((ClassDecl)sig.getTypeDecl()) //@nowarn Cast,NonNull;
    694                                         .superClass)
    695                        : sig;
    696
    697                    /*
    698                     * Everything before the constructor invocation call occurs is
    699                     * considered to be in a static context:
    700                     */
    701                    Env sEnv = e.asStaticContext();
    702
    703                    Type[] argTypes = checkExprVec(sEnv, ci.args);
    704
    705
    706                    /*
    707                     * Handle type checking/inference for enclosing instance ptr:
    708                     */
    709
    710                    // Get the type of calleeSig's enclosing instance or null if none
    711                    // exists:
    712                    TypeSig enclosingInstanceType = calleeSig.getEnv(false)
    713                        .getEnclosingInstance();
    714
    715                    // If calleeSig has an enclosing instance and the user didn't supply
    716                    // a value for it, try to infer one:
    717                    if (ci.enclosingInstance==null && enclosingInstanceType != null) {
    718                        ci.locDot = ci.getStartLoc();
    719                        ci.enclosingInstance =
    720                            sEnv.lookupEnclosingInstance(enclosingInstanceType,
    721                                                         ci.getStartLoc());
    722                    }
    723
    724                    if (ci.enclosingInstance != null) {
    725                        if (enclosingInstanceType != null)
    726                            ci.enclosingInstance = checkExpr(sEnv,
    727                                                             ci.enclosingInstance,
    728                                                             enclosingInstanceType);
    729                        else
    730                            ErrorSet.error(ci.enclosingInstance.getStartLoc(),
    731                                           "An enclosing instance may be provided only "
    732                                           + "when the superclass has an enclosing instance");
    733                    } else if (enclosingInstanceType != null) {
    734                        /*
    735                         * Compute appropriate error message details:
    736                         */
    737                        String details;
    738                        if (ci.locKeyword == sig.getTypeDecl().locOpenBrace) {
    739                            // inferred constructor with an inferred super inside it:
    740                            details = "cannot create a default constructor for class "
    741                                + sig + ".";
    742                        } else if (ci.locKeyword == ci.locOpenParen) {
    743                            // inferred super(...) in an explicit constructor:
    744                            details = "cannot create a default superclass constructor."
    745                                + "  (superclass is " + calleeSig + ")";
    746                        } else {
    747                            // explicit super(...) case...
    748                            details = "an explicit one must be"
    749                                + " provided when creating inner class "
    750                                + calleeSig + ".";
    751                        }
    752
    753                        ErrorSet.error(ci.getStartLoc(),
    754                                       "No enclosing instance of class "
    755                                       + enclosingInstanceType
    756                                       + " is in scope; " + details);
    757                    }
    758
    759
    760                    try {
    761                        ConstructorDecl cd
    762                            = calleeSig.lookupConstructor(argTypes, sig);
    763                        Assert.notNull(cd);
    764                        ci.decl = cd;
    765                    } catch(LookupException ex) {
    766                        // Don't print an error if superclass is an interface (an
    767                        // error has already been reported in this case)
    768                        if (! ci.superCall
    769                            || calleeSig.getTypeDecl().getTag() == TagConstants.CLASSDECL)
    770                            reportLookupException(ex,
    771                                                  "constructor " + calleeSig.getTypeDecl().id
    772                                                  + Types.printName(argTypes),
    773                                                  Types.printName(calleeSig),
    774                                                  ci.locKeyword);
    775                    }
    776
    777                    // Rest of constructor body is in the normal non-static context:
    778                    return e;
    779                }
    780
    781                case TagConstants.ASSERTSTMT: {
    782                    AssertStmt assertStmt = (AssertStmt)s;
    783                    if (assertStmt.label != null)
    784                        assertStmt.label = checkExpr(e, assertStmt.label);
    785                    assertStmt.pred = checkExpr(e, assertStmt.pred, Types.booleanType);
    786
    787                    // Turn a Java assert into a conditional throw and attach it to the
    788                    // AssertStmt.
    789
    790                    // assert Predicate ;
    791                    // ==>
    792                    // if (! Predicate)
    793                    //   throw new java.lang.AssertionError();
    794                    // or
    795                    // assert Predicate : LabelExpr ;
    796                    // ==>
    797                    // if (! Predicate)
    798                    //   throw new java.lang.AssertionError(LabelExpr);
    799                    int startLoc = assertStmt.getStartLoc();
    800                    int endLoc = assertStmt.getEndLoc();
    801                    Assert.notFalse(startLoc != Location.NULL);
    802                    UnaryExpr negatedPredicate =
    803                        UnaryExpr.make(TagConstants.NOT, assertStmt.pred, startLoc);
    804                    ParenExpr parenthesizedNegatedPredicate =
    805                        ParenExpr.make(negatedPredicate, startLoc, endLoc);
    806                    Name javaLangAssertionErrorName =
    807                        Name.make("java.lang.AssertionError", startLoc);
    808                    TypeName javaLangAssertionTypeName = TypeName.make(javaLangAssertionErrorName);
    809                    ExprVec constructorArgs = null;
    810                    if (assertStmt.label != null) {
    811                        Expr [] constructorArgsAsArray = { assertStmt.label };
    812                        constructorArgs = ExprVec.make(constructorArgsAsArray);
    813                    } else {
    814                        constructorArgs = ExprVec.make();
    815                    }
    816                    NewInstanceExpr newAssertionError =
    817                        NewInstanceExpr.make(null, Location.NULL, javaLangAssertionTypeName,
    818                                             constructorArgs, null, startLoc, endLoc);
    819                    ThrowStmt throwAssertionError = ThrowStmt.make(newAssertionError,
    820                                                                   startLoc);
    821                    Stmt elseSkip = SkipStmt.make(startLoc);
    822                    IfStmt ifStmt = IfStmt.make(parenthesizedNegatedPredicate, throwAssertionError,
    823                                                elseSkip, startLoc);
    824                    // Now typecheck the generated IfStmt so that it is fully resolved.
    825                    ifStmt.expr = checkExpr(e, ifStmt.expr, Types.booleanType);
    826                    checkStmt(e, ifStmt.thn);
    827                    checkStmt(e, ifStmt.els);
    828                    // Reattach this translated form to the AST node.
    829                    assertStmt.ifStmt = ifStmt;
    830
    831                    return e;
    832                }
    833
    834                default:
    835                    if(s instanceof StmtPragma)
    836                        checkStmtPragma(e, (StmtPragma)s);
    837                    else {
    838                        Assert.fail("Switch fall-through (" + s.getTag() + " " +
    839                            TagConstants.toString(s.getTag()) + " " +
    840                            Location.toString(s.getStartLoc()) + ")");
    841                    }
    842            }
    843            return e;                       // dummy
    844        }
    845
    846        //@ requires !(se instanceof EnvForCU);
    847        //@ requires sig != null;
    848        protected void checkForLoopAfterInit(/*@ non_null */ Env se,
    849                                             /*@ non_null */ ForStmt f) {
    850            f.test = checkExpr(se, f.test);
    851            for (int i = 0; i < f.forUpdate.size(); i++) {
    852                Expr ex = checkExpr(se, f.forUpdate.elementAt(i));
    853                f.forUpdate.setElementAt(ex, i);
    854            }
    855            enclosingLabels.addElement(f);
    856            checkStmt(se, f.body);
    857            enclosingLabels.pop();
    858        }
    859
    860        //@ requires env != null && v != null;
    861        //@ requires !(env instanceof EnvForCU);
    862        //@ requires sig != null;
    863        //@ ensures \result != null;
    864        //@ ensures !(\result instanceof EnvForCU);
    865        protected Env checkStmtVec(Env env, StmtVec v) {
    866            for(int i = 0, sz = v.size(); i < sz; i++) {
    867                Stmt stmt = v.elementAt(i);
    868
    869                env = checkStmt(env, stmt);
    870            }
    871
    872            return env;
    873        }
    874
    875
    876        //@ requires env != null && ev != null  ;
    877        //@ requires !(env instanceof EnvForCU);
    878        //@ requires sig != null;
    879        //@ ensures \nonnullelements(\result);
    880        protected Type[] checkExprVec(Env env, ExprVec ev) {
    881
    882            Type[] r = new Type[ ev.size() ];
    883
    884            for(int i = 0; i < ev.size(); i++) {
    885                Expr expr = ev.elementAt(i);
    886                Expr newExpr = checkExpr(env, expr);
    887                ev.setElementAt(newExpr, i);
    888                r[i] = getType(newExpr);
    889            }
    890
    891            return r;
    892        }
    893
    894
    895        //@ requires sig != null;
    896        //@ requires !(env instanceof EnvForCU);
    897        //@ requires env != null && x != null && expectedResult != null;
    898        //@ ensures \result != null;
    899        //@ ensures (x instanceof ArrayInit) ==> \result instanceof ArrayInit;
    900        protected VarInit checkInit(Env env, VarInit x, Type expectedResult) {
    901            if (x instanceof ArrayInit) {
    902                ArrayInit ai = (ArrayInit)x;
    903
    904                if(expectedResult instanceof ArrayType) {
    905                    Type elemType = ((ArrayType)expectedResult).elemType;
    906                    for(int i=0; i< ai.elems.size(); i++) {
    907                        VarInit disamb = checkInit(env, ai.elems.elementAt(i), elemType);
    908                        ai.elems.setElementAt(disamb, i);
    909                    }
    910                    setType(ai, expectedResult);
    911                } else {
    912                    ErrorSet.error(ai.locOpenBrace,
    913                                   "Unexpected array value in initializer");
    914                }
    915                return x;
    916
    917            } else {
    918                //@ assume \typeof(x) <: \type(Expr);
    919                return checkExpr(env, (Expr) x, expectedResult);
    920            }
    921        }
    922
    923        //@ requires env != null && e != null;
    924        //@ requires !(env instanceof EnvForCU);
    925        //@ requires sig != null;
    926        //@ ensures \result != null;
    927        protected Expr checkDesignator(Env env, Expr e) {
    928            Expr result = checkExpr(env, e);
    929            if (result.getTag() == TagConstants.FIELDACCESS) {
    930                FieldAccess fa = (FieldAccess)result;
    931                if (fa.decl == Types.lengthFieldDecl) {
    932                    ErrorSet.error(fa.locId, "Invalid designator");
    933                }
    934                // Note, if it weren't for some Java 1.1 features, one could also
    935                // rule out the case:
    936                //   fa.decl != null && Modifiers.isFinal(fa.decl.modifiers)
    937                // here with a message "Final fields cannot be used as designators",
    938                // but Java 1.1 allows assignments to final fields in some contexts.
    939                // A more elaborate test could perhaps be used, though.
    940            }
    941            return result;
    942        }
    943
    944        //@ requires env != null && expr != null && t != null;
    945        //@ requires !(env instanceof EnvForCU);
    946        //@ requires sig != null;
    947        //@ ensures \result != null;
    948        protected Expr checkExpr(Env env, Expr expr, Type t) {
    949            Expr ne = checkExpr(env,expr);
    950            checkType(ne, t);
    951            return ne;
    952        }
    953
    954        /**
    955         * This method should call <code>setType</code> on <code>x</code> before its
    956         * done.
    957         */
    958        //@ requires env != null && x != null;
    959        //@ requires !(env instanceof EnvForCU);
    960        //@ requires sig != null;
    961        //@ ensures \result != null;
    962        protected Expr checkExpr(Env env, Expr x) {
    963
    964            // System.out.println("Checking: "+Location.toString(x.getStartLoc()));
    965
    966            if (getTypeOrNull(x) != null)
    967                // already done
    968                return x;
    969
    970            // set default result type to integer, in case there is an error
    971            setType(x, Types.intType);
    972
    973            switch (x.getTag()) {
    974
    975                case TagConstants.THISEXPR: {
    976                    ThisExpr t = (ThisExpr)x;
    977
    978                    if (env.isStaticContext() && t.classPrefix==null) {
    979                        ErrorSet.error(x.getStartLoc(),
    980                           "Unqualified this cannot be used in static contexts");
    981                    }
    982
    983                    Type referredType = sig;
    984                    if (t.classPrefix != null) {
    985                        env.resolveType(sig,t.classPrefix);
    986                        referredType = t.classPrefix;
    987                        checkTypeModifiers(env, referredType);
    988
    989                        /*
    990                         * Check that t.classPrefix is the class of one of our
    991                         * current/enclosing instances:
    992                         */
    993                        TypeSig classPrefix = Types.toClassTypeSig(referredType);
    994                        if (classPrefix==null || !env.canAccessInstance(classPrefix)) {
    995                            ErrorSet.error(t.getStartLoc(),
    996                                           "Undefined variable: "
    997                                           + PrettyPrint.inst.toString(referredType)
    998                                           + ".this");
    999                            setType(x, Types.errorType);
    1000                            return x;
    1001                        }
    1002                    }
    1003
    1004                    setType(x, referredType);
    1005                    return x;
    1006                }
    1007
    1008                case TagConstants.STRINGLIT:
    1009                    setType(x, Types.javaLangString());
    1010                    return x;
    1011
    1012                case TagConstants.CHARLIT:
    1013                    setType(x, Types.charType);
    1014                    return x;
    1015
    1016                case TagConstants.BOOLEANLIT:
    1017                    setType(x, Types.booleanType);
    1018                    return x;
    1019
    1020                case TagConstants.FLOATLIT:
    1021                    setType(x, Types.floatType);
    1022                    return x;
    1023
    1024                case TagConstants.DOUBLELIT:
    1025                    setType(x, Types.doubleType);
    1026                    return x;
    1027
    1028                case TagConstants.INTLIT:
    1029                    setType(x, Types.intType);
    1030                    return x;
    1031
    1032                case TagConstants.LONGLIT:
    1033                    setType(x, Types.longType);
    1034                    return x;
    1035
    1036                case TagConstants.NULLLIT:
    1037                    setType(x, Types.nullType);
    1038                    return x;
    1039
    1040                case TagConstants.ARRAYREFEXPR: {
    1041                    ArrayRefExpr r = (ArrayRefExpr)x;
    1042
    1043                    r.array = checkExpr(env, r.array);
    1044                    Type arrType = getType(r.array);
    1045
    1046                    if(arrType instanceof ArrayType) {
    1047                        setType(r, ((ArrayType)arrType).elemType);
    1048                    } else {
    1049                        setType(r, Types.errorType);
    1050                        if (!Types.isErrorType(arrType))
    1051                            ErrorSet.error(r.locOpenBracket,
    1052                                        "Attempt to index a non-array value");
    1053                    }
    1054
    1055                    r.index = checkExpr(env, r.index);
    1056                    Type t = getType(r.index);
    1057                    Type ndxType = Types.isNumericType(t) ? Types.unaryPromote(t) : t;
    1058                    if(!Types.isSameType(ndxType, Types.intType) &&
    1059                       !Types.isErrorType(ndxType))
    1060                        ErrorSet.error(r.locOpenBracket, "Array index is not an integer");
    1061
    1062                    return r;
    1063                }
    1064
    1065                case TagConstants.NEWINSTANCEEXPR: {
    1066                    NewInstanceExpr ne = (NewInstanceExpr)x;
    1067
    1068                    /*
    1069                     * We handle the "scoping" of ne.type differently depending on
    1070                     * whether or not an explicit enclosing instance ptr is
    1071                     * provided:
    1072                     */
    1073                    TypeSig calleeSig;
    1074                    if (ne.enclosingInstance==null) {
    1075                        // 1.0 case:  new N(...) ...
    1076                        env.resolveType(sig,ne.type);
    1077                        checkTypeModifiers(env, ne.type);
    1078                        calleeSig = TypeSig.getSig(ne.type);
    1079                    } else {
    1080                        // 1.1 case: E.new I(...) ...
    1081
    1082                        // Type check E to get class type enclosingType:
    1083                        ne.enclosingInstance = checkExpr(env, ne.enclosingInstance);
    1084                        TypeSig enclosingInstanceType;
    1085                        try {
    1086                            enclosingInstanceType =
    1087                                (TypeSig)getType(ne.enclosingInstance);  //@ nowarn Cast;//caught
    1088                        } catch (ClassCastException E) {
    1089                            ErrorSet.error(ne.enclosingInstance.getStartLoc(),
    1090                                           "The enclosing instance supplied in a new"
    1091                                           + " expression must be of a class type.");
    1092                            enclosingInstanceType = Types.javaLangObject();
    1093                        }
    1094
    1095                        // Check and "resolve" I:
    1096                        if (ne.type.name.size() != 1)
    1097                            ErrorSet.error(ne.type.getStartLoc(),
    1098                                           "Only a simple name can be used after new"
    1099                                           + " when an enclosing instance is supplied.");
    1100                        Identifier id = ne.type.name.identifierAt(0);
    1101                        int idLoc = ne.type.name.locIdAt(0);
    1102                        calleeSig = enclosingInstanceType.lookupType(enclosingInstanceType, id, idLoc);
    1103                        if (calleeSig==null)
    1104                            ErrorSet.fatal(ne.type.getStartLoc(),
    1105                                           "No such type: "
    1106                                           + enclosingInstanceType.toString()+"$"+id);
    1107                        checkTypeModifiers(env, ne.type);
    1108                        TypeSig.setSig(ne.type, calleeSig);
    1109                    }
    1110
    1111
    1112                    /*
    1113                     * Handle remaining type checking/inference for enclosing instance ptr:
    1114                     */
    1115
    1116                    // Get the type of calleeSig's enclosing instance or null if none
    1117                    // exists:
    1118                    TypeSig enclosingInstanceType = calleeSig.getEnv(false)
    1119                        .getEnclosingInstance();
    1120
    1121                    // If calleeSig has an enclosing instance and the user didn't supply
    1122                    // a value for it, try to infer one:
    1123                    if (ne.enclosingInstance==null && enclosingInstanceType != null) {
    1124                        Expr enclosingInstance =
    1125                            env.lookupEnclosingInstance(enclosingInstanceType,
    1126                                                        ne.getStartLoc());
    1127                        if (enclosingInstance != null) {
    1128                            ne.locDot = ne.getStartLoc();
    1129                            ne.enclosingInstance = enclosingInstance;
    1130                            checkExpr(env, ne.enclosingInstance, enclosingInstanceType);
    1131                        }
    1132                    }
    1133
    1134                    if (ne.enclosingInstance != null) {
    1135                        if (enclosingInstanceType==null)
    1136                            ErrorSet.error(ne.enclosingInstance.getStartLoc(),
    1137                                           "An enclosing instance may be provided only "
    1138                                           + "when the named instance type is an inner class");
    1139                    } else if (enclosingInstanceType != null) {
    1140                        ErrorSet.error(ne.getStartLoc(),
    1141                                       "No enclosing instance of class "
    1142                                       + enclosingInstanceType
    1143                                       + " is in scope; an explicit one must be provided"
    1144                                       + " when creating instances of inner class "
    1145                                       + calleeSig + ".");
    1146                    }
    1147
    1148                    /*
    1149                     * The type that will *actually* call the constructor
    1150                     *
    1151                     * (matters if the constructor is "protected"!)
    1152                     */
    1153                    TypeSig caller = sig;
    1154
    1155                    /*
    1156                     * Handle anonymous class case:
    1157                     */
    1158                    if (ne.anonDecl != null) {
    1159                        // Update anonDecl to have proper supertype:
    1160                        if (calleeSig.getTypeDecl() instanceof ClassDecl) {
    1161                            Assert.notFalse(ne.anonDecl.superClass==null);  //@ nowarn Pre;
    1162                            ne.anonDecl.superClass = ne.type;
    1163                        } else {
    1164                            ne.anonDecl.superInterfaces.addElement(ne.type);
    1165                            calleeSig = Types.javaLangObject();
    1166                        }
    1167
    1168                        // Create and check TypeSig for declared type:
    1169                        TypeSig T = Types.makeTypeSig(null, env, ne.anonDecl);
    1170                        T.typecheck();
    1171                        caller = T;
    1172                        setType(ne, T);
    1173                    } else
    1174                        setType(ne, ne.type);
    1175
    1176
    1177                    Type[] argTypes = checkExprVec(env, ne.args);
    1178
    1179                    if (!(calleeSig.getTypeDecl() instanceof ClassDecl))
    1180                        ErrorSet.error(ne.loc,
    1181                                       "Cannot create an instance of an interface");
    1182                    else if (Modifiers.isAbstract(calleeSig.getTypeDecl().modifiers)
    1183                             && ne.anonDecl==null)
    1184                        ErrorSet.error(ne.loc,
    1185                                       "Cannot create an instance of an abstract class");
    1186                    else {
    1187                        try {
    1188                            ConstructorDecl cd = calleeSig.lookupConstructor(argTypes, caller);
    1189                            ne.decl = cd;
    1190                        } catch(LookupException e) {
    1191                            reportLookupException(e, "constructor",
    1192                                                  Types.printName(calleeSig), ne.loc);
    1193                        }
    1194                    }
    1195
    1196                    return ne;
    1197                }
    1198
    1199                case TagConstants.NEWARRAYEXPR: {
    1200                    NewArrayExpr na = (NewArrayExpr)x;
    1201                    env.resolveType(sig,na.type);
    1202                    Type r = na.type;
    1203                    checkTypeModifiers(env, r);
    1204                    for(int i = 0; i < na.dims.size(); i++) {
    1205                        Expr e = na.dims.elementAt(i);
    1206                        Expr newExpr = checkExpr(env, e, Types.intType);
    1207                        na.dims.setElementAt(newExpr, i);
    1208                        r = ArrayType.make(r, na.locOpenBrackets[i]);
    1209                        checkTypeModifiers(env, r);
    1210                    }
    1211                    setType(na, r);
    1212
    1213                    if (na.init != null)
    1214                        na.init = (ArrayInit)checkInit(env, na.init, r);
    1215
    1216                    return na;
    1217                }
    1218
    1219                case TagConstants.CONDEXPR: {
    1220                    CondExpr ce = (CondExpr)x;
    1221                    ce.test = checkExpr(env, ce.test, Types.booleanType);
    1222                    ce.thn = checkExpr(env, ce.thn);
    1223                    ce.els = checkExpr(env, ce.els);
    1224
    1225                    Type res = tryCondExprMatch(ce.thn, ce.els);
    1226                    if (res != null)
    1227                        setType(ce, res);
    1228                    else
    1229                        ErrorSet.error(ce.locQuestion,
    1230                                        "Incompatible arguments to the ?: operator");
    1231
    1232                    return ce;
    1233                }
    1234
    1235                case TagConstants.INSTANCEOFEXPR: {
    1236                    InstanceOfExpr ie = (InstanceOfExpr)x;
    1237                    ie.expr = checkExpr(env, ie.expr);
    1238                    Type exprType = getType(ie.expr);
    1239                    env.resolveType(sig,ie.type);
    1240                    checkTypeModifiers(env, ie.type);
    1241                    if(!Types.isReferenceType(ie.type)) {
    1242                        ErrorSet.error(ie.loc, "Non-reference type in instanceof operation");
    1243                    }
    1244                    else if(!Types.isCastable(exprType, ie.type)) {
    1245                        ErrorSet.error(ie.loc,
    1246                                       "Invalid instanceof operation: "+
    1247                                       "A value of type "+Types.printName(exprType)
    1248                                       +" can never be an instance of "
    1249                                       +Types.printName(ie.type));
    1250                    }
    1251                    setType(ie, Types.booleanType);
    1252                    return ie;
    1253                }
    1254
    1255                case TagConstants.CASTEXPR: {
    1256                    CastExpr ce = (CastExpr)x;
    1257                    ce.expr = checkExpr(env, ce.expr);
    1258                    Type exprType = getType(ce.expr);
    1259                    env.resolveType(sig,ce.type);
    1260                    checkTypeModifiers(env, ce.type);
    1261
    1262                    if(!Types.isCastable(exprType, ce.type)) {
    1263                        ErrorSet.error(ce.locOpenParen,
    1264                                       "Bad cast from "+Types.printName(exprType)
    1265                                       +" to "+Types.printName(ce.type));
    1266                    }
    1267                    setType(ce, ce.type);
    1268                    return ce;
    1269                }
    1270
    1271                case TagConstants.CLASSLITERAL: {
    1272                    ClassLiteral cl = (ClassLiteral)x;
    1273                    env.resolveType(sig,cl.type);
    1274                    checkTypeModifiers(env, cl.type);
    1275                    setType(cl, Types.javaLangClass());
    1276                    return cl;
    1277                }
    1278
    1279                case TagConstants.OR: case TagConstants.AND:
    1280                case TagConstants.BITOR: case TagConstants.BITXOR:
    1281                case TagConstants.BITAND: case TagConstants.NE:
    1282                case TagConstants.EQ: case TagConstants.GE:
    1283                case TagConstants.GT: case TagConstants.LE:
    1284                case TagConstants.LT: case TagConstants.LSHIFT:
    1285                case TagConstants.RSHIFT: case TagConstants.URSHIFT:
    1286                case TagConstants.ADD: case TagConstants.SUB:
    1287                case TagConstants.DIV: case TagConstants.MOD:
    1288                case TagConstants.STAR: {
    1289                    BinaryExpr be = (BinaryExpr)x;
    1290                    be.left = checkExpr(env, be.left);
    1291                    be.right = checkExpr(env, be.right);
    1292                    Type t = checkBinaryExpr(be.op, be.left, be.right, be.locOp);
    1293                    setType(be, t);
    1294                    return be;
    1295                }
    1296
    1297                case TagConstants.ASSIGN: case TagConstants.ASGMUL:
    1298                case TagConstants.ASGDIV: case TagConstants.ASGREM:
    1299                case TagConstants.ASGADD: case TagConstants.ASGSUB:
    1300                case TagConstants.ASGLSHIFT: case TagConstants.ASGRSHIFT:
    1301                case TagConstants.ASGURSHIFT: case TagConstants.ASGBITAND:
    1302                case TagConstants.ASGBITOR: case TagConstants.ASGBITXOR: {
    1303                    BinaryExpr be = (BinaryExpr)x;
    1304                    be.left = checkDesignator(env, be.left);
    1305                    be.right = checkExpr(env, be.right);
    1306                    Type t = checkBinaryExpr(be.op, be.left, be.right, be.locOp);
    1307                    setType(be, t);
    1308                    return be;
    1309                }
    1310
    1311                    // Unary operations
    1312
    1313                case TagConstants.UNARYADD:
    1314                case TagConstants.UNARYSUB: {
    1315                    UnaryExpr ue = (UnaryExpr)x;
    1316                    ue.expr = checkExpr(env, ue.expr);
    1317                    // Argument must be primitive numeric type
    1318                    Type t = getType(ue.expr);
    1319                    if(checkNumericType(ue.expr)) {
    1320                        // Result is value of unary promoted type of arg
    1321                        setType(ue, Types.unaryPromote(getType(ue.expr)));
    1322                    }
    1323                    return ue;
    1324                }
    1325
    1326                case TagConstants.BITNOT: {
    1327                    UnaryExpr ue = (UnaryExpr)x;
    1328                    ue.expr = checkExpr(env, ue.expr);
    1329                    // Argument must be primitive numeric type
    1330                    if(checkIntegralType(ue.expr)) {
    1331                        // Result is value of unary promoted type of arg
    1332                        setType(ue, Types.unaryPromote(getType(ue.expr)));
    1333                    }
    1334                    return ue;
    1335                }
    1336
    1337                case TagConstants.INC: case TagConstants.DEC:
    1338                case TagConstants.POSTFIXINC: case TagConstants.POSTFIXDEC: {
    1339                    UnaryExpr ue = (UnaryExpr)x;
    1340                    ue.expr = checkDesignator(env, ue.expr);
    1341
    1342                    if (ue.expr instanceof VariableAccess) {
    1343                        GenericVarDecl v = ((VariableAccess)ue.expr).decl;
    1344                        if (Modifiers.isFinal(v.modifiers))
    1345                            ErrorSet.caution(ue.expr.getStartLoc(),
    1346                                "May not assign to a final variable",
    1347                                v.getStartLoc());
    1348                    } else if (ue.expr instanceof FieldAccess) {
    1349                        GenericVarDecl v = ((FieldAccess)ue.expr).decl;
    1350                        // v is null if there was an error such as a field
    1351                        // name that does not exist
    1352                        if (v == Types.lengthFieldDecl)
    1353                            ErrorSet.error(ue.expr.getStartLoc(),
    1354                                "May not assign to array's length field");
    1355                        else if (v != null && Modifiers.isFinal(v.modifiers))
    1356                            ErrorSet.caution(ue.expr.getStartLoc(),
    1357                                "May not assign to a final field",
    1358                                v.getStartLoc());
    1359
    1360                    }
    1361                        // FIXME - need checks of more complicated expressions
    1362
    1363                    // Argument must be primitive numeric variable type
    1364                    if (checkNumericType(ue.expr)) {
    1365                        if(!isVariable(ue.expr))
    1366                            ErrorSet.error(ue.locOp,
    1367                                            "Argument of increment/decrement operation "
    1368                                            +"is not a location");
    1369                        // Result is of same type
    1370                        setType(ue, getType(ue.expr));
    1371                    }
    1372                    return ue;
    1373                }
    1374
    1375                case TagConstants.NOT: {
    1376                    // Argument must be boolean, result is boolean
    1377                    UnaryExpr ue = (UnaryExpr)x;
    1378                    ue.expr = checkExpr(env, ue.expr, Types.booleanType);
    1379                    setType(ue, Types.booleanType);
    1380                    return ue;
    1381                }
    1382
    1383                case TagConstants.PARENEXPR: {
    1384                    ParenExpr pe = (ParenExpr)x;
    1385                    pe.expr = checkExpr(env, pe.expr);
    1386                    setType(pe, getType(pe.expr));
    1387                    return pe;
    1388                }
    1389
    1390                case TagConstants.AMBIGUOUSVARIABLEACCESS: {
    1391                    AmbiguousVariableAccess av = (AmbiguousVariableAccess)x;
    1392                    Assert.notNull(av.name);
    1393                    Expr resolved = env.disambiguateExprName(av.name);
    1394                    if(resolved == null) {
    1395                        if (av.name.size() == 1) {
    1396                            ErrorSet.error(av.getStartLoc(),
    1397                                           "Undefined variable '" + av.name.printName() + "'");
    1398                        } else ErrorSet.error(av.getStartLoc(),
    1399                                            "Cannot resolve variable access '"
    1400                                            +av.name.printName()+"'");
    1401                        setType(x, Types.errorType);
    1402                        return av;
    1403                    }
    1404                    Assert.notFalse(resolved.getTag() !=
    1405                                    TagConstants.AMBIGUOUSVARIABLEACCESS);
    1406                    return checkExpr(env, resolved);
    1407                }
    1408
    1409                case TagConstants.FIELDACCESS: {
    1410                    FieldAccess fa = (FieldAccess)x;
    1411                    Type t = checkObjectDesignator(env, fa.od);
    1412                    if(t != null) {
    1413                        try {
    1414                            fa.decl = Types.lookupField(t, fa.id, sig);
    1415                            setType(fa, fa.decl.type);
    1416
    1417                            if (fa.od instanceof TypeObjectDesignator &&
    1418                                !Modifiers.isStatic(fa.decl.modifiers)) {
    1419                                // Is fa.decl an instance field of the same class as
    1420                                // fa is part of?
    1421                                boolean thisField = false;
    1422                                if (fa.decl.parent != null)
    1423                                    thisField = (env.getEnclosingClass()
    1424                                                 .isSubtypeOf(TypeSig.getSig(fa.decl.parent)));
    1425                                if (thisField ||
    1426                                    ((TypeObjectDesignator)fa.od).type instanceof TypeName)
    1427                                    ErrorSet.error(fa.locId,
    1428                                                   "An instance field may be accessed only via "
    1429                                                   + "an object and/or from a non-static"
    1430                                                   + " context or an inner class enclosed"
    1431                                                   + " by a type possessing that field.");
    1432                                            // FIXME - point to declaration
    1433                                else
    1434                                    ErrorSet.error(fa.locId,
    1435                                                   "The instance fields of type "
    1436                                                   + ((TypeObjectDesignator)fa.od).type
    1437                                                   + " may not be accessed from type "
    1438                                                   + sig);
    1439                                            // FIXME = point to declaration
    1440                            }
    1441                        } catch(LookupException ex) {
    1442                            if (!Types.isErrorType(t))
    1443                                reportLookupException(ex, "field",
    1444                                    Types.printName(t), fa.locId);
    1445                            setType(fa, Types.errorType);
    1446                        }
    1447                    }
    1448                    return fa;
    1449                }
    1450
    1451                case TagConstants.AMBIGUOUSMETHODINVOCATION: {
    1452                    AmbiguousMethodInvocation ami = (AmbiguousMethodInvocation)x;
    1453                    MethodInvocation resolved = env.disambiguateMethodName(ami);
    1454                    if (resolved == null) {
    1455                        // This currently never happens because non-resolvable
    1456                        // ambiguous methods result in a fatal error.  (See EnvForTypeSig)
    1457                        ErrorSet.error(ami.getStartLoc(),
    1458                                        "Ambiguous method invocation");
    1459                        return ami;
    1460                    }
    1461                    return checkExpr(env, resolved);
    1462                }
    1463
    1464                case TagConstants.METHODINVOCATION: {
    1465                    MethodInvocation mi = (MethodInvocation)x;
    1466                    Type t = checkObjectDesignator(env, mi.od);
    1467                    Type[] argTypes = checkExprVec(env, mi.args);
    1468                    if(t != null) {
    1469                        try {
    1470                            mi.decl = Types.lookupMethod(t, mi.id, argTypes, sig);
    1471                            setType(mi, mi.decl.returnType);
    1472
    1473                            if (mi.od instanceof TypeObjectDesignator &&
    1474                                !Modifiers.isStatic(mi.decl.modifiers)) {
    1475                                // Is mi.decl an instance method of the same class as
    1476                                // mi is part of?
    1477                                boolean thisMethod = false;
    1478                                if (mi.decl.parent != null)
    1479                                    thisMethod =
    1480                                        env.getEnclosingClass().isSubtypeOf(TypeSig.getSig(mi.decl.parent));
    1481
    1482                                if (thisMethod ||
    1483                                    ((TypeObjectDesignator)mi.od).type instanceof TypeName)
    1484                                    ErrorSet.error(mi.locId, "An instance method may be invoked" +
    1485                                                   " only via an object and/or from a non-static" +
    1486                                                   " context or an inner class enclosed by a type" +
    1487                                                   " possessing that method.");
    1488                                else
    1489                                    ErrorSet.error(mi.locId,
    1490                                                   "The instance methods of type "
    1491                                                   + ((TypeObjectDesignator)mi.od).type
    1492                                                   + " may not be invoked from type "
    1493                                                   + sig);
    1494                            }
    1495                        } catch(LookupException ex) {
    1496                            if (!Types.isErrorType(t))
    1497                                reportLookupException(ex,
    1498                                                  "method "+mi.id
    1499                                                  +Types.printName(argTypes),
    1500                                                  Types.printName(t), mi.locId);
    1501                            setType(mi, Types.errorType);
    1502                        }
    1503                    }
    1504                    return mi;
    1505                }
    1506
    1507                case TagConstants.VARIABLEACCESS: {
    1508                    VariableAccess lva = (VariableAccess)x;
    1509                    setType(lva, lva.decl.type);
    1510                    Assert.notNull(getType(lva));
    1511
    1512                    // Front-end VariableAccess's never point to fields:
    1513                    Assert.notFalse(!(lva.decl instanceof FieldDecl)); //@ nowarn Pre;
    1514
    1515                    // Make sure only access final variables from enclosing instances:
    1516                    if (Env.whereDeclared(lva.decl) != sig &&
    1517                        !Modifiers.isFinal(lva.decl.modifiers))
    1518                        ErrorSet.error(lva.loc,
    1519                                       "Attempt to use a non-final variable"
    1520                                       + " from a different method.  From enclosing"
    1521                                       + " blocks, only final local variables are"
    1522                                       + " available.");
    1523
    1524                    return lva;
    1525                }
    1526
    1527                default:
    1528                    System.out.println("FAIL " + x);
    1529                    System.out.println(" AT " + Location.toString(x.getStartLoc()));
    1530                    Assert.fail("Switch fall-through (" +
    1531                                TagConstants.toString(x.getTag()) + ")");
    1532                    return null;            // Dummy
    1533            }
    1534        }
    1535
    1536        // ======================================================================
    1537
    1538        //@ requires env != null && od != null;
    1539        //@ requires !(env instanceof EnvForCU);
    1540        //@ requires sig != null;
    1541        protected Type checkObjectDesignator(Env env, ObjectDesignator od) {
    1542
    1543            switch(od.getTag()) {
    1544
    1545                case TagConstants.EXPROBJECTDESIGNATOR: {
    1546                    ExprObjectDesignator eod = (ExprObjectDesignator)od;
    1547                    eod.expr = checkExpr(env, eod.expr);
    1548                    eod.type = getType(eod.expr);
    1549                    return eod.type;
    1550                }
    1551
    1552                case TagConstants.TYPEOBJECTDESIGNATOR: {
    1553                    TypeObjectDesignator tod = (TypeObjectDesignator)od;
    1554                    // Type has been created by disambiguation code, so it is ok.
    1555
    1556                    Type t = tod.type;
    1557                    if(t instanceof TypeName) {
    1558                        t = TypeSig.getSig((TypeName)t);
    1559                        tod.type = t;
    1560                    }
    1561                    Assert.notFalse(t instanceof TypeSig);
    1562                    checkTypeModifiers(env, t);
    1563                    return (TypeSig)t;
    1564                }
    1565
    1566                case TagConstants.SUPEROBJECTDESIGNATOR: {
    1567                    SuperObjectDesignator sod = (SuperObjectDesignator)od;
    1568                    if(env.isStaticContext()) {
    1569                        ErrorSet.error(sod.locSuper,
    1570                                       "Keyword super cannot be used in a static context");
    1571                        return null;
    1572                    }
    1573                    else {
    1574                        TypeDecl d = sig.getTypeDecl();
    1575                        if (d instanceof ClassDecl) {
    1576                            TypeName superClass = ((ClassDecl)d).superClass;
    1577                            if (superClass==null) {
    1578                                Assert.notFalse(sig==Types.javaLangObject()); //@ nowarn Pre;
    1579                                ErrorSet.error(sod.locDot,
    1580                                                "Can't use keyword super in java.lang.Object");
    1581                                return null;
    1582                            }
    1583
    1584                            TypeSig ts = TypeSig.getSig(superClass);
    1585                            sod.type = ts;
    1586                            return ts;
    1587                        } else {
    1588                            ErrorSet.error(sod.locDot,
    1589                                            "Can't use keyword super in an interface");
    1590                            return null;
    1591                        }
    1592                    }
    1593                }
    1594
    1595                default:
    1596                    Assert.fail("Fall thru");
    1597                    return null; // dummy return
    1598            }
    1599        }
    1600
    1601        // ======================================================================
    1602
    1603        /**
    1604         * Return the type of a E1 : L ? R expression given the typechecked Expr's for L
    1605         * and R, as per JLS 15.24.
    1606         *
    1607         * @return null if the given combination is illegal.
    1608         */
    1609        //@ requires leftExpr != null && rightExpr != null;
    1610        private Type tryCondExprMatch(Expr leftExpr, Expr rightExpr) {
    1611            Type leftType = getType(leftExpr);
    1612            Type rightType = getType(rightExpr);
    1613
    1614            /*
    1615             * If the second and third operands have the same type,
    1616             * then than is the type of the conditional expression:
    1617             */
    1618            if (Types.isSameType(leftType, rightType))
    1619                return leftType;
    1620
    1621
    1622            /*
    1623             * Rules for case where both L and R have numeric types:
    1624             */
    1625            if (Types.isNumericType(leftType)
    1626                && Types.isNumericType(rightType)) {
    1627                /*
    1628                 * If one of the operands is of type byte
    1629                 * and the other is of type short,
    1630                 * then the type of the conditional expression is short:
    1631                 */
    1632                if (Types.isSameType(leftType, Types.byteType) &&
    1633                    Types.isSameType(rightType, Types.shortType))
    1634                    return Types.shortType;
    1635                if (Types.isSameType(rightType, Types.byteType) &&
    1636                    Types.isSameType(leftType, Types.shortType))
    1637                    return Types.shortType;
    1638
    1639                /*
    1640                 * If one of the operands is of type T where T is byte/short/char,
    1641                 * and the other operand is a constant expression of type int
    1642                 * whose value is representable in type T,
    1643                 * then the type of the conditional expression is T.
    1644                 */
    1645                if ((Types.isSameType(leftType, Types.byteType) ||
    1646                     Types.isSameType(leftType, Types.shortType) ||
    1647                     Types.isSameType(leftType, Types.charType))
    1648                    && ConstantExpr.
    1649                    constantValueFitsIn(ConstantExpr.eval(rightExpr),
    1650                                        (PrimitiveType)leftType))
    1651                    return leftType;
    1652                if ((Types.isSameType(rightType, Types.byteType) ||
    1653                     Types.isSameType(rightType, Types.shortType) ||
    1654                     Types.isSameType(rightType, Types.charType))
    1655                    && ConstantExpr.
    1656                    constantValueFitsIn(ConstantExpr.eval(leftExpr),
    1657                                        (PrimitiveType)rightType))
    1658                    return rightType;
    1659
    1660
    1661                /*
    1662                 * Otherwise, binary numeric promotion (5.6.2) is applied
    1663                 * to the operand types, and the type of the conditional
    1664                 * expression is the promoted type:
    1665                 */
    1666                return Types.binaryNumericPromotion(leftType, rightType);
    1667            }
    1668
    1669
    1670            /*
    1671             * If one operands is of the null type and the other is
    1672             * a reference type, then the result type is that reference type
    1673             */
    1674            if (Types.isSameType(leftType, Types.nullType) &&
    1675                Types.isReferenceType(rightType))
    1676                return rightType;
    1677            if (Types.isSameType(rightType, Types.nullType) &&
    1678                Types.isReferenceType(leftType))
    1679                return leftType;
    1680
    1681
    1682            /*
    1683             * If the second and third operands are of different reference
    1684             * types, then it must be possible to convert one of the types
    1685             * to the other type (call this latter type T) by assignment
    1686             * conversion (5.2); the type of the conditional expression
    1687             * is T. It is a compile-time error if neither type is
    1688             * assignment compatible with the other type.
    1689             */
    1690            if (Types.isReferenceType(leftType)
    1691                && Types.isReferenceType(rightType)) {
    1692                if (assignmentConvertable(leftExpr, rightType))
    1693                    return rightType;
    1694                if (assignmentConvertable(rightExpr, leftType))
    1695                    return leftType;
    1696            }
    1697
    1698            // Invalid combination
    1699            return null;
    1700
    1701        }
    1702
    1703        // ======================================================================
    1704
    1705        //@ requires left != null && right != null;
    1706        //@ requires loc != Location.NULL;
    1707        //@ ensures \result != null  ;
    1708        protected Type checkBinaryExpr(int op, Expr left, Expr right, int loc) {
    1709
    1710            Type leftType = getType(left);
    1711            Type rightType = getType(right);
    1712
    1713            switch(op) {
    1714
    1715                case TagConstants.ADD:
    1716
    1717                    if(Types.isSameType(leftType, Types.javaLangString())
    1718                        || Types.isSameType(rightType, Types.javaLangString())) {
    1719
    1720                        // Operation is string concatenation
    1721                        return Types.javaLangString();
    1722                    }
    1723                    // else fall thru
    1724
    1725                case TagConstants.STAR:
    1726                case TagConstants.DIV:
    1727                case TagConstants.MOD:
    1728                case TagConstants.SUB: {
    1729                    if(checkNumericType(left)
    1730                        && checkNumericType(right))
    1731                        return Types.binaryNumericPromotion(leftType, rightType);
    1732                    else
    1733                        // error recovery
    1734                        return Types.intType;
    1735                }
    1736
    1737                case TagConstants.LSHIFT:
    1738                case TagConstants.RSHIFT:
    1739                case TagConstants.URSHIFT:
    1740
    1741                    // Arguments must be primitive integral types
    1742                    // result is unary promoted type of left operand
    1743
    1744                    if(checkIntegralType(left)
    1745                        && checkIntegralType(right))
    1746                        return Types.unaryPromote(leftType);
    1747                    else
    1748                        // error recovery
    1749                        return Types.intType;
    1750
    1751                case TagConstants.LT:
    1752                case TagConstants.LE:
    1753                case TagConstants.GT:
    1754                case TagConstants.GE:
    1755
    1756                    // Arguments must be primitive numeric types
    1757                    // result is boolean
    1758
    1759                    checkNumericType(left);
    1760                    checkNumericType(right);
    1761                    return Types.booleanType;
    1762
    1763                case TagConstants.BITAND:
    1764                case TagConstants.BITOR:
    1765                case TagConstants.BITXOR: {
    1766                    if(!Types.isBooleanType(leftType)) {
    1767
    1768                        // Arguments are primitive integral
    1769                        // binary numeric promotion is performed
    1770                        // type of result is promoted type of operands
    1771
    1772                        if(checkIntegralType(left)
    1773                            && checkIntegralType(right))
    1774                            return Types.binaryNumericPromotion(leftType, rightType);
    1775                        else
    1776                            // error recovery
    1777                            return Types.intType;
    1778                    }
    1779
    1780                    // else fall thru. Arguments must be boolean, result is boolean
    1781                }
    1782
    1783                case TagConstants.AND:
    1784                case TagConstants.OR: {
    1785                    // Arguments must be boolean, result is also boolean
    1786                    checkType(left, Types.booleanType);
    1787                    checkType(right, Types.booleanType);
    1788                    return Types.booleanType;
    1789                }
    1790
    1791                case TagConstants.EQ:
    1792                case TagConstants.NE:
    1793                    if( (Types.isNumericType(leftType)
    1794                           && Types.isNumericType(rightType))
    1795                          || (!Types.isVoidType(leftType)
    1796                              && Types.isSameType(leftType, rightType))
    1797                          || (Types.isReferenceOrNullType(leftType)
    1798                              && Types.isReferenceOrNullType(rightType))) {
    1799
    1800                        if(  Types.isCastable(leftType, rightType)
    1801                              || Types.isCastable(rightType, leftType)) {
    1802                            // is ok, result boolean
    1803                            return Types.booleanType;
    1804                        }
    1805                    }
    1806
    1807                    // Fall thru to here on error
    1808
    1809                    if (!Types.isErrorType(leftType) && !Types.isErrorType(rightType)) {
    1810                        ErrorSet.error(loc,
    1811                                   "Invalid types ("+Types.printName(leftType)
    1812                                   +" and "+Types.printName(rightType)
    1813                                   +") in equality comparison");
    1814                    }
    1815                    return Types.booleanType;
    1816
    1817                case TagConstants.ASSIGN:
    1818                case TagConstants.ASGMUL:
    1819                case TagConstants.ASGDIV:
    1820                case TagConstants.ASGREM:
    1821                case TagConstants.ASGADD:
    1822                case TagConstants.ASGSUB:
    1823                case TagConstants.ASGLSHIFT:
    1824                case TagConstants.ASGRSHIFT:
    1825                case TagConstants.ASGURSHIFT:
    1826                case TagConstants.ASGBITAND:
    1827                case TagConstants.ASGBITOR:
    1828                case TagConstants.ASGBITXOR: {
    1829                    if (left instanceof VariableAccess) {
    1830                        GenericVarDecl v = ((VariableAccess)left).decl;
    1831                        if (Modifiers.isFinal(v.modifiers) &&
    1832                            (v instanceof FormalParaDecl ||
    1833                            (v instanceof LocalVarDecl &&
    1834                                ((LocalVarDecl)v).init != null)
    1835                            ))
    1836                            ErrorSet.caution(left.getStartLoc(),
    1837                                "May not assign to a final variable",
    1838                                v.getStartLoc());
    1839                    } else if (left instanceof FieldAccess) {
    1840                        GenericVarDecl v = ((FieldAccess)left).decl;
    1841                        // v is null if there was an error such as a field
    1842                        // name that does not exist
    1843                        if (v == Types.lengthFieldDecl)
    1844                            ErrorSet.error(left.getStartLoc(),
    1845                                "May not assign to array's length field");
    1846                        else if (v != null && Modifiers.isFinal(v.modifiers) &&
    1847                            v instanceof FieldDecl &&
    1848                            ((FieldDecl)v).init != null)
    1849                            ErrorSet.caution(left.getStartLoc(),
    1850                                "May not assign to a final field",
    1851                                v.getStartLoc());
    1852
    1853                    }
    1854                        // FIXME - need checks of more complicated expressions
    1855
    1856                    if(!isVariable(left)) {
    1857                        if (!Types.isErrorType(leftType)) ErrorSet.error(loc,
    1858                                       "Left hand side of assignment operator "+
    1859                                       "is not a location");
    1860                    } else if(op == TagConstants.ASSIGN) {
    1861                        if(!assignmentConvertable(right, leftType) &&
    1862                            !Types.isErrorType(getType(right)) && !Types.isErrorType(leftType))
    1863                            ErrorSet.error(loc,
    1864                                           "Value of type "+Types.printName(getType(right))
    1865                                           +" cannot be assigned to location of type "
    1866                                           + Types.printName(leftType));
    1867                    } else {
    1868                        // E1 op= E2 is equivalent to
    1869                        // E1 = (T)(E1 op E2), where T is type of E1
    1870                        int simpleop;
    1871                        switch(op) {
    1872                            case TagConstants.ASGMUL:    simpleop=TagConstants.STAR;    break;
    1873                            case TagConstants.ASGDIV:    simpleop=TagConstants.DIV;     break;
    1874                            case TagConstants.ASGREM:    simpleop=TagConstants.MOD;     break;
    1875                            case TagConstants.ASGADD:    simpleop=TagConstants.ADD;     break;
    1876                            case TagConstants.ASGSUB:    simpleop=TagConstants.SUB;     break;
    1877                            case TagConstants.ASGLSHIFT: simpleop=TagConstants.LSHIFT;  break;
    1878                            case TagConstants.ASGRSHIFT: simpleop=TagConstants.RSHIFT;  break;
    1879                            case TagConstants.ASGURSHIFT:simpleop=TagConstants.URSHIFT; break;
    1880                            case TagConstants.ASGBITAND: simpleop=TagConstants.BITAND;  break;
    1881                            case TagConstants.ASGBITOR:  simpleop=TagConstants.BITOR;   break;
    1882                            case TagConstants.ASGBITXOR: simpleop=TagConstants.BITXOR;  break;
    1883                            default: Assert.fail("Incomplete case"); simpleop=0; // dummy init
    1884                        }
    1885                        Type result = checkBinaryExpr(simpleop, left, right, loc);
    1886                        // Check if result is convertable to leftType
    1887                        if(!Types.isCastable(result, leftType))
    1888                            ErrorSet.error(loc,
    1889                                           "Result type "+Types.printName(result)
    1890                                           +" of assignment operation cannot be cast to type "
    1891                                           +Types.printName(leftType));
    1892                    }
    1893                    // done
    1894                    return leftType;
    1895                }
    1896
    1897                default:
    1898                    Assert.fail("Fall thru, op = "+op);
    1899                    return null;
    1900            }
    1901        }
    1902
    1903        // *********************************************************************
    1904
    1905        //@ requires e != null;
    1906        static boolean checkIntegralType(Expr e) {
    1907            Type t = getType(e);
    1908            if(Types.isIntegralType(t)) {
    1909                return true;
    1910            } else {
    1911                if (!Types.isErrorType(t))
    1912                    ErrorSet.error(e.getStartLoc(),
    1913                                "Cannot convert "+Types.printName(t)
    1914                                +" to an integral type");
    1915                return false;
    1916            }
    1917        }
    1918
    1919        //@ requires e != null;
    1920        static boolean checkNumericType(Expr e) {
    1921            Type t = getType(e);
    1922            if(!Types.isNumericType(t)) {
    1923                if (!Types.isErrorType(t))
    1924                    ErrorSet.error(e.getStartLoc(),
    1925                                "Cannot convert "+Types.printName(t)
    1926                                +" to a numeric type ");
    1927                return false;
    1928            } else {
    1929                return true;
    1930            }
    1931        }
    1932
    1933        //@ requires e != null;
    1934        static boolean isVariable(Expr e) {
    1935            switch(e.getTag()) {
    1936                case TagConstants.ARRAYREFEXPR:
    1937                case TagConstants.VARIABLEACCESS:
    1938                case TagConstants.FIELDACCESS:
    1939                    return true;
    1940
    1941                default:
    1942                    return false;
    1943            }
    1944        }
    1945
    1946        // ======================================================================
    1947
    1948        /**
    1949         * Decorates <code>VarInit</code> nodes to point to <code>Type</code> objects.
    1950         */
    1951        //@ private invariant typeDecoration != null;
    1952        //@ private invariant typeDecoration.decorationType == \type(Type);
    1953        private static ASTDecoration typeDecoration
    1954            = new ASTDecoration("typeDecoration");
    1955
    1956        //@ requires i != null && t != null;
    1957        public static VarInit setType(VarInit i, Type t) {
    1958            if (t instanceof TypeName)
    1959                t = TypeSig.getSig((TypeName)t);
    1960            typeDecoration.set(i, t);
    1961            return i;
    1962        }
    1963
    1964        /**
    1965         * Retrieves the <code>Type</code> of a <code>VarInit</code>.  This type is
    1966         * associated with an expression by the typechecking pass. If the expression does
    1967         * not have an associated type, then null is returned.
    1968         */
    1969        //@ requires i != null;
    1970        protected static Type getTypeOrNull(VarInit i) {
    1971            return (Type)typeDecoration.get(i);
    1972        }
    1973
    1974        /**
    1975         * Retrieves the <code>Type</code> of a <code>VarInit</code>.  This type is
    1976         * associated with an expression by the typechecking pass. If the expression does
    1977         * not have an associated type, then <code>Assert.fail</code> is called.
    1978         */
    1979        //@ requires i != null;
    1980        //@ ensures \result != null;
    1981        public static Type getType(VarInit i) {
    1982            Type t = getTypeOrNull(i);
    1983            if(t==null)
    1984                Assert.fail("getType at "+i.getTag()+" "+
    1985                            PrettyPrint.inst.toString(i) +
    1986                            Location.toString(i.getStartLoc()));
    1987            return t;
    1988        }
    1989
    1990
    1991        // ======================================================================
    1992
    1993        /**
    1994         * Decorates <code>BranchStmt</code> nodes to point to labelled <code>Stmt</code>
    1995         * objects.
    1996         */
    1997        //@ private invariant branchDecoration != null;
    1998        //@ private invariant branchDecoration.decorationType == \type(Stmt);
    1999        private static ASTDecoration branchDecoration
    2000            = new ASTDecoration("branchDecoration");
    2001
    2002        //@ requires s != null && l != null;
    2003        private static void setBranchLabel(BranchStmt s, Stmt l) {
    2004            Assert.notFalse(branchDecoration.get(s) == null);       //@ nowarn Pre;
    2005            branchDecoration.set(s,l);
    2006        }
    2007
    2008        /**
    2009         * Retrieves the <code>Stmt</code> target of a <code>BranchStmt</code>.  This
    2010         * <code>Stmt</code> may be mentioned either explicitly (as in <code>break
    2011         * label;</code>), or implicitly (as in <code>break;</code>) by the
    2012         * <code>BranchStmt</code>.  The correct <code>Stmt</code> target is associated
    2013         * with the <code>BranchStmt</code> by the typechecking pass. This type is
    2014         * associated with an expression by the typechecking pass. If the
    2015         * <code>BranchStmt</code> does not have an associated <code>Stmt</code> target,
    2016         * then <code>Assert.fail</code> is called.
    2017         */
    2018        //@ requires s != null;
    2019        static Stmt getBranchLabel(BranchStmt s) {
    2020            Stmt l = (Stmt)branchDecoration.get(s);
    2021            if(l==null)
    2022                Assert.fail("getBranchLabel failed at "+s.getTag());
    2023            return l;
    2024        }
    2025
    2026        // ======================================================================
    2027
    2028        //@ requires expr != null && t != null;
    2029        static void checkType(Expr expr, Type t) {
    2030            if(!inst.assignmentConvertable(expr, t)) {
    2031                if (!Types.isErrorType(getType(expr)))
    2032                    ErrorSet.error(expr.getStartLoc(),
    2033                                "Cannot convert "+Types.printName(getType(expr))
    2034                                +" to "+Types.printName(t));
    2035            }
    2036
    2037        }
    2038
    2039        //@ requires e != null && s != null && t != null;
    2040        //@ requires loc != Location.NULL;
    2041        protected static void reportLookupException(LookupException e,
    2042                                                    String s,
    2043                                                    String t,
    2044                                                    int loc) {
    2045            switch(e.reason) {
    2046                case LookupException.NOTFOUND:
    2047                    ErrorSet.error(loc, "No such "+s+" in type "+t);
    2048                    break;
    2049                case LookupException.AMBIGUOUS:
    2050                    ErrorSet.error(loc, "Ambiguous "+s+" for type "+t);
    2051                    break;
    2052                case LookupException.BADTYPECOMBO:
    2053                    ErrorSet.error(loc, "No "+s+" matching given argument types");
    2054                    break;
    2055                case LookupException.NOTACCESSIBLE:
    2056                    ErrorSet.error(loc, "Cannot access this "+s);
    2057                    break;
    2058                default:
    2059                    Assert.fail("Bad lookup exception: "+e.reason);
    2060            }
    2061        }
    2062
    2063        /**
    2064         * Checks if Exp e can be assigned to Type t.  This method is here instead of in
    2065         * {@link javafe.tc.Types}, because it needs to mess with constants.
    2066         */
    2067        //@ requires e != null && t != null;
    2068        protected boolean assignmentConvertable(Expr e, Type t) {
    2069
    2070            Type te = getType(e);
    2071
    2072            if(Types.isInvocationConvertable(te, t))
    2073                return true;
    2074
    2075            // Check if t is byte/short/char,
    2076            // and e a constant expression whose value fits in t.
    2077
    2078            switch(t.getTag()) {
    2079                case TagConstants.BYTETYPE:
    2080                case TagConstants.SHORTTYPE:
    2081                case TagConstants.CHARTYPE:
    2082                    Object val = ConstantExpr.eval(e);
    2083                    if(val != null &&
    2084                       ConstantExpr.constantValueFitsIn(val, (PrimitiveType)t))
    2085                        return true;
    2086                    else return false;
    2087                default:
    2088                    return false;
    2089            }
    2090        }
    2091
    2092        // ======================================================================
    2093
    2094        //@ requires e != null;
    2095        protected void checkTypeDeclElemPragma(TypeDeclElemPragma e) {
    2096            Assert.fail("Unexpected TypeDeclElemPragma");
    2097        }
    2098
    2099        /**
    2100         * Hook to do additional processing on <code>ModifierVec</code>s.  The
    2101         * <code>ASTNode</code> is the parent of the <code>ModifierPragma</code>, and
    2102         * <code>env</code> is the current environment.
    2103         */
    2104        //@ requires env != null;
    2105        protected Env checkModifierPragmaVec(ModifierPragmaVec v,
    2106                                             ASTNode ctxt,
    2107                                             Env env) {
    2108            if (v != null)
    2109              for(int i = 0; i < v.size(); i++) {
    2110                env = checkModifierPragma(v.elementAt(i), ctxt, env);
    2111                  }
    2112              return env;
    2113        }
    2114
    2115        /**
    2116         * Hook to do additional processing on <code>Modifier</code>s.  The
    2117         * <code>ASTNode</code> is the parent of the <code>ModifierPragma</code>, and
    2118         * <code>env</code> is the current environment.
    2119         * @return true if pragma should be deleted
    2120         */
    2121        //@ requires p != null && env != null;
    2122        protected Env checkModifierPragma(ModifierPragma p, ASTNode ctxt, Env env) {
    2123            // Assert.fail("Unexpected ModifierPragma");
    2124            return env;
    2125        }
    2126
    2127        //@ requires e != null && s != null;
    2128        protected Env checkStmtPragma(Env e, StmtPragma s) {
    2129            Assert.fail("Unexpected StmtPragma");
    2130            return e;
    2131        }
    2132
    2133        //@ requires env != null;
    2134        protected Env checkTypeModifierPragmaVec(TypeModifierPragmaVec v,
    2135                                                  ASTNode ctxt,
    2136                                                  Env env) {
    2137            if(v != null)
    2138                for(int i=0; i<v.size(); i++)
    2139                    env = checkTypeModifierPragma(v.elementAt(i), ctxt, env);
    2140            return env;
    2141        }
    2142
    2143        //@ requires p != null && env != null;
    2144        protected Env checkTypeModifierPragma(TypeModifierPragma p,
    2145                                               ASTNode ctxt,
    2146                                               Env env) {
    2147            Assert.fail("Unexpected TypeModifierPragma");
    2148            return env;
    2149        }
    2150
    2151        /**
    2152         * This may be called more than once on a Type t.
    2153         */
    2154        //@ requires t != null;
    2155        protected Env checkTypeModifiers(Env env, Type t) {
    2156            // don't know context for type, so pull it out of the type's decorations.
    2157            if (env == null) {
    2158                env = (Env)Env.typeEnv.get(t);
    2159            }
    2160            Assert.notFalse(env != null);  //@ nowarn Pre;
    2161            checkTypeModifierPragmaVec(t.tmodifiers, t, env);
    2162            if (t instanceof ArrayType) {
    2163                env = checkTypeModifiers(env, ((ArrayType)t).elemType);
    2164            }
    2165            return env;
    2166        }
    2167
    2168    }
    2169
    2170    /*
    2171     * Local Variables:
    2172     * Mode: Java
    2173     * fill-column: 85
    2174     * End:
    2175     */