    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.tc;
    004
    005    import java.util.Enumeration;
    006
    007    import javafe.ast.*;
    008
    009    import javafe.tc.Env;
    010    import javafe.tc.EnvForLocals;
    011    import javafe.tc.EnvForTypeSig;
    012    import javafe.tc.LookupException;
    013    import javafe.tc.TypeSig;
    014
    015    import javafe.util.*;
    016
    017    import escjava.ast.*;
    018    import escjava.ast.Modifiers;
    019    import escjava.ast.TagConstants;
    020    import escjava.tc.Types;
    021    import escjava.Main;
    022
    023    public class FlowInsensitiveChecks extends javafe.tc.FlowInsensitiveChecks
    024    {
    025      static {
    026        inst = new FlowInsensitiveChecks();
    027      }
    028      static public javafe.tc.FlowInsensitiveChecks inst() { return inst; }
    029
    030      // Setup for ghost variables
    031
    032      /**
    033       * Are we in the middle of processing an annotation? (Used by {@link GhostEnv}.)
    034       */
    035      public static boolean inAnnotation = false;
    036      public static boolean inModelBody = false;
    037      // FIXME - the above two variables are a hack!  Note that below we have to save and
    038      // restore their values so that the appropriate values are read out of these
    039      // global-static variables by GhostEnv.  It would be much better to create a sub
    040      // Env that understands what to do and pass that along for the checks. -- DRCok
    041
    042      public escjava.AnnotationHandler annotationHandler =
    043        new escjava.AnnotationHandler();
    044      /**
    045       * Indicates whether <code>LS</code> is allowed in this context.  The default is
    046       * <code>true</code>.  For contexts where <code>LS</code> is not allowed,
    047       * <code>isLocksetContext</code> should be set <code>false</code> only temporarily.
    048       */
    049      protected boolean isLocksetContext = true;
    050
    051      /**
    052       * <code>\result</code> is allowed in this context when <code>isRESContext</code>
    053       * is <code>true</code> and <code>returnType != null</code>.  The default value
    054       * of <code>isRESContext</code> is <code>false</code>.  For contexts where
    055       * <code>isRESContext</code> should be <code>true</code>,
    056       * <code>isRESContext</code> should be set to <code>true</code> only temporarily.
    057       */
    058      protected boolean isRESContext = false;
    059
    060      /**
    061       * Indicates whether <code>\old</code> and <code>\fresh</code> are allowed in
    062       * this context.  The default is <code>false</code>.  For contexts where these
    063       * functions are allowed, <code>isTwoStateContext</code> should be set
    064       * <code>true</code> only temporarily.
    065       */
    066      protected boolean isTwoStateContext = false;
    067
    068      /**
    069       * Indicates whether checking is currently being done inside a <code>PRE</code>.
    070       * This is used by the code that disallows nested <code>PRE</code> expressions.
    071       * Note: alternatively, one could use <code>isTwoStateContext</code> to implement
    072       * this functionality, but by having a separate bit, a more precise error message
    073       * can be produced.
    074       */
    075      protected boolean isInsidePRE = false;
    076
    077      /**
    078       * Indicates whether a quantification or labeled predicate is allowed in this
    079       * context.  This boolean is used only between one call of <code>checkExpr</code>
    080       * to a following recursive call.
    081       */
    082      protected boolean isPredicateContext = false;
    083
    084      /**
    085       * Indicates whether private field accesses are allowed in the current context.
    086       * Private field accesses are allowed everywhere, except in postconditions of
    087       * overridable methods.
    088       */
    089      protected boolean isPrivateFieldAccessAllowed = true;
    090
    091      protected int accessibilityLowerBound = ACC_LOW_BOUND_Private;
    092      // Note, "ACC_LOW_BOUND_Private" would be the same as "no lower bound"
    093      protected static final int ACC_LOW_BOUND_Private = 0;
    094      protected static final int ACC_LOW_BOUND_Package = 1;
    095      protected static final int ACC_LOW_BOUND_Protected = 2;
    096      protected static final int ACC_LOW_BOUND_Public = 3;
    097
    098      /**
    099       * If <code>accessibilityLowerBound != ACC_LOW_BOUND_Private</code>, then
    100       * <code>accessibilityContext</code> is the field or routine whose modifier
    101       * pragma is being type checked.
    102       */
    103      /*@ invariant accessibilityContext == null ||
    104        @           accessibilityContext instanceof FieldDecl ||
    105        @           accessibilityContext instanceof RoutineDecl;
    106      */
    107      //@ readable accessibilityContext if accessibilityLowerBound != ACC_LOW_BOUND_Private;
    108      protected ASTNode accessibilityContext;
    109
    110      /**
    111       * Acts as a parameter to <code>checkExpr</code>.  Its value is meaningful only
    112       * on entry to <code>checkExpr</code>.  It indicates whether the expression to be
    113       * checked is in a specification designator context.  In particular, this
    114       * parameter is used to disallow array index wild cards in non-spec designator
    115       * contexts.
    116       */
    117      protected boolean isSpecDesignatorContext = false;
    118
    119      /**
    120       * Contains the loop invariant statement pragmas seen so far and not yet
    121       * processed.
    122       */
    123      protected ExprStmtPragmaVec loopInvariants = ExprStmtPragmaVec.make();
    124
    125      /**
    126       * Contains the loop decreases statement pragmas seen so far and not yet
    127       * processed.
    128       */
    129      protected ExprStmtPragmaVec loopDecreases = ExprStmtPragmaVec.make();
    130
    131      protected ExprStmtPragmaVec loopPredicates = ExprStmtPragmaVec.make();
    132
    133      protected LocalVarDeclVec skolemConstants = LocalVarDeclVec.make();
    134
    135      /**
    136       * Indicates whether we are are checking an invariant pragma.
    137       */
    138      protected boolean invariantContext = false;
    139
    140      /**
    141       * Counts the number of accesses of free variables and fields used for checking
    142       * the appropriateness of invariants.
    143       */
    144      //@ readable countFreeVarsAccesses if invariantContext;
    145      protected int countFreeVarsAccesses = 0 ;
    146
    147      /**
    148       * Override so that we use {@link GhostEnv} instead of {@link EnvForTypeSig}.
    149       */
    150      protected EnvForTypeSig makeEnvForTypeSig(TypeSig s,
    151                                                boolean staticContext) {
    152        return new GhostEnv(s.getEnclosingEnv(), s, staticContext);
    153      }
    154
    155      public static ASTDecoration envDecoration =
    156        new ASTDecoration("env");
    157      public static ASTDecoration staticenvDecoration =
    158        new ASTDecoration("staticenv");
    159
    160      public void checkTypeDeclaration(/*@ non_null */ TypeSig s) {
    161        super.checkTypeDeclaration(s);
    162        TypeDecl td = s.getTypeDecl();
    163        envDecoration.set(td,rootIEnv);
    164        staticenvDecoration.set(td,rootSEnv);
    165      }
    166
    167      // Extensions to type declaration member checkers.
    168
    169      protected void checkTypeDeclElem(TypeDeclElem e) {
    170        boolean savedInAnnotation = inAnnotation;
    171        boolean savedInModelBody = inModelBody;
    172        // FIXME - should this use Utils.isModel ???
    173        if (e instanceof ConstructorDecl &&
    174            null != Utils.findModifierPragma(((ConstructorDecl)e).pmodifiers,TagConstants.MODEL)) {
    175          inAnnotation = true;
    176          inModelBody = true;
    177        }
    178        if (e instanceof MethodDecl &&
    179            null != Utils.findModifierPragma(((MethodDecl)e).pmodifiers,TagConstants.MODEL)) {
    180          inAnnotation = true;
    181          inModelBody = true;
    182        }
    183        try {
    184          super.checkTypeDeclElem(e);
    185          if (e instanceof RoutineDecl) {
    186            // Desugaring presumes that typechecking has already
    187            // been performed
    188            RoutineDecl m = (RoutineDecl)e;
    189    /*
    190            if ((m instanceof ConstructorDecl) && m.implicit) {
    191              // The desugaring of m can require the desugared
    192              // specs of a parent constructor, so we have to be
    193              // sure that the parent constructor is typechecked.
    194              TypeSig s = TypeSig.getSig(m.parent).superClass();
    195              if (s != null) checkTypeDeclElem(s.getTypeDecl());
    196            }
    197    */
    198    /*
    199            if (m.originalRaises != null &&
    200                m.originalRaises.size() != m.raises.size()) {
    201
    202                for (int i=m.originalRaises.size()+1; i < m.raises.size(); ++i) {
    203
    204                  TypeSig t = TypeSig.getSig(m.raises.elementAt(i));
    205    System.out.println("FOUND " + t);
    206                  if (!t.isSubtypeOf(Types.javaLangRuntimeException())) {
    207                     ErrorSet.error(m.raises.elementAt(i).getStartLoc(),
    208                       "The type " + t + " is not a subtype of " +
    209                       "RuntimeException and is not declared by the API, and " +
    210                       "consequently may not be declared in a specification.");
    211                     System.out.println("BAD");
    212                  }
    213                }
    214            }
    215    */
    216            annotationHandler.desugar(m);
    217          }
    218        } finally {
    219          inAnnotation = savedInAnnotation;
    220          inModelBody = savedInModelBody;
    221        }
    222
    223        // Do a separate set of checks - purity checking
    224        // FIXME - perhaps these should be moved into this routine
    225        annotationHandler.process(e);
    226
    227        if (e.getTag() == TagConstants.INITBLOCK) {
    228          InitBlock ib = (InitBlock)e;
    229          if (ib.pmodifiers != null) {
    230            checkModifierPragmaVec(ib.pmodifiers,ib,
    231                                   Modifiers.isStatic(ib.modifiers) ? rootSEnv : rootIEnv);
    232            /*
    233              for (int i = 0; i < ib.pmodifiers.size(); i++) {
    234              ModifierPragma mp = (ModifierPragma)ib.pmodifiers.elementAt(i);
    235              ErrorSet.error(mp.getStartLoc(),
    236              TagConstants.toString(mp.getTag()) +
    237              " pragma cannot be applied to initializer block");
    238              }
    239            */
    240          }
    241        }
    242
    243      }
    244
    245      // Extensions to Expr and Stmt checkers.
    246
    247      protected Env checkStmt(Env env, Stmt s) {
    248        boolean savedTwoStateContext = isTwoStateContext;
    249        isTwoStateContext = true;
    250        try {
    251          int tag = s.getTag();
    252
    253          // Check for any loop invariants, loop bounds, loop predicates, or skolem
    254          // constants in the wrong place
    255          if (loopInvariants.size() != 0 ||
    256              loopDecreases.size() != 0 ||
    257              loopPredicates.size() != 0 ||
    258              skolemConstants.size() != 0) {
    259            switch (tag) {
    260            case TagConstants.DOSTMT:
    261            case TagConstants.WHILESTMT:
    262            case TagConstants.FORSTMT:
    263            case TagConstants.LABELSTMT:
    264            case TagConstants.LOOP_INVARIANT:
    265            case TagConstants.MAINTAINING:
    266            case TagConstants.DECREASES:
    267            case TagConstants.DECREASING:
    268            case TagConstants.LOOP_PREDICATE:
    269            case TagConstants.SKOLEMCONSTANTPRAGMA:
    270              break;
    271            default:
    272              checkLoopInvariants(env, false);
    273              checkLoopDecreases(env, false);
    274              checkLoopPredicates(env, false);
    275              checkSkolemConstants(env, false);
    276              break;
    277            }
    278          }
    279
    280          switch(tag) {
    281          case TagConstants.DOSTMT:
    282          case TagConstants.WHILESTMT: {
    283            checkLoopInvariants(env, true);
    284            checkLoopDecreases(env, true);
    285            Env newEnv = checkSkolemConstants(env, true);
    286            checkLoopPredicates(newEnv, true);
    287            super.checkStmt(env, s);
    288            break;
    289          }
    290          case TagConstants.FORSTMT: {
    291            ForStmt f = (ForStmt)s;
    292
    293            ExprStmtPragmaVec invs = loopInvariants;
    294            ExprStmtPragmaVec decrs = loopDecreases;
    295            ExprStmtPragmaVec preds = loopPredicates;
    296            LocalVarDeclVec skolemConsts = skolemConstants;
    297
    298            loopInvariants = ExprStmtPragmaVec.make();
    299            loopDecreases = ExprStmtPragmaVec.make();
    300            loopPredicates = ExprStmtPragmaVec.make();
    301            skolemConstants = LocalVarDeclVec.make();
    302
    303            Env se = checkStmtVec(env, f.forInit);
    304
    305            Assert.notFalse(loopInvariants.size() == 0);
    306            Assert.notFalse(loopDecreases.size() == 0);
    307            Assert.notFalse(loopPredicates.size() == 0);
    308            Assert.notFalse(skolemConstants.size() == 0);
    309
    310            loopInvariants = invs;
    311            loopDecreases = decrs;
    312            loopPredicates = preds;
    313            skolemConstants = skolemConsts;
    314
    315            checkLoopInvariants(se, true);
    316            checkLoopDecreases(se, true);
    317            Env newEnv = checkSkolemConstants(se, true);
    318            checkLoopPredicates(newEnv, true);
    319            checkForLoopAfterInit(se, f);
    320            break;
    321          }
    322          case TagConstants.BLOCKSTMT: {
    323            env = super.checkStmt(env, s);
    324            // Check for any loop_invariant statement pragmas at the end of the
    325            // body.
    326            checkLoopInvariants(env, false);
    327            checkLoopDecreases(env, false);
    328            checkLoopPredicates(env, false);
    329            checkSkolemConstants(env, false);
    330            break;
    331          }
    332          case TagConstants.VARDECLSTMT: {
    333            VarDeclStmt vs = (VarDeclStmt)s;
    334            LocalVarDecl x = vs.decl;
    335            if (Utils.findModifierPragma(x.pmodifiers,
    336                                         TagConstants.GHOST) != null) {
    337              boolean savedInAnnotation = inAnnotation;
    338              inAnnotation = true;
    339              try {
    340                env.resolveType(sig, x.type);
    341                checkTypeModifiers(env, x.type);
    342                javafe.tc.PrepTypeDeclaration.inst.
    343                  checkModifiers(x.modifiers, Modifiers.ACC_FINAL,
    344                                 x.locId, "local ghost variable");
    345                checkModifierPragmaVec(x.pmodifiers, x, env);
    346
    347                Env newEnv = new EnvForGhostLocals(env,x);
    348                if (x.init != null)
    349                  x.init = checkInit(newEnv, x.init, x.type);
    350                env = newEnv;
    351              } finally {
    352                inAnnotation = savedInAnnotation;
    353              }
    354              break;
    355            }
    356
    357            env = super.checkStmt(env, s);
    358            break;
    359
    360          }
    361          case TagConstants.CLASSDECLSTMT: {
    362            ClassDeclStmt cds = (ClassDeclStmt)s;
    363            ClassDecl cd = cds.decl;
    364            (new escjava.AnnotationHandler.NestedPragmaParser()).parseAllRoutineSpecs(cd);
    365            env = super.checkStmt(env, s);
    366            annotationHandler.desugar(cd);
    367            break;
    368          }
    369          default:
    370            env = super.checkStmt(env, s);
    371            break;
    372          }
    373
    374        } finally {
    375          isTwoStateContext = savedTwoStateContext;
    376        }
    377        return env;
    378      }
    379
    380      protected void checkLoopInvariants(Env env, boolean allowed) {
    381        for (int i = 0; i < loopInvariants.size(); i++) {
    382          ExprStmtPragma s = loopInvariants.elementAt(i);
    383          Assert.notFalse(s.getTag() == TagConstants.LOOP_INVARIANT
    384                          || s.getTag() == TagConstants.MAINTAINING);
    385          if (allowed) {
    386            //Assert.notFalse(!isTwoStateContext);
    387            Assert.notFalse(!inAnnotation || inModelBody);
    388            boolean savedInAnnotation = inAnnotation;
    389            inAnnotation = true;
    390            //isTwoStateContext = true;
    391            try {
    392              s.expr = checkPredicate(env, s.expr);
    393            } finally {
    394              inAnnotation = savedInAnnotation;
    395              //isTwoStateContext = false;
    396            }
    397          } else {
    398            errorExpectingLoop(s.getStartLoc(), TagConstants.LOOP_INVARIANT);
    399          }
    400        }
    401        loopInvariants.removeAllElements();
    402      }
    403
    404      protected void checkLoopDecreases(Env env, boolean allowed) {
    405        for (int i = 0; i < loopDecreases.size(); i++) {
    406          ExprStmtPragma s = loopDecreases.elementAt(i);
    407          Assert.notFalse(s.getTag() == TagConstants.DECREASES
    408                          || s.getTag() == TagConstants.DECREASING);
    409          if (allowed) {
    410            //Assert.notFalse(!isTwoStateContext);
    411            Assert.notFalse(!inAnnotation || inModelBody);
    412            boolean savedInAnnotation = inAnnotation;
    413            inAnnotation = true;
    414            try {
    415              s.expr = checkExpr(env, s.expr, Types.bigintType);
    416            } finally {
    417              inAnnotation = savedInAnnotation;
    418            }
    419          } else {
    420            errorExpectingLoop(s.getStartLoc(), TagConstants.DECREASES);
    421          }
    422        }
    423        loopDecreases.removeAllElements();
    424      }
    425
    426      protected void checkLoopPredicates(Env env, boolean allowed) {
    427        for (int i = 0; i < loopPredicates.size(); i++) {
    428          ExprStmtPragma s = loopPredicates.elementAt(i);
    429          Assert.notFalse(s.getTag() == TagConstants.LOOP_PREDICATE);
    430          if (allowed) {
    431            //Assert.notFalse(!isTwoStateContext);
    432            Assert.notFalse(!inAnnotation || inModelBody);
    433            boolean savedInAnnotation = inAnnotation;
    434            inAnnotation = true;
    435            //isTwoStateContext = true;
    436            try {
    437              s.expr = checkPredicate(env, s.expr);
    438            } finally {
    439              inAnnotation = savedInAnnotation;
    440              //isTwoStateContext = false;
    441            }
    442          } else {
    443            errorExpectingLoop(s.getStartLoc(), TagConstants.LOOP_PREDICATE);
    444          }
    445        }
    446        loopPredicates.removeAllElements();
    447      }
    448
    449      protected Env checkSkolemConstants(Env env, boolean allowed) {
    450        for (int i = 0; i < skolemConstants.size(); i++) {
    451          LocalVarDecl s = skolemConstants.elementAt(i);
    452          if (allowed) {
    453            //Assert.notFalse(!isTwoStateContext);
    454            Assert.notFalse(!inAnnotation || inModelBody);
    455            boolean savedInAnnotation = inAnnotation;
    456            inAnnotation = true;
    457            //isTwoStateContext = true;
    458            try {
    459              env.resolveType(sig, s.type);
    460              env = new EnvForLocals(env, s);
    461            } finally {
    462              inAnnotation = savedInAnnotation;
    463              //isTwoStateContext = false;
    464            }
    465          } else {
    466            errorExpectingLoop(s.getStartLoc(), TagConstants.SKOLEM_CONSTANT);
    467          }
    468        }
    469        skolemConstants.removeAllElements();
    470        return env;
    471      }
    472
    473      private void errorExpectingLoop(int loc, int tag) {
    474        ErrorSet.error(loc, "'" + TagConstants.toString(tag) +
    475                       "' pragmas can occur " +
    476                       "only immediately prior to a loop statement.  Loop " +
    477                       "statement expected (and not found) here.");
    478      }
    479
    480      protected Expr checkPredicate(Env env, Expr e) {
    481        boolean savedPredicateContext = isPredicateContext;
    482        isPredicateContext = true;
    483        Expr ee = checkExpr(env, e, Types.booleanType);
    484        isPredicateContext = savedPredicateContext;
    485        return ee;
    486      }
    487
    488      //@ also requires e != null;
    489      protected Expr checkExpr(Env env, Expr e) {
    490        // Anticipate that the next context is probably not one suitable for
    491        // quantifications and labels.  "isPredicateContext" must revert to its old
    492        // value before return.
    493        boolean isCurrentlyPredicateContext = isPredicateContext;
    494        isPredicateContext = false;
    495
    496        try {
    497
    498          if (getTypeOrNull(e) != null )
    499            // already done
    500            return e;
    501
    502          // No recursive call to "checkExpr" is a specification designator context, so
    503          // set "isSpecDesignatorContext" to "false", keeping the initial value in
    504          // local variable "isCurrentlySpecDesignatorContext".
    505          boolean isCurrentlySpecDesignatorContext = isSpecDesignatorContext;
    506          isSpecDesignatorContext = false;
    507
    508          int tag = e.getTag();
    509          switch(tag) {
    510
    511            // Handle accesses to ghost fields as well...
    512          case TagConstants.FIELDACCESS:
    513            {
    514              if (!inAnnotation)
    515                return super.checkExpr(env, e);
    516
    517              // a field access is considerded a free variable access in an
    518              // invariant.
    519              if (invariantContext) countFreeVarsAccesses++;
    520
    521              // set default result type to errorType, in case there is an error.
    522              setType( e, Types.errorType );
    523              FieldAccess fa = (FieldAccess)e;
    524              Type t = checkObjectDesignator(env, fa.od);
    525              if (t==null)
    526                return fa;
    527              if (t instanceof TypeName)
    528                t = TypeSig.getSig( (TypeName) t );
    529
    530              if (Types.isErrorType(t)) {
    531                setType( fa, Types.errorType );
    532                return fa;
    533              }
    534
    535              try {
    536                fa.decl = escjava.tc.Types.lookupField( t, fa.id, sig );
    537              } catch( LookupException ex) {
    538                if (!Types.isErrorType(t))
    539                  reportLookupException(ex, "field",
    540                                        Types.printName(t), fa.locId);
    541                setType( fa, Types.errorType );
    542                return fa;
    543              }
    544              setType( fa, fa.decl.type );
    545
    546              if (fa.od instanceof TypeObjectDesignator &&
    547                  !GhostEnv.isStatic(fa.decl)) {
    548                // Is fa.decl an instance field of the same class as fa is
    549                // part of?
    550                boolean thisField = false;
    551                if (fa.decl.parent != null)
    552                  thisField = (env.getEnclosingClass()
    553                               .isSubtypeOf(TypeSig.getSig(fa.decl.parent)));
    554
    555                if (thisField ||
    556                    ((TypeObjectDesignator)fa.od).type instanceof TypeName) {
    557
    558                  ErrorSet.error(fa.locId,
    559                                 "An instance field may be accessed only via "
    560                                 + "an object and/or from a non-static"
    561                                 + " context or an inner class enclosed"
    562                                 + " by a type possessing that field.");
    563
    564                } else
    565                  ErrorSet.error(fa.locId,
    566                                 "The instance fields of type "
    567                                 + ((TypeObjectDesignator)fa.od).type
    568                                 + " may not be accessed from type "
    569                                 + sig );
    570              }
    571
    572              /* FIXME -- need to clean up testing of access modifiers and to make them
    573                 consistent with JML
    574                 if (!isPrivateFieldAccessAllowed &&
    575                 Modifiers.isPrivate(fa.decl.modifiers) &&
    576                 Utils.findModifierPragma(fa.decl,
    577                 TagConstants.SPEC_PUBLIC) == null &&
    578                 Utils.findModifierPragma(fa.decl,
    579                 TagConstants.SPEC_PROTECTED) == null) {
    580                 ErrorSet.error(fa.locId,
    581                 "A private field can be used in "+
    582                 "postconditions of overridable methods only if "+
    583                 "it is declared spec_public or spec_protected");
    584                 }
    585              */
    586
    587              // The following code checks that "fa" is at least as
    588              // spec-accessible as "accessibilityContext" is Java-accessible.
    589              // This is vacuously true if "accessibilityLowerBound" is
    590              // private.
    591              if (accessibilityLowerBound != ACC_LOW_BOUND_Private) {
    592                boolean isAccessibleEnough;
    593                if (Modifiers.isPublic(fa.decl.modifiers) ||
    594                    Utils.findModifierPragma(fa.decl,
    595                                             TagConstants.SPEC_PUBLIC) != null) {
    596                  // public and spec_public fields are always accessible
    597                  isAccessibleEnough = true;
    598                } else if (Utils.findModifierPragma(fa.decl,
    599                                                    TagConstants.SPEC_PROTECTED) != null) {
    600
    601                  // Copied from the protected case down below.
    602                  isAccessibleEnough = false;
    603                  if (accessibilityLowerBound == ACC_LOW_BOUND_Package) {
    604                    isAccessibleEnough = true;
    605                  } else if (accessibilityLowerBound == ACC_LOW_BOUND_Protected) {
    606                    TypeDecl tdContext;
    607                    if (accessibilityContext instanceof FieldDecl) {
    608                      tdContext = ((FieldDecl)accessibilityContext).parent;
    609                    } else {
    610                      tdContext = ((RoutineDecl)accessibilityContext).parent;
    611                    }
    612                    TypeSig tsContext = TypeSig.getSig(tdContext);
    613                    if (tsContext.isSubtypeOf(TypeSig.getSig(fa.decl.parent))) {
    614                      isAccessibleEnough = true;
    615                    }
    616                  }
    617
    618                } else if (Modifiers.isPrivate(fa.decl.modifiers)) {
    619                  // Note: if "fa" type-checked so far, then "fa.decl" and
    620                  // "accessibilityContext" are declared in the same class.
    621                  // It would be nice to assert this fact at run-time, but
    622                  // control may reach this point even if "fa" does not
    623                  // type-check above.
    624
    625                  // "fa.decl" can be private only if
    626                  // "accessibilityContext" is private, which was checked
    627                  // above
    628                  isAccessibleEnough = false;
    629
    630                } else if (Modifiers.isPackage(fa.decl.modifiers)) {
    631                  // Note: if "fa" type-checked so far, then "fa.decl" and
    632                  // "accessibilityContext" are declared in the same
    633                  // package.  It would be nice to assert this fact at
    634                  // run-time, but control may reach this point even if
    635                  // "fa" does not type-check above.
    636
    637                  // "fa.decl" can be package (default) accessible only if
    638                  // "accessibilityContext" is private (which was checked
    639                  // above) or package
    640                  isAccessibleEnough =
    641                    (accessibilityLowerBound == ACC_LOW_BOUND_Package);
    642
    643                } else {
    644                  Assert.notFalse(Modifiers.isProtected(fa.decl.modifiers));
    645                  // Note: if "fa" type-checked so far, then either
    646                  // "fa.decl" and "accessibilityContext" are declared in
    647                  // the same package or the class declaring
    648                  // "accessibilityContext" is a subtype of the class
    649                  // declaring "fa.decl".  It would be nice to assert this
    650                  // fact at run-time, but control may reach this point
    651                  // even if "fa" does not type-check above.
    652
    653                  // "fa.decl" can be protected only if
    654                  // "accessibilityContext" is private (which was checked
    655                  // above) or package, or if "accessibilityContext" is
    656                  // protected and "fa.decl" is declared in a superclass of
    657                  // the class that declares "accessibilityContext".
    658                  isAccessibleEnough = false;
    659                  if (accessibilityLowerBound == ACC_LOW_BOUND_Package) {
    660                    isAccessibleEnough = true;
    661                  } else if (accessibilityLowerBound == ACC_LOW_BOUND_Protected) {
    662                    TypeDecl tdContext;
    663                    if (accessibilityContext instanceof FieldDecl) {
    664                      tdContext = ((FieldDecl)accessibilityContext).parent;
    665                    } else {
    666                      tdContext = ((RoutineDecl)accessibilityContext).parent;
    667                    }
    668                    TypeSig tsContext = TypeSig.getSig(tdContext);
    669                    if (tsContext.isSubtypeOf(TypeSig.getSig(fa.decl.parent))) {
    670                      isAccessibleEnough = true;
    671                    }
    672                  }
    673                }
    674                /* Need to fix the accessibility checking to conform with JML - FIXME
    675                   if (!isAccessibleEnough) {
    676                   ErrorSet.error(fa.locId, "Fields mentioned in this modifier "+
    677                   "pragma must be at least as accessible "+
    678                   "as the field/method being modified (perhaps "+
    679                   "try spec_public)");
    680                   }
    681                */
    682              }
    683
    684              return fa;
    685            }
    686
    687          case TagConstants.METHODINVOCATION:
    688            {
    689              countFreeVarsAccesses++;
    690              MethodInvocation mi = (MethodInvocation)e;
    691              Type t = checkObjectDesignator(env, mi.od);
    692              if (mi.od instanceof ExprObjectDesignator && Types.objectsetType == t) {
    693    // FIXME - all reach expressions are true for now
    694                Expr ee = LiteralExpr.make(TagConstants.BOOLEANLIT,Boolean.TRUE,
    695                                              Location.NULL);
    696                setType(ee, Types.booleanType);
    697                return ee;
    698              } else {
    699                Expr ee = super.checkExpr(env,e);
    700                return ee;
    701              }
    702            }
    703
    704          case TagConstants.IMPLIES:
    705          case TagConstants.EXPLIES:
    706          case TagConstants.IFF:
    707          case TagConstants.NIFF:
    708            {
    709              BinaryExpr be = (BinaryExpr)e;
    710              // each argument is allowed to contain quantifiers and labels if
    711              // this expression is
    712              isPredicateContext = isCurrentlyPredicateContext;
    713              be.left = checkExpr(env, be.left, Types.booleanType);
    714              isPredicateContext = isCurrentlyPredicateContext;
    715              be.right = checkExpr(env, be.right, Types.booleanType);
    716
    717              // check illegal associativity of ==> and <==
    718              if ((tag == TagConstants.IMPLIES &&
    719                   (be.left.getTag() == TagConstants.EXPLIES ||
    720                    be.right.getTag() == TagConstants.EXPLIES)) ||
    721                  (tag == TagConstants.EXPLIES &&
    722                   (be.left.getTag() == TagConstants.IMPLIES ||
    723                    be.right.getTag() == TagConstants.IMPLIES))) {
    724                // unfortunately, we don't have the location of either of the
    725                // operators at fault
    726                ErrorSet.error(be.getStartLoc(),
    727                               "Ambiguous association of ==> and <==.  " +
    728                               "Use parentheses to disambiguate.");
    729              }
    730
    731              setType(e, Types.booleanType);
    732              return e;
    733            }
    734
    735          case TagConstants.DOTDOT:
    736            {
    737              BinaryExpr be = (BinaryExpr)e;
    738              // each argument is allowed to contain quantifiers and labels if
    739              // this expression is
    740              isPredicateContext = false;
    741              be.left = checkExpr(env, be.left, Types.intType);
    742              be.right = checkExpr(env, be.right, Types.intType);
    743
    744              // FIXME - this really needs to be a range type
    745              setType(e, Types.intType);
    746              return e;
    747            }
    748
    749          case TagConstants.SUBTYPE:
    750            {
    751              BinaryExpr be = (BinaryExpr)e;
    752              Type expected = Types.booleanType;
    753              if (tag == TagConstants.SUBTYPE)
    754                expected = Types.typecodeType;
    755              be.left = checkExpr(env, be.left, expected);
    756              be.right = checkExpr(env, be.right, expected);
    757              setType(e, Types.booleanType);
    758              return e;
    759            }
    760
    761          case TagConstants.REACH: {
    762            // FIXME - just enough to get by for now
    763            NaryExpr ne = (NaryExpr)e;
    764            Expr nu =
    765              checkExpr(env, ne.exprs.elementAt(0));
    766            ne.exprs.setElementAt(nu, 0);
    767            if (ne.exprs.size() != 1) {
    768              ErrorSet.error(ne.sloc,
    769                   "A \\reach expression expects just one argument");
    770              setType(e, Types.errorType);
    771            } else if (!Types.isReferenceOrNullType(getType(nu))) {
    772              ErrorSet.error(nu.getStartLoc(),
    773                   "A \\reach expression expects an Object argument");
    774            } else {
    775              setType(e, Types.objectsetType);
    776            }
    777            return e;
    778          }
    779
    780          case TagConstants.FRESH:
    781            {
    782              NaryExpr ne = (NaryExpr)e;
    783              if (ne.exprs.size() == 0) {
    784                ErrorSet.error(ne.sloc,
    785                           "The function fresh must have at least one argument");
    786              } else if (!isTwoStateContext) {
    787                ErrorSet.error(ne.sloc,
    788                           "The function \\fresh cannot be used in this context");
    789              } else if (isInsidePRE) {
    790                ErrorSet.error(ne.sloc, "The function \\fresh cannot be used "+
    791                               "inside a \\old expression");
    792              } else {
    793                for (int i = 0; i<ne.exprs.size(); ++i) {
    794                  Expr nu =
    795                    checkExpr(env, ne.exprs.elementAt(i), Types.javaLangObject());
    796                  ne.exprs.setElementAt(nu, i);
    797                }
    798              }
    799              setType(e, Types.booleanType);
    800              return e;
    801            }
    802
    803          case TagConstants.ELEMSNONNULL:
    804            {
    805              NaryExpr ne = (NaryExpr)e;
    806              if (ne.exprs.size() != 1)
    807                ErrorSet.error(ne.sloc,
    808                               "The function \\nonnullelements takes only one argument");
    809              else {
    810                Expr nu = checkExpr(env, ne.exprs.elementAt(0),
    811                                    ArrayType.make(Types.javaLangObject(),
    812                                                   Location.NULL));
    813                ne.exprs.setElementAt(nu, 0);
    814              }
    815              setType(e, Types.booleanType);
    816              return e;
    817            }
    818
    819          case TagConstants.DTTFSA:
    820            {
    821              NaryExpr ne = (NaryExpr)e;
    822              Type resultType = Types.voidType;
    823              if (ne.exprs.size() < 2) {
    824                Assert.notFalse(1 <= ne.exprs.size());
    825                ErrorSet.error(ne.sloc,
    826                               "The function \\dttfsa requires at least two arguments");
    827              } else {
    828                // type check each of the arguments
    829                for (int i = 0; i < ne.exprs.size(); i++) {
    830                  Expr nu = checkExpr(env, ne.exprs.elementAt(i));
    831                  ne.exprs.setElementAt(nu, i);
    832                }
    833                // the first argument should be a TypeExpr; retrieve the type
    834                // it denotes
    835                resultType = ((TypeExpr)ne.exprs.elementAt(0)).type;
    836                // the second argument should be a String literal
    837                Expr arg1 = ne.exprs.elementAt(1);
    838                if (arg1.getTag() != TagConstants.STRINGLIT) {
    839                  ErrorSet.error(arg1.getStartLoc(),
    840                                 "The second argument to \\dttfsa must be a String literal");
    841                } else {
    842                  LiteralExpr lit = (LiteralExpr)arg1;
    843                  String op = (String)lit.value;
    844                  if (op.equals("identity") && ne.exprs.size() != 3) {
    845                    ErrorSet.error(ne.sloc,
    846                                   "The function \\dttfsa requires exactly 3 arguments when the second argument is \"identity\"");
    847                  }
    848                }
    849              }
    850              setType(e, resultType);
    851              return e;
    852            }
    853
    854          case TagConstants.WACK_NOWARN:
    855          case TagConstants.NOWARN_OP:
    856          case TagConstants.WARN:
    857          case TagConstants.WARN_OP:
    858            {
    859              NaryExpr ne = (NaryExpr)e;
    860              Expr nu;
    861              if( ne.exprs.size() != 1 ) {
    862                ErrorSet.error(ne.sloc,
    863                               "The function " + TagConstants.toString(tag) +
    864                               " takes only one argument");
    865                setType( e, Types.errorType );
    866              } else {
    867                // Get rid of this - FIXME - these are an obsolete definition
    868                e = checkExpr(env, ne.exprs.elementAt(0));
    869                //ne.exprs.setElementAt( nu, 0 );
    870                //setType( e, getType(nu) );
    871              }
    872              return e;
    873            }
    874
    875          case TagConstants.ELEMTYPE:
    876            {
    877              NaryExpr ne = (NaryExpr)e;
    878              if( ne.exprs.size() != 1 )
    879                ErrorSet.error(ne.sloc,
    880                               "The function \\elemtype takes only one argument");
    881              else {
    882                Expr nu = checkExpr(env, ne.exprs.elementAt(0));
    883                ne.exprs.setElementAt( nu, 0 );
    884                if (!Types.isTypeType(getType(nu)))
    885                  ErrorSet.error(nu.getStartLoc(),
    886                                 "The argument must have TYPE type");
    887              }
    888              setType( e, Types.typecodeType );
    889              return e;
    890            }
    891
    892          case TagConstants.WACK_DURATION:
    893          case TagConstants.WACK_WORKING_SPACE:
    894          case TagConstants.SPACE:
    895            {
    896              NaryExpr ne = (NaryExpr)e;
    897              if( ne.exprs.size() != 1 )
    898                ErrorSet.error(ne.sloc,
    899                               "The function " + TagConstants.toString(tag) +
    900                               " takes only one argument");
    901              else {
    902                // Note: the arguments are not evaluated
    903                Expr nu = checkExpr(env, ne.exprs.elementAt(0));
    904                ne.exprs.setElementAt( nu, 0 );
    905              }
    906              setType( e, Types.longType );
    907              return e;
    908            }
    909
    910          case TagConstants.INVARIANT_FOR:
    911          case TagConstants.IS_INITIALIZED:
    912            {
    913              NaryExpr ne = (NaryExpr)e;
    914              // FIXME - Is this a one argument function ?
    915              if( ne.exprs.size() != 1 )
    916                ErrorSet.error( ne.sloc,
    917                                "The function takes only one argument");
    918              else {
    919                Expr nu = checkExpr(env, ne.exprs.elementAt(0));
    920                ne.exprs.setElementAt( nu, 0 );
    921              }
    922              setType( e, Types.booleanType );
    923              return e;
    924            }
    925
    926          case TagConstants.NOTMODIFIEDEXPR:
    927            {
    928              NotModifiedExpr ne = (NotModifiedExpr)e;
    929              ne.expr = checkExpr(env, ne.expr);
    930              setType( e, Types.booleanType );
    931              return e;
    932            }
    933
    934          case TagConstants.MAX:
    935            {
    936              NaryExpr ne = (NaryExpr)e;
    937              if( ne.exprs.size() != 1 )
    938                ErrorSet.error( ne.sloc,
    939                                "The function \\max takes only one argument");
    940              else {
    941                Expr nu = checkExpr(env, ne.exprs.elementAt(0), Types.locksetType);
    942                ne.exprs.setElementAt( nu, 0 );
    943              }
    944              setType( e, Types.javaLangObject() );
    945              return e;
    946            }
    947
    948          case TagConstants.PRE:
    949            {
    950              NaryExpr ne = (NaryExpr)e;
    951              if( ne.exprs.size() != 1 ) {
    952                ErrorSet.error( ne.sloc,
    953                                "The function \\old takes only one argument");
    954                setType(e, Types.voidType);
    955              } else if (!isTwoStateContext) {
    956                ErrorSet.error(ne.sloc,
    957                               "The function \\old cannot be used in this context");
    958                setType(e, Types.voidType);
    959              } else if (isInsidePRE) {
    960                ErrorSet.error(ne.sloc, "Nested applications of \\old not allowed");
    961                setType(e, Types.voidType);
    962              } else {
    963                isInsidePRE = true;
    964                Expr nu = checkExpr(env, ne.exprs.elementAt(0) );
    965                Assert.notFalse(isInsidePRE);
    966                isInsidePRE = false;
    967                ne.exprs.setElementAt( nu, 0 );
    968                setType( e, getType( nu ) );
    969              }
    970              return e;
    971            }
    972
    973          case TagConstants.TYPEOF:
    974            {
    975              NaryExpr ne = (NaryExpr)e;
    976              if( ne.exprs.size() != 1 )
    977                ErrorSet.error( ne.sloc,
    978                                "The function \\typeof takes only one argument");
    979              else {
    980                Expr ex = ne.exprs.elementAt(0);
    981                Expr nu = checkExpr(env, ex );
    982                ne.exprs.setElementAt( nu, 0 );
    983                Type t = getType(nu);
    984                if (t instanceof PrimitiveType) {
    985                  e = TypeExpr.make(ex.getStartLoc(),ex.getEndLoc(),t);
    986                }
    987              }
    988              setType( e, Types.typecodeType );
    989              return e;
    990            }
    991
    992          case TagConstants.TYPEEXPR:
    993            {
    994              TypeExpr te = (TypeExpr)e;
    995              env.resolveType( sig, te.type );
    996              setType(e, Types.typecodeType );
    997              return e;
    998            }
    999
    1000          case TagConstants.LABELEXPR:
    1001            {
    1002              LabelExpr le = (LabelExpr)e;
    1003              if (!isCurrentlyPredicateContext) {
    1004                ErrorSet.error(le.getStartLoc(),
    1005                               "Labeled predicates are not allowed in this context");
    1006                setType(e, Types.booleanType);
    1007              } else {
    1008                isPredicateContext = true;
    1009                le.expr = checkExpr(env, le.expr);
    1010                setType(e, getType( le.expr ) );
    1011              }
    1012              return e;
    1013            }
    1014
    1015          case TagConstants.NUM_OF:
    1016            {
    1017              NumericalQuantifiedExpr qe = (NumericalQuantifiedExpr)e;
    1018
    1019              // if (!isCurrentlyPredicateContext) {
    1020              //     ErrorSet.error(qe.getStartLoc(),
    1021              //       "Quantified expressions are not allowed in this context");
    1022              //   } else
    1023              {
    1024                Env subenv = env;
    1025
    1026                for( int i=0; i<qe.vars.size(); i++) {
    1027                  GenericVarDecl decl = qe.vars.elementAt(i);
    1028                  env.resolveType( sig, decl.type );
    1029
    1030                  subenv = new EnvForLocals(subenv, decl);
    1031                }
    1032                isPredicateContext = true;
    1033                qe.expr = checkExpr(subenv, qe.expr, Types.booleanType);
    1034              }
    1035              setType(e, Types.intType);
    1036              return e;
    1037            }
    1038
    1039          case TagConstants.SUM:
    1040          case TagConstants.PRODUCT:
    1041          case TagConstants.MIN:
    1042          case TagConstants.MAXQUANT:
    1043            {
    1044              GeneralizedQuantifiedExpr qe = (GeneralizedQuantifiedExpr)e;
    1045
    1046              /*
    1047                if (!isCurrentlyPredicateContext) {
    1048                ErrorSet.error(qe.getStartLoc(),
    1049                "Quantified expressions are not allowed in this context");
    1050                } else */
    1051              {
    1052                Env subenv = env;
    1053
    1054                for( int i=0; i<qe.vars.size(); i++) {
    1055                  GenericVarDecl decl = qe.vars.elementAt(i);
    1056                  env.resolveType( sig, decl.type );
    1057
    1058                  subenv = new EnvForLocals(subenv, decl);
    1059                }
    1060                isPredicateContext = true;
    1061                qe.rangeExpr = checkExpr(subenv, qe.rangeExpr, Types.booleanType);
    1062                qe.expr = checkExpr(subenv, qe.expr, Types.intType);
    1063              }
    1064              setType(e, Types.intType);
    1065              return e;
    1066            }
    1067
    1068          case TagConstants.FORALL:
    1069          case TagConstants.EXISTS:
    1070            {
    1071              QuantifiedExpr qe = (QuantifiedExpr)e;
    1072
    1073              if (!isCurrentlyPredicateContext) {
    1074                ErrorSet.error(qe.getStartLoc(),
    1075                               "Quantified expressions are not allowed in this context");
    1076              } else {
    1077                Env subenv = env;
    1078
    1079                for( int i = 0; i < qe.vars.size(); i++) {
    1080                  GenericVarDecl decl = qe.vars.elementAt(i);
    1081                  env.resolveType(sig, decl.type);
    1082
    1083                  subenv = new EnvForLocals(subenv, decl, false);
    1084                }
    1085                isPredicateContext = true;
    1086                if (qe.rangeExpr != null) {
    1087                  qe.rangeExpr = checkExpr(subenv, qe.rangeExpr, Types.booleanType);
    1088                }
    1089                qe.expr = checkExpr(subenv, qe.expr, Types.booleanType);
    1090              }
    1091              if (qe.rangeExpr == null) { // skip
    1092              } else if (tag == TagConstants.FORALL) {
    1093                qe.expr = BinaryExpr.make(TagConstants.IMPLIES,
    1094                                          qe.rangeExpr,qe.expr,Location.NULL);
    1095                setType(qe.expr,Types.booleanType);
    1096              } else {
    1097                qe.expr = BinaryExpr.make(TagConstants.AND,
    1098                                          qe.rangeExpr,qe.expr,Location.NULL);
    1099                setType(qe.expr,Types.booleanType);
    1100              }
    1101              setType(e, Types.booleanType);
    1102              return e;
    1103            }
    1104
    1105          case TagConstants.PARENEXPR:
    1106          case TagConstants.NOT:
    1107            {
    1108              // the sub-expression is allowed to contain quantifiers and
    1109              // labels if this expression is
    1110              isPredicateContext = isCurrentlyPredicateContext;
    1111              return super.checkExpr(env, e);
    1112            }
    1113
    1114          case TagConstants.ADD:
    1115            {
    1116              Expr ee = super.checkExpr(env, e);
    1117              if (!Main.options().useOldStringHandling &&
    1118                  Types.isSameType(getType(ee),Types.javaLangString())) {
    1119                 boolean savedInAnnotation = inAnnotation;
    1120                 inAnnotation = true;
    1121                 BinaryExpr be = (BinaryExpr)ee;
    1122                 Expr left = be.left;
    1123                 Expr right = be.right;
    1124                 if (!Types.isSameType(getType(left),Types.javaLangString())) {
    1125                    Name nn = Name.make("java.lang.String.valueOf",left.getStartLoc());
    1126                    ExprVec a = ExprVec.make();
    1127                    a.addElement(left);
    1128                    AmbiguousMethodInvocation mi = AmbiguousMethodInvocation.make(
    1129                        nn,null,left.getStartLoc(),a);
    1130                    MethodInvocation mm = env.disambiguateMethodName(mi);
    1131                    left = checkExpr(env, mm);
    1132                 }
    1133                 if (!Types.isSameType(getType(right),Types.javaLangString())) {
    1134                    Name nn = Name.make("java.lang.String.valueOf",right.getStartLoc());
    1135                    ExprVec a = ExprVec.make();
    1136                    a.addElement(right);
    1137                    AmbiguousMethodInvocation mi = AmbiguousMethodInvocation.make(
    1138                        nn,null,right.getStartLoc(),a);
    1139                    MethodInvocation mm = env.disambiguateMethodName(mi);
    1140                    right = checkExpr(env, mm);
    1141                 }
    1142                 int loc = be.locOp;
    1143                 Name n = Name.make(TagConstants.STRINGCATINFIX,loc);
    1144                 ExprVec args = ExprVec.make();
    1145                 args.addElement(left);
    1146                 args.addElement(right);
    1147                 AmbiguousMethodInvocation ami = AmbiguousMethodInvocation.make(
    1148                        n,null,loc,args);
    1149                 MethodInvocation m = env.disambiguateMethodName(ami);
    1150                 ee = checkExpr(env, m);
    1151                 inAnnotation = savedInAnnotation;
    1152              }
    1153              return ee;
    1154            }
    1155
    1156          case TagConstants.OR:
    1157          case TagConstants.AND:
    1158          case TagConstants.EQ:
    1159          case TagConstants.NE:
    1160            {
    1161              BinaryExpr be = (BinaryExpr)e;
    1162              // each argument is allowed to contain quantifiers and labels if
    1163              // this expression is
    1164              isPredicateContext = isCurrentlyPredicateContext;
    1165              be.left = checkExpr(env, be.left);
    1166              isPredicateContext = isCurrentlyPredicateContext;
    1167              be.right = checkExpr(env, be.right);
    1168              if (false && Types.isTypeType(getType(be.left)) &&
    1169                  // DO WE NEED TO check the composite expressions ??? FIXME TYPE-EQUIV
    1170                  Types.isTypeType(getType(be.right))) {
    1171                setType( be, Types.booleanType);
    1172              } else {
    1173                Type t = checkBinaryExpr(be.op, be.left, be.right, be.locOp);
    1174                setType( be, t );
    1175              }
    1176              return be;
    1177            }
    1178
    1179          case TagConstants.WILDREFEXPR:
    1180            {
    1181              // FIXME - WildRefExpr needs cleanup .  In current usage r.od is always null
    1182              // on input.
    1183              WildRefExpr r = (WildRefExpr)e;
    1184              if (!isCurrentlySpecDesignatorContext) {
    1185                setType(r, Types.errorType);
    1186                ErrorSet.error(r.getStartLoc(),
    1187                               "Reference wild cards allowed only as "+
    1188                               "specification designators");
    1189              } else {
    1190                // Can't set the type, but need to check the type of the od
    1191                if (r.od == null) {
    1192                  if (r.var instanceof AmbiguousVariableAccess) {
    1193                    AmbiguousVariableAccess a = (AmbiguousVariableAccess)r.var;
    1194                    Object o = env.disambiguateTypeOrFieldName(a.name);
    1195                    if (o instanceof TypeSig) {
    1196                      r.od = TypeObjectDesignator.make(r.var.getStartLoc(),
    1197                                                       (TypeSig)o );
    1198                    } else {
    1199                      r.var = checkExpr(env,r.var);
    1200                      // FIXME - really need locDot here
    1201                      r.od = ExprObjectDesignator.make(
    1202                                                       r.var.getEndLoc(),
    1203                                                       r.var);
    1204                    }
    1205                    r.var = null;
    1206                  } else {
    1207                    r.var = checkExpr(env,r.var);
    1208                    // FIXME - really need locDot here
    1209                    r.od = ExprObjectDesignator.make(
    1210                                                     r.var.getEndLoc(),
    1211                                                     r.var);
    1212                  }
    1213                  checkObjectDesignator(env,r.od);
    1214                } else {
    1215                  Type t = checkObjectDesignator(env,r.od);
    1216                  // FIXME
    1217                  //System.out.println("TYPE " + t);
    1218                }
    1219              }
    1220              return r;
    1221            }
    1222
    1223          case TagConstants.ARRAYREFEXPR:
    1224            {
    1225              ArrayRefExpr r = (ArrayRefExpr)e;
    1226
    1227              r.array = checkExpr(env, r.array);
    1228              Type arrType = getType( r.array );
    1229              r.index = checkExpr(env, r.index);
    1230              Type t = getType( r.index );
    1231
    1232              if( arrType instanceof ArrayType ) {
    1233                setType( r, ((ArrayType)arrType).elemType );
    1234                Type ndxType =
    1235                  Types.isNumericType( t ) ? Types.unaryPromote( t ) : t;
    1236                if( !Types.isSameType( ndxType, Types.intType ) &&
    1237                    !Types.isErrorType(ndxType) )
    1238                  ErrorSet.error(r.locOpenBracket, "Array index is not an integer");
    1239
    1240              } else if( arrType.getTag() == TagConstants.LOCKSET ) {
    1241                setType( r, Types.booleanType );
    1242                if( !Types.isReferenceOrNullType( t ) &&
    1243                    !Types.isErrorType(t) )
    1244                  ErrorSet.error(r.locOpenBracket,
    1245                                 "Can only index \\lockset with a reference type");
    1246              } else {
    1247                setType( r, Types.errorType );
    1248                if (!Types.isErrorType(arrType) )
    1249                  ErrorSet.error( r.locOpenBracket,
    1250                                  "Attempt to index a non-array value");
    1251              }
    1252
    1253              return r;
    1254            }
    1255
    1256          case TagConstants.ARRAYRANGEREFEXPR:
    1257            {
    1258              ArrayRangeRefExpr r = (ArrayRangeRefExpr)e;
    1259              if (!isCurrentlySpecDesignatorContext) {
    1260                setType(r, Types.errorType);
    1261                ErrorSet.error(r.getStartLoc(),
    1262                               "Array ranges are allowed only as "+
    1263                               "specification designators");
    1264              } else {
    1265
    1266                r.array = checkExpr(env, r.array);
    1267                Type arrType = getType( r.array );
    1268                if (r.lowIndex != null) r.lowIndex = checkExpr(env, r.lowIndex);
    1269                if (r.highIndex != null) r.highIndex = checkExpr(env, r.highIndex);
    1270                Type t = r.lowIndex == null ? null : getType( r.lowIndex );
    1271                Type tt = r.highIndex == null ? null : getType( r.highIndex );
    1272
    1273                if( arrType instanceof ArrayType ) {
    1274                  setType( r, ((ArrayType)arrType).elemType );
    1275                  if (t != null) {
    1276                    Type ndxType =
    1277                      Types.isNumericType( t ) ? Types.unaryPromote( t ) : t;
    1278                    if( !Types.isSameType( ndxType, Types.intType ) &&
    1279                        !Types.isErrorType(ndxType) )
    1280                      ErrorSet.error(r.locOpenBracket, "Array index is not an integer");
    1281                  }
    1282                  if (tt != null) {
    1283                    Type ndxType =
    1284                      Types.isNumericType( tt ) ? Types.unaryPromote( tt ) : tt;
    1285                    if( !Types.isSameType( ndxType, Types.intType ) &&
    1286                        !Types.isErrorType(ndxType) )
    1287                      ErrorSet.error(r.locOpenBracket, "Array index is not an integer");
    1288                  }
    1289
    1290                } else {
    1291                  setType( r, Types.errorType );
    1292                  if (!Types.isErrorType(arrType) )
    1293                    ErrorSet.error( r.locOpenBracket,
    1294                                    "Attempt to index a non-array value");
    1295                }
    1296              }
    1297
    1298              return r;
    1299            }
    1300          case TagConstants.RESEXPR:
    1301            {
    1302              if (!isRESContext || returnType == null) {
    1303                if (!Types.isErrorType(returnType))
    1304                  ErrorSet.error(e.getStartLoc(),
    1305                                 "Keyword \\result is not allowed in this context");
    1306                setType( e, Types.errorType );
    1307              }
    1308              else
    1309                setType( e, returnType );
    1310
    1311              return e;
    1312            }
    1313
    1314          case TagConstants.SETCOMPEXPR:
    1315            {
    1316              SetCompExpr s = (SetCompExpr)e;
    1317
    1318              env.resolveType(sig, s.type);
    1319              env.resolveType(sig, s.fp.type);
    1320              Env subenv = new EnvForLocals(env,s.fp,false);
    1321              boolean savedPredicateContext = isPredicateContext;
    1322              isPredicateContext = true;
    1323              s.expr = checkExpr(subenv, s.expr, Types.booleanType);
    1324              isPredicateContext = savedPredicateContext;
    1325              setType( e, s.type);
    1326              // FIXME - CHeck that the type is only JMLObjectSet, JMLValueSet
    1327              // Check that the predicate has the correct restricted form
    1328              return e;
    1329            }
    1330
    1331          case TagConstants.NOTSPECIFIEDEXPR:
    1332            {
    1333              setType( e, Types.voidType);
    1334              return e;
    1335            }
    1336          case TagConstants.EVERYTHINGEXPR:
    1337            {
    1338              if (!isCurrentlySpecDesignatorContext) {
    1339                ErrorSet.error(e.getStartLoc(),
    1340                               "Keyword \\everything is not allowed in this context");
    1341                setType( e, Types.errorType);
    1342              } else {
    1343                setType( e, Types.voidType);
    1344              }
    1345              return e;
    1346            }
    1347          case TagConstants.NOTHINGEXPR:
    1348            {
    1349              if (!isCurrentlySpecDesignatorContext) {
    1350                ErrorSet.error(e.getStartLoc(),
    1351                               "Keyword \\nothing is not allowed in this context");
    1352                setType( e, Types.errorType);
    1353              } else {
    1354                setType( e, Types.voidType);
    1355              }
    1356              return e;
    1357            }
    1358          case TagConstants.LOCKSETEXPR:
    1359            {
    1360              if (! isLocksetContext) {
    1361                ErrorSet.error(e.getStartLoc(),
    1362                               "Keyword \\lockset is not allowed in this context");
    1363              }
    1364              setType( e, Types.locksetType );
    1365              return e;
    1366            }
    1367
    1368          case TagConstants.LE:
    1369          case TagConstants.LT:
    1370            {
    1371              BinaryExpr be = (BinaryExpr)e;
    1372              be.left = checkExpr(env, be.left);
    1373              be.right = checkExpr(env, be.right);
    1374
    1375              if( Types.isReferenceOrNullType( getType( be.left ) )
    1376                  && Types.isReferenceOrNullType( getType( be.right ) ) ) {
    1377                // is lock comparison, and is ok
    1378                setType( be, Types.booleanType );
    1379                return be;
    1380              } else {
    1381                return super.checkExpr(env, e);
    1382              }
    1383            }
    1384
    1385          case TagConstants.NEWINSTANCEEXPR:
    1386          case TagConstants.NEWARRAYEXPR:
    1387            {
    1388              countFreeVarsAccesses++;
    1389              /* FIXME - Yes it can, but it must be pure!
    1390                 if (inAnnotation) {
    1391                 ErrorSet.error(e.getStartLoc(),
    1392                 "new cannot be used in specification expressions");
    1393                 }
    1394              */
    1395              return super.checkExpr(env, e);
    1396            }
    1397
    1398          case TagConstants.ASSIGN: case TagConstants.ASGMUL:
    1399          case TagConstants.ASGDIV: case TagConstants.ASGREM:
    1400          case TagConstants.ASGADD: case TagConstants.ASGSUB:
    1401          case TagConstants.ASGLSHIFT: case TagConstants.ASGRSHIFT:
    1402          case TagConstants.ASGURSHIFT: case TagConstants.ASGBITAND:
    1403          case TagConstants.ASGBITOR: case TagConstants.ASGBITXOR:
    1404            {
    1405              if (inAnnotation && !inModelBody) {
    1406                BinaryExpr be = (BinaryExpr)e;
    1407                ErrorSet.error(be.locOp,
    1408                               "assignments cannot be used in specification expressions");
    1409              }
    1410              return super.checkExpr(env, e);
    1411            }
    1412
    1413          case TagConstants.INC: case TagConstants.DEC:
    1414          case TagConstants.POSTFIXINC: case TagConstants.POSTFIXDEC:
    1415            {
    1416              if (inAnnotation && !inModelBody) {
    1417                UnaryExpr ue = (UnaryExpr)e;
    1418                ErrorSet.error(ue.locOp,
    1419                               "assignments cannot be used in specification expressions");
    1420              }
    1421              return super.checkExpr(env, e);
    1422            }
    1423
    1424          default:
    1425            return super.checkExpr(env, e);
    1426          }
    1427
    1428        } finally {
    1429
    1430          isPredicateContext = isCurrentlyPredicateContext;
    1431        }
    1432      }
    1433
    1434      // Pragma checkers
    1435
    1436      protected  void checkTypeDeclElemPragma(TypeDeclElemPragma e) {
    1437        int tag = e.getTag();
    1438        boolean savedInAnnotation = inAnnotation;
    1439        inAnnotation = true;        // Must be reset before we exit!
    1440        try {
    1441
    1442          switch(tag) {
    1443          case TagConstants.AXIOM:
    1444          case TagConstants.INITIALLY:
    1445          case TagConstants.INVARIANT:
    1446          case TagConstants.CONSTRAINT: // FIXME - do we need to change the logic below to handle constraints?
    1447            {
    1448              ExprDeclPragma ep = (ExprDeclPragma)e;
    1449              Env rootEnv = (tag == TagConstants.AXIOM ||
    1450                             Modifiers.isStatic(ep.modifiers)) ? rootSEnv : rootIEnv;
    1451
    1452              invariantContext = (tag == TagConstants.INVARIANT) ||
    1453                tag == TagConstants.INITIALLY;
    1454              isTwoStateContext = (tag == TagConstants.CONSTRAINT);
    1455              boolean oldIsLocksetContext = isLocksetContext;
    1456              isLocksetContext = false;
    1457              if (invariantContext){
    1458                // FIXME                       Assert.notFalse(countFreeVarsAccesses == 0);
    1459                countFreeVarsAccesses = 0;
    1460              }
    1461
    1462              ep.expr = checkPredicate(rootEnv, ep.expr);
    1463              isLocksetContext = oldIsLocksetContext;
    1464
    1465              TypeSig sig = TypeSig.getSig(e.getParent());
    1466              if (sig==javafe.tc.Types.javaLangObject() ||
    1467                  sig==javafe.tc.Types.javaLangCloneable()) {
    1468                if (invariantContext) ErrorSet.fatal(e.getStartLoc(),
    1469                                                     "java.lang.Object and java.lang.Cloneable may not"
    1470                                                     + " contain invariants.");  // FIXME - Why?
    1471              }
    1472              /*
    1473                FIXME - see uses of countFreeVarsAccess
    1474                if (invariantContext && countFreeVarsAccesses == 0 &&
    1475                // Don't print an error if the entire invariant
    1476                // is an informal predicate
    1477                escjava.parser.EscPragmaParser.
    1478                informalPredicateDecoration.get(ep.expr)==null) {
    1479                ErrorSet.error(e.getStartLoc(),
    1480                "Class invariants must mention program variables"
    1481                + " or fields.");
    1482                }
    1483              */
    1484
    1485              if (invariantContext) {countFreeVarsAccesses = 0;}
    1486              invariantContext = false;
    1487              isTwoStateContext = false;
    1488              break;
    1489            }
    1490          case TagConstants.REPRESENTS:
    1491            {
    1492              NamedExprDeclPragma ep = (NamedExprDeclPragma)e;
    1493              boolean stat = Modifiers.isStatic(ep.modifiers);
    1494
    1495              // What about static model vars?
    1496              // Can the represents clause be static ? FIXME
    1497              Env rootEnv = stat? rootSEnv : rootIEnv;
    1498              ep.target = checkExpr(rootEnv, ep.target);
    1499
    1500              if (ep.target instanceof FieldAccess) {
    1501                invariantContext = false;
    1502                isTwoStateContext = false;
    1503                boolean oldIsLocksetContext = isLocksetContext;
    1504                isLocksetContext = false;
    1505                if (invariantContext){
    1506                  // FIXME                       Assert.notFalse(countFreeVarsAccesses == 0);
    1507                  countFreeVarsAccesses = 0;
    1508                }
    1509
    1510                ep.expr = checkPredicate(rootEnv, ep.expr);
    1511                isLocksetContext = oldIsLocksetContext;
    1512
    1513                FieldAccess fa = (FieldAccess)ep.target;
    1514                if (!Utils.isModel(fa.decl)) {
    1515                  ErrorSet.error(fa.getStartLoc(),
    1516                                 "A represents clause must name a model field",
    1517                                 fa.decl.locId);
    1518                }
    1519                if (stat && !Modifiers.isStatic(fa.decl.modifiers)) {
    1520                  ErrorSet.error(fa.getStartLoc(),
    1521                                 "A static represents clause must name a static model field");
    1522                }
    1523                if (!stat && Modifiers.isStatic(fa.decl.modifiers)) {
    1524                  ErrorSet.error(fa.getStartLoc(),
    1525                                 "A non-static represents clause must name a non-static model field");
    1526                }
    1527
    1528                /* THis is done in type prepping
    1529                   TypeDecl td = ep.parent;
    1530                   TypeDeclElemVec tv = (TypeDeclElemVec)Utils.representsDecoration.get(td);
    1531                   if (tv == null) {
    1532                   tv = TypeDeclElemVec.make(10);
    1533                   Utils.representsDecoration.set(td,tv);
    1534                   }
    1535                   tv.addElement(ep);
    1536                */
    1537                   TypeDeclElemVec tv = (TypeDeclElemVec)Utils.representsDecoration.get(fa.decl);
    1538                   if (tv == null) {
    1539                       tv = TypeDeclElemVec.make(10);
    1540                       Utils.representsDecoration.set(fa.decl,tv);
    1541                   }
    1542                   tv.addElement(ep);
    1543              } else if (!(ep.target instanceof AmbiguousVariableAccess)){
    1544                // If the type is Ambiguous, then an Undefined variable
    1545                // error has already been issued.  I'm not actually
    1546                // sure that this point is reachable.
    1547                ErrorSet.error(ep.target.getStartLoc(),
    1548                               "Expected a field identifier here");
    1549              }
    1550              break;
    1551            }
    1552          case TagConstants.DEPENDS:
    1553            {
    1554              DependsPragma ep = (DependsPragma)e;
    1555              // FIXME - perhaps use rootSEnv if the variable
    1556              // being discussed is static ?
    1557              Env rootEnv = rootIEnv;
    1558
    1559              ep.target = checkExpr(rootEnv, ep.target);
    1560
    1561              ExprVec ev = ep.exprs;
    1562              for (int i=0; i<ev.size(); ++i) {
    1563                ev.setElementAt(
    1564                                checkExpr(rootEnv, ev.elementAt(i)), i);
    1565              }
    1566
    1567              // FIXME - Need to check that
    1568              //    LHS is a simple model variable, a field of
    1569              //            this or a super class or an interface
    1570              //    RHS consists of store-refs, no computed expressions
    1571              //    RHS may have other model variables
    1572              //    check access ?
    1573              break;
    1574            }
    1575
    1576          case TagConstants.MODELCONSTRUCTORDECLPRAGMA: {
    1577            ModelConstructorDeclPragma me = (ModelConstructorDeclPragma)e;
    1578            ConstructorDecl cd = me.decl;
    1579            Env rootEnv = Modifiers.isStatic(cd.modifiers)
    1580              ? rootSEnv
    1581              : rootIEnv;
    1582
    1583            // All gets checked since the associated ConstructorDecl is
    1584            // part of the type
    1585
    1586            // FIXME - the body needs to allow ghost/model vars
    1587            break;
    1588          }
    1589
    1590
    1591          case TagConstants.MODELMETHODDECLPRAGMA: {
    1592            MethodDecl decl = ((ModelMethodDeclPragma)e).decl;
    1593            Env rootEnv = Modifiers.isStatic(decl.modifiers)
    1594              ? rootSEnv
    1595              : rootIEnv;
    1596
    1597            // All gets checked since the associated ConstructorDecl is
    1598            // part of the type
    1599
    1600            // FIXME - the body needs to allow ghost/model vars
    1601            break;
    1602          }
    1603
    1604          case TagConstants.MONITORS_FOR: {
    1605            IdExprDeclPragma emp = (IdExprDeclPragma)e;
    1606            Identifier id = emp.id;
    1607            TypeDeclElemVec elems = e.parent.elems;
    1608            FieldDecl fd = null;
    1609            for (int i=0; i<elems.size(); ++i) {
    1610              TypeDeclElem td = elems.elementAt(i);
    1611              if (td instanceof FieldDecl &&
    1612                  ((FieldDecl)td).id == id) {
    1613                fd = (FieldDecl)td;
    1614                break;
    1615              }
    1616            }
    1617            boolean isStatic = false;
    1618            if (fd == null) {
    1619              ErrorSet.error(emp.loc,
    1620                             "Could not find identifier " + id + " in this class");
    1621            } else {
    1622              isStatic = Modifiers.isStatic(fd.modifiers);
    1623            }
    1624            if (Modifiers.isStatic(emp.modifiers)) isStatic = true;
    1625            Env env = isStatic ? rootSEnv : rootIEnv;
    1626            int oldAccessibilityLowerBound = accessibilityLowerBound;
    1627            ASTNode oldAccessibilityContext = accessibilityContext;
    1628            accessibilityLowerBound = getAccessibility(fd.modifiers);
    1629            accessibilityContext = fd;
    1630            emp.expr = checkExpr(env, emp.expr, Types.javaLangObject());
    1631            accessibilityLowerBound = oldAccessibilityLowerBound;
    1632            accessibilityContext = oldAccessibilityContext;
    1633            fd.pmodifiers.addElement(
    1634                                     ExprModifierPragma.make(
    1635                                                             TagConstants.MONITORED_BY,
    1636                                                             emp.expr,
    1637                                                             emp.loc
    1638                                                             ));
    1639            break;
    1640          }
    1641
    1642          case TagConstants.WRITABLE:
    1643          case TagConstants.READABLE: {
    1644            NamedExprDeclPragma emp = (NamedExprDeclPragma)e;
    1645
    1646            isSpecDesignatorContext = true;
    1647            Env newenv = rootIEnv;
    1648            emp.target = checkDesignator(newenv, emp.target);
    1649            isSpecDesignatorContext = false;
    1650            emp.expr = checkPredicate(newenv, emp.expr);
    1651            switch (emp.target.getTag()) {
    1652            case TagConstants.FIELDACCESS: {
    1653              FieldAccess fa = (FieldAccess)emp.target;
    1654              if (fa.decl != null &&
    1655                  // The array "length" field has already been checked
    1656                  // insuper.checkDesignator().
    1657                  fa.decl != Types.lengthFieldDecl) {
    1658
    1659                if (tag == TagConstants.WRITABLE &&
    1660                    Modifiers.isFinal(fa.decl.modifiers)) {
    1661                  // FIXME
    1662                }
    1663                fa.decl.pmodifiers.addElement(
    1664                                              ExprModifierPragma.make(
    1665                                                                      emp.tag == TagConstants.READABLE ?
    1666                                                                      TagConstants.READABLE_IF:
    1667                                                                      TagConstants.WRITABLE_IF,
    1668                                                                      emp.expr,
    1669                                                                      emp.loc
    1670                                                                      )
    1671                                              );
    1672              }
    1673              break;
    1674            }
    1675
    1676            case TagConstants.ARRAYREFEXPR:
    1677            case TagConstants.ARRAYRANGEREFEXPR:
    1678            case TagConstants.WILDREFEXPR:
    1679            case TagConstants.EVERYTHINGEXPR:
    1680            case TagConstants.NOTHINGEXPR:
    1681            case TagConstants.NOTSPECIFIEDEXPR:
    1682              // FIXME - not implemented
    1683              break;
    1684
    1685            default:
    1686              if (escjava.parser.EscPragmaParser.
    1687                  informalPredicateDecoration.get(emp.target)==null) {
    1688                // The expression is not a designator
    1689                // but we allow an informal predicate
    1690                if (!Types.isErrorType(getType(emp.target)))
    1691                  ErrorSet.error(emp.target.getStartLoc(),
    1692                                 "Not a specification designator expression");
    1693              } else {
    1694                emp.target = null;
    1695              }
    1696            }
    1697            break;
    1698          }
    1699
    1700          case TagConstants.MODELDECLPRAGMA: {
    1701            FieldDecl decl = ((ModelDeclPragma)e).decl;
    1702            Env rootEnv = Modifiers.isStatic(decl.modifiers)
    1703              ? rootSEnv
    1704              : rootIEnv;
    1705
    1706            rootEnv.resolveType( sig, decl.type );
    1707            checkModifierPragmaVec( decl.pmodifiers, decl, rootEnv );
    1708            checkTypeModifiers(rootEnv, decl.type);
    1709
    1710            // Check for both static and instance declarations
    1711
    1712            if (Modifiers.isStatic(decl.modifiers)) {
    1713              ModifierPragma inst = Utils.findModifierPragma(decl,
    1714                                                             TagConstants.INSTANCE);
    1715              if (inst != null) ErrorSet.error(inst.getStartLoc(),
    1716                                               "May not specify both static and instance on a declaration");
    1717            }
    1718
    1719            /*
    1720             * Check for other fields with the same name:
    1721             */
    1722            {
    1723              TypeDeclElemVec elems = decl.parent.elems;
    1724              FieldDecl fd;
    1725              for (int i = 0; i<elems.size(); ++i) {
    1726                TypeDeclElem tde = elems.elementAt(i);
    1727                if (tde instanceof FieldDecl) {
    1728                  fd = (FieldDecl)tde;
    1729                } else if (tde instanceof GhostDeclPragma) {
    1730                  fd = ((GhostDeclPragma)tde).decl;
    1731                } else if (tde instanceof ModelDeclPragma) {
    1732                  fd = ((ModelDeclPragma)tde).decl;
    1733                } else
    1734                  continue;
    1735                if (fd.id ==  decl.id && fd != decl)
    1736                  ErrorSet.error(decl.locId,
    1737                                 "Another field named '"+decl.id.toString()
    1738                                 +"' already exists in this type", fd.locId);
    1739              }
    1740            }
    1741
    1742            break;
    1743          }
    1744
    1745          case TagConstants.GHOSTDECLPRAGMA: {
    1746            FieldDecl decl = ((GhostDeclPragma)e).decl;
    1747            ModifierPragma inst = Utils.findModifierPragma(decl,
    1748                                                           TagConstants.INSTANCE);
    1749            // Check for both static and instance declarations
    1750
    1751            if (Modifiers.isStatic(decl.modifiers)) {
    1752              if (inst != null) ErrorSet.error(inst.getStartLoc(),
    1753                                               "May not specify both static and instance on a declaration");
    1754            }
    1755
    1756            Env rootEnv = Modifiers.isStatic(decl.modifiers)
    1757              ? rootSEnv
    1758              : rootIEnv;
    1759
    1760            rootEnv.resolveType( sig, decl.type );
    1761            checkModifierPragmaVec( decl.pmodifiers, decl, rootEnv );
    1762            checkTypeModifiers(rootEnv, decl.type);
    1763
    1764
    1765
    1766            /*
    1767             * Handle initializer:
    1768             */
    1769
    1770            if (decl.init != null) {
    1771              leftToRight = true;
    1772              allowedExceptions.removeAllElements();
    1773              Assert.notFalse( allowedExceptions.size() == 0);
    1774              decl.init = checkInit(rootEnv, decl.init, decl.type);
    1775            }
    1776
    1777            /*
    1778             * Check for other fields with the same name:
    1779             */
    1780            {
    1781              TypeDeclElemVec elems = decl.parent.elems;
    1782              FieldDecl fd;
    1783              for (int i = 0; i<elems.size(); ++i) {
    1784                TypeDeclElem tde = elems.elementAt(i);
    1785                if (tde instanceof FieldDecl) {
    1786                  fd = (FieldDecl)tde;
    1787                } else if (tde instanceof GhostDeclPragma) {
    1788                  fd = ((GhostDeclPragma)tde).decl;
    1789                } else if (tde instanceof ModelDeclPragma) {
    1790                  fd = ((ModelDeclPragma)tde).decl;
    1791                } else
    1792                  continue;
    1793                if (fd.id ==  decl.id && fd != decl)
    1794                  ErrorSet.error(decl.locId,
    1795                                 "Another field named '"+decl.id.toString()
    1796                                 +"' already exists in this type", fd.locId);
    1797              }
    1798            }
    1799
    1800
    1801            break;
    1802          }
    1803
    1804          case TagConstants.STILLDEFERREDDECLPRAGMA: {
    1805            StillDeferredDeclPragma sddp = (StillDeferredDeclPragma)e;
    1806            if (!sig.hasField(sddp.var)) {
    1807              ErrorSet.error(sddp.locId, "No such field");
    1808            }
    1809
    1810            // TBW:  To support still_deferred, one also needs to check that
    1811            // "sddp.var" is declared as writable-deferred in the direct
    1812            // superclass.
    1813            break;
    1814          }
    1815
    1816          default:
    1817            Assert.fail("Unexpected tag " + tag +
    1818                        " " + TagConstants.toString(tag));
    1819          }
    1820        } finally {
    1821          inAnnotation = savedInAnnotation;
    1822        }
    1823      }
    1824
    1825      protected Env checkModifierPragma(ModifierPragma p, ASTNode ctxt, Env env) {
    1826
    1827        boolean savedInAnnotation = inAnnotation;
    1828        inAnnotation = true;        // Must be reset before we exit!
    1829        try {
    1830          int tag = p.getTag();
    1831          switch(tag)
    1832            {
    1833            case TagConstants.EVERYTHINGEXPR:
    1834            case TagConstants.EVERYTHING:
    1835            case TagConstants.NOTHING:
    1836            case TagConstants.NOT_SPECIFIED:
    1837            case TagConstants.NOTHINGEXPR:
    1838            case TagConstants.NOTSPECIFIEDEXPR:
    1839              // FIXME - check the context???
    1840              break;
    1841
    1842            case TagConstants.UNINITIALIZED:
    1843              if( ctxt.getTag() != TagConstants.LOCALVARDECL ) {
    1844                int loc;
    1845                if (ctxt instanceof GenericVarDecl)
    1846                  loc = ((GenericVarDecl)ctxt).locId;
    1847                else
    1848                  loc = p.getStartLoc();
    1849                ErrorSet.error(loc,
    1850                               "The uninitialized annotation can occur only on "
    1851                               +"local variable declarations");
    1852              } else if( ((LocalVarDecl)ctxt).init == null ) {
    1853                ErrorSet.error(((GenericVarDecl)ctxt).locId,
    1854                               "The uninitialized annotation can occur only on "
    1855                               +"local variable declarations "
    1856                               +"that have an initializer");
    1857              }
    1858              break;
    1859
    1860            case TagConstants.MONITORED:
    1861              {
    1862                if( ctxt.getTag() != TagConstants.FIELDDECL ) {
    1863                  int loc;
    1864                  if (ctxt instanceof GenericVarDecl)
    1865                    loc = ((GenericVarDecl)ctxt).locId;
    1866                  else
    1867                    loc = p.getStartLoc();
    1868                  ErrorSet.error(loc,
    1869                                 "The monitored annotation can occur only on "
    1870                                 +"field declarations");
    1871                  /* added functionality to have monitors on static fields
    1872                     } else if (env.isStaticContext()) {
    1873                     FieldDecl fd = (FieldDecl)ctxt;
    1874                     ErrorSet.error(fd.locId,
    1875                     "The monitored annotation can occur only on "+
    1876                     "instance field declarations");
    1877                  */
    1878                }
    1879                break;
    1880              }
    1881
    1882            case TagConstants.NON_NULL:
    1883              // NOTE:  Part of the NON_NULL check is found in checkTypeDeclElem()
    1884              // above, since there's not enough context information here to
    1885              // determine whether a formal parameter is declared for a method
    1886              // override.
    1887              switch (ctxt.getTag()) {
    1888              case TagConstants.FORMALPARADECL:
    1889              case TagConstants.LOCALVARDECL:
    1890              case TagConstants.FIELDDECL: {
    1891                GenericVarDecl vd = (GenericVarDecl)ctxt;
    1892                if (! Types.isReferenceType(vd.type)) {
    1893                  ErrorSet.error(vd.locId,
    1894                                 "The non_null pragma can be applied only to "+
    1895                                 "variables, fields, and parameters of "+
    1896                                 "reference types");
    1897                }
    1898                break;
    1899              }
    1900              case TagConstants.METHODDECL: {
    1901                MethodDecl md = (MethodDecl) ctxt;
    1902                if (!Types.isReferenceType(md.returnType)) {
    1903                  ErrorSet.error(md.getStartLoc(),
    1904                                 "'non_null' can only be used with methods whose "+
    1905                                 "result type is a reference type");
    1906                }
    1907                break;
    1908              }
    1909              default:
    1910                ErrorSet.error(p.getStartLoc(),
    1911                               "The non_null pragma can be applied only to "+
    1912                               "variables, fields, parameters, and methods");
    1913                break;
    1914              }
    1915              break;
    1916
    1917              // FIXME - should have a spec_protected case as well ???
    1918            case TagConstants.SPEC_PUBLIC:
    1919            case TagConstants.SPEC_PROTECTED:
    1920              // JML now allows spec_public and spec_protected on declarations
    1921              // of any java accessibiilty
    1922              break;
    1923
    1924            case TagConstants.WRITABLE_DEFERRED:
    1925              {
    1926                if (ctxt.getTag() != TagConstants.FIELDDECL ||
    1927                    Modifiers.isStatic(((FieldDecl)ctxt).modifiers)) {
    1928                  ErrorSet.error(p.getStartLoc(),
    1929                                 "The writable_deferred annotation can occur only on "
    1930                                 +"instance field declarations");
    1931                }
    1932                break;
    1933              }
    1934
    1935            case TagConstants.INSTANCE:
    1936              {
    1937                int ctag = ctxt.getTag();
    1938
    1939                if (!(ctxt instanceof GhostDeclPragma) &&
    1940                    !(ctxt instanceof ModelDeclPragma)) {
    1941
    1942                  // FIXME - should this use Utils.isModel ???
    1943                  if (ctxt instanceof FieldDecl &&
    1944                      (Utils.findModifierPragma( ((FieldDecl)ctxt).pmodifiers, TagConstants.MODEL) != null ||
    1945                       Utils.findModifierPragma( ((FieldDecl)ctxt).pmodifiers, TagConstants.GHOST) != null )) {
    1946                    // skip
    1947                  } else {
    1948                    ErrorSet.error(p.getStartLoc(),
    1949                                   "An instance modifier may only be applied to ghost and model fields");
    1950                  }
    1951                }
    1952
    1953                break;
    1954              }
    1955
    1956            case TagConstants.FUNCTION:
    1957              // FIXME - do some checking
    1958              // must be pure, static, immutable arguments, not void
    1959              break;
    1960
    1961            case TagConstants.PURE:
    1962              {
    1963                if (ctxt instanceof RoutineDecl) {
    1964                } else if (ctxt instanceof TypeDecl) {
    1965                } else {
    1966                  ErrorSet.error(p.getStartLoc(),
    1967                                 "Expected pure to modify a class, interface, constructor or method declaration");
    1968                }
    1969                break;
    1970              }
    1971
    1972            case TagConstants.HELPER:
    1973              switch (ctxt.getTag()) {
    1974              case TagConstants.CONSTRUCTORDECL:
    1975                ((ConstructorDecl)ctxt).modifiers |= Modifiers.ACC_HELPER;
    1976                break;
    1977              case TagConstants.METHODDECL:
    1978                {
    1979                  MethodDecl md = (MethodDecl) ctxt;
    1980                  md.modifiers |= Modifiers.ACC_HELPER;
    1981                  if (getOverrideStatus(md) != MSTATUS_NEW_ROUTINE) {
    1982                    ErrorSet.error(p.getStartLoc(),
    1983                                   "The helper pragma cannot be " +
    1984                                   "applied to a method override");
    1985                  } else if (isOverridable(md)) {
    1986                    ErrorSet.error(p.getStartLoc(),
    1987                                   "The helper pragma cannot be applied " +
    1988                                   "to method that can be overridden");
    1989                  } else if (md.body == null) {
    1990                    ErrorSet.error(p.getStartLoc(),
    1991                                   "The helper pragma cannot be applied " +
    1992                                   "to method without a body");
    1993                  }
    1994                  break;
    1995                }
    1996              default:
    1997                ErrorSet.error(p.getStartLoc(),
    1998                               "The helper pragma can only be applied to "+
    1999                               "methods and constructors");
    2000                break;
    2001              }
    2002              break;
    2003
    2004            case TagConstants.IMMUTABLE:
    2005              {
    2006                if (!(ctxt instanceof TypeDecl)) {
    2007                  ErrorSet.error(p.getStartLoc(),
    2008                                 "The immutable modifier may be applied only to type declarations");
    2009                }
    2010              }
    2011              break;
    2012
    2013            case TagConstants.WRITABLE_IF:
    2014            case TagConstants.READABLE_IF:
    2015              {
    2016                ExprModifierPragma emp = (ExprModifierPragma)p;
    2017
    2018                if( ctxt.getTag() != TagConstants.FIELDDECL
    2019                    && ctxt.getTag() != TagConstants.LOCALVARDECL ) {
    2020                  ErrorSet.error(p.getStartLoc(),
    2021                                 "The " + TagConstants.toString(tag)
    2022                                 +" annotation can occur only on "
    2023                                 +"field declarations and "
    2024                                 +"local variable declarations");
    2025                }
    2026
    2027                int oldAccessibilityLowerBound = accessibilityLowerBound;
    2028                ASTNode oldAccessibilityContext = accessibilityContext;
    2029                if (ctxt.getTag() == TagConstants.FIELDDECL) {
    2030                  FieldDecl fd = (FieldDecl)ctxt;
    2031                  accessibilityLowerBound = getAccessibility(fd.modifiers);
    2032                  accessibilityContext = fd;
    2033                }
    2034                emp.expr = checkPredicate(env, emp.expr);
    2035                accessibilityLowerBound = oldAccessibilityLowerBound;
    2036                accessibilityContext = oldAccessibilityContext;
    2037                break;
    2038              }
    2039
    2040            case TagConstants.NO_WACK_FORALL:
    2041            case TagConstants.OLD:
    2042              {
    2043                VarDeclModifierPragma vd = (VarDeclModifierPragma)p;
    2044                LocalVarDecl x = vd.decl;
    2045                env.resolveType( sig, vd.decl.type );
    2046                checkTypeModifiers(env, x.type);
    2047                javafe.tc.PrepTypeDeclaration.inst.
    2048                  checkModifiers(x.modifiers, Modifiers.NONE,
    2049                                 x.locId, "local specification variable");
    2050
    2051                boolean savedContext = isTwoStateContext;
    2052                isTwoStateContext = true;
    2053                // The case of x.init==null is illegal and should have
    2054                // been caught by the parser.
    2055                if (x.init != null) {
    2056                  //if (x.init instanceof ArrayInit) {
    2057                  x.init = checkInit(env, x.init, x.type);
    2058                  //} else {
    2059                  //checkExpr(newEnv, (Expr)x.init, x.type);
    2060                  //}
    2061                }
    2062                isTwoStateContext = savedContext;
    2063                // We create the new environment after checking the
    2064                // initializer to be sure that the initializer does not
    2065                // reference itself.
    2066                env = new EnvForGhostLocals(env,x);
    2067                break;
    2068              }
    2069
    2070            case TagConstants.ALSO_REQUIRES:
    2071            case TagConstants.REQUIRES:
    2072            case TagConstants.PRECONDITION:
    2073              {
    2074                ExprModifierPragma emp = (ExprModifierPragma)p;
    2075
    2076                if( ctxt instanceof InitBlock ) {
    2077                  if (emp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR)
    2078                    emp.expr = checkPredicate(env, emp.expr);
    2079                } else if( ctxt instanceof RoutineDecl ) {
    2080                  RoutineDecl rd = (RoutineDecl)ctxt;
    2081
    2082                  int ms = getOverrideStatus(rd);
    2083
    2084                  Env newenv = env;
    2085                  /* Interpret constructor as acting on an existing object, to initialize it,
    2086                     so this and fields are in scope.
    2087                     if (rd instanceof ConstructorDecl) {
    2088                     newenv = env.asStaticContext();
    2089                     }
    2090                  */
    2091                  int oldAccessibilityLowerBound = accessibilityLowerBound;
    2092                  ASTNode oldAccessibilityContext = accessibilityContext;
    2093                  accessibilityLowerBound = getAccessibility(rd.modifiers);
    2094                  accessibilityContext = rd;
    2095                  if (emp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR)
    2096                    emp.expr = checkPredicate(newenv, emp.expr);
    2097                  accessibilityLowerBound = oldAccessibilityLowerBound;
    2098                  accessibilityContext = oldAccessibilityContext;
    2099                } else {
    2100                  ErrorSet.error(p.getStartLoc(), TagConstants.toString(tag) +
    2101                                 " annotations can occur only on method" +
    2102                                 ((tag == TagConstants.REQUIRES ||
    2103                                   tag == TagConstants.PRECONDITION) ? " and constructor" : "") +
    2104                                 " declarations");
    2105                }
    2106                break;
    2107              }
    2108
    2109            case TagConstants.MEASURED_BY:
    2110            case TagConstants.DURATION:
    2111            case TagConstants.WORKING_SPACE:
    2112              {
    2113                CondExprModifierPragma emp = (CondExprModifierPragma)p;
    2114
    2115                if( !(ctxt instanceof RoutineDecl ) ) {
    2116                  ErrorSet.error(p.getStartLoc(),
    2117                                 TagConstants.toString(tag)
    2118                                 +" annotations can occur only on "
    2119                                 +"method and constructor declarations");
    2120                } else {
    2121                  RoutineDecl rd = (RoutineDecl)ctxt;
    2122                  boolean oldIsRESContext = isRESContext;
    2123                  boolean oldIsTwoStateContext = isTwoStateContext;
    2124                  boolean oldIsPrivFieldAccessAllowed = isPrivateFieldAccessAllowed;
    2125                  isRESContext = true;
    2126                  isTwoStateContext = true;
    2127                  // If "rd" is an overridable method, then every private field
    2128                  // mentioned in "emp.expr" must be spec_public.
    2129                  if (rd instanceof MethodDecl && isOverridable((MethodDecl)rd)) {
    2130                    isPrivateFieldAccessAllowed = false;
    2131                  }
    2132                  try {
    2133                    if (tag == TagConstants.MEASURED_BY) {
    2134                      // FIXME - what type to use?
    2135                      emp.expr = checkExpr(env, emp.expr);
    2136                    } else if (emp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR)
    2137                      emp.expr = checkExpr(env, emp.expr, Types.longType);
    2138                    if (emp.cond != null)
    2139                      emp.cond = checkExpr(env, emp.cond, Types.booleanType);
    2140                  } finally {
    2141                    isRESContext = oldIsRESContext;
    2142                    isTwoStateContext = oldIsTwoStateContext;
    2143                    isPrivateFieldAccessAllowed = oldIsPrivFieldAccessAllowed;
    2144                  }
    2145                }
    2146                break;
    2147              }
    2148
    2149            case TagConstants.DIVERGES:
    2150                if (ctxt instanceof RoutineDecl) {
    2151                    RoutineDecl rd = (RoutineDecl)ctxt;
    2152                    if (Utils.isPure(rd)) {
    2153                    ExprModifierPragma emp = (ExprModifierPragma)p;
    2154                    if (emp.expr instanceof LiteralExpr &&
    2155                            ((LiteralExpr)emp.expr).value == Boolean.FALSE) {
    2156                      // OK
    2157                    } else if (p.getStartLoc() == Location.NULL) {
    2158                      // Default clause - ignore it and deal with it during desugaring
    2159                    } else {
    2160                      int locp = Utils.findPurePragma(rd).getStartLoc();
    2161                      int loc = p.getStartLoc();
    2162                      if (loc == Location.NULL) {
    2163                        ErrorSet.error(locp,
    2164                                 "A lightweight specification case for a pure method must have a 'diverges false' clause");
    2165                      } else {
    2166                        ErrorSet.error(loc,
    2167                                 "A pure method may not have a diverges clause",
    2168                                 locp);
    2169                      }
    2170                    }
    2171                  }
    2172                }
    2173                // fall-through
    2174            case TagConstants.ENSURES:
    2175            case TagConstants.ALSO_ENSURES:
    2176            case TagConstants.POSTCONDITION:
    2177            case TagConstants.WHEN:
    2178              {
    2179                ExprModifierPragma emp = (ExprModifierPragma)p;
    2180
    2181                if( ctxt instanceof InitBlock ) {
    2182                  boolean oldIsRESContext = isRESContext;
    2183                  boolean oldIsTwoStateContext = isTwoStateContext;
    2184                  boolean oldIsPrivFieldAccessAllowed = isPrivateFieldAccessAllowed;
    2185                  try {
    2186                    isRESContext = true;
    2187                    isTwoStateContext = true;
    2188                    if (emp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR)
    2189                      emp.expr = checkPredicate(env, emp.expr);
    2190                  } finally {
    2191                    isRESContext = oldIsRESContext;
    2192                    isTwoStateContext = oldIsTwoStateContext;
    2193                    isPrivateFieldAccessAllowed = oldIsPrivFieldAccessAllowed;
    2194                  }
    2195                } else if( ctxt instanceof RoutineDecl ) {
    2196                  RoutineDecl rd = (RoutineDecl)ctxt;
    2197                  escjava.ast.Utils.owningDecl.set(emp,rd);
    2198                  boolean oldIsRESContext = isRESContext;
    2199                  boolean oldIsTwoStateContext = isTwoStateContext;
    2200                  boolean oldIsPrivFieldAccessAllowed = isPrivateFieldAccessAllowed;
    2201                  isRESContext = true;
    2202                  isTwoStateContext = true;
    2203                  // If "rd" is an overridable method, then every private field
    2204                  // mentioned in "emp.expr" must be spec_public.
    2205                  if (rd instanceof MethodDecl && isOverridable((MethodDecl)rd)) {
    2206                    isPrivateFieldAccessAllowed = false;
    2207                  }
    2208                  try {
    2209                    if (emp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR)
    2210                      emp.expr = checkPredicate(env, emp.expr);
    2211                  } finally {
    2212                    isRESContext = oldIsRESContext;
    2213                    isTwoStateContext = oldIsTwoStateContext;
    2214                    isPrivateFieldAccessAllowed = oldIsPrivFieldAccessAllowed;
    2215                  }
    2216                } else {
    2217                  ErrorSet.error(p.getStartLoc(),
    2218                                 TagConstants.toString(tag)
    2219                                 +" annotations can occur only on "
    2220                                 +"initializer, method and constructor declarations");
    2221                }
    2222                break;
    2223              }
    2224
    2225
    2226            case TagConstants.SIGNALS:
    2227              {
    2228                tag = p.originalTag();
    2229                VarExprModifierPragma vemp = (VarExprModifierPragma)p;
    2230
    2231                if( !(ctxt instanceof RoutineDecl ) ) {
    2232                  ErrorSet.error(p.getStartLoc(),
    2233                                 TagConstants.toString(tag)
    2234                                 +" annotations can occur only on "
    2235                                 +"method and constructor declarations");
    2236                } else {
    2237                  RoutineDecl rd = (RoutineDecl)ctxt;
    2238
    2239                  // Resolve type and check that it is a subtype of Throwable
    2240                  // and comparable to some type mentioned in the throws set.
    2241                  env.resolveType(sig,vemp.arg.type);
    2242                  //TypeSig top = Main.options().useThrowable ?
    2243            //                Types.javaLangThrowable() : Types.javaLangException();
    2244                  TypeSig top = Types.javaLangThrowable();
    2245                     // FIXME - JML actually requires that the var be a subtype of
    2246                     // Exception, but the original Esc/Java did not
    2247                  if (!Types.isSubclassOf(vemp.arg.type,top)) {
    2248                    ErrorSet.error(vemp.arg.type.getStartLoc(),
    2249                                   "The type of the " +
    2250                                   TagConstants.toString(tag) +
    2251                                   " argument must be a subtype of " +
    2252                                   Types.printName(top));
    2253                  } else {
    2254                    // "vemp.arg.type" is a subclass of "Throwable", so it
    2255                    // must be a "TypeName" or a "TypeSig"
    2256                    TypeSig ssig;
    2257                    if (vemp.arg.type instanceof TypeSig) {
    2258                      ssig = (TypeSig)vemp.arg.type;
    2259                    } else {
    2260                      ssig = TypeSig.getSig((TypeName)vemp.arg.type);
    2261                    }
    2262                    boolean okay = false;
    2263                    for (int i = 0; i < rd.raises.size(); i++) {
    2264                      TypeName tn = rd.raises.elementAt(i);
    2265                      TypeSig tsig = TypeSig.getSig(tn);
    2266                      if (Types.isSubclassOf(ssig, tsig) ||
    2267                          Types.isSubclassOf(tsig, ssig)) {
    2268                        okay = true;
    2269                        break;
    2270                      }
    2271                    }
    2272                    /* FIXME - what about Error exceptions, must they be mentioned?  */
    2273                    /* FIXME
    2274                       if (!okay) {
    2275                       if (!( (vemp.expr instanceof LiteralExpr) &&
    2276                       ((LiteralExpr)vemp.expr).value.equals(Boolean.FALSE))) {
    2277                       ErrorSet.error(vemp.arg.type.getStartLoc(),
    2278                       "The type of the " +
    2279                       TagConstants.toString(tag) +
    2280                       " argument must be comparable to some type"+
    2281                       " mentioned in the routine's throws set");
    2282                       }
    2283                       }
    2284                    */
    2285                  }
    2286
    2287                  if (tag == TagConstants.SIGNALS_ONLY) {
    2288                      // Check that all Exceptions listed are either in the
    2289                      // throws list or are RuntimeExceptions
    2290
    2291                      // FIXME
    2292
    2293                  }
    2294
    2295                  Env subenv = new EnvForLocals(env, vemp.arg);
    2296                  // FIXME - below we say that this is a twostate context, in which case we should not set this to static???
    2297                  /*
    2298                    if (rd instanceof ConstructorDecl) {
    2299                    subenv = subenv.asStaticContext();
    2300                    }
    2301                  */
    2302
    2303                  // Check the expression to be an appropriate predicate
    2304                  boolean oldIsTwoStateContext = isTwoStateContext;
    2305                  boolean oldIsPrivFieldAccessAllowed = isPrivateFieldAccessAllowed;
    2306                  isTwoStateContext = true;
    2307                  // If "rd" is an overridable method, then every private field
    2308                  // mentioned in "emp.expr" must be spec_public.
    2309                  if (rd instanceof MethodDecl && isOverridable((MethodDecl)rd)) {
    2310                    isPrivateFieldAccessAllowed = false;
    2311                  }
    2312                  try {
    2313                    if (vemp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR)
    2314                      vemp.expr = checkPredicate(subenv, vemp.expr);
    2315                  } finally {
    2316                    isTwoStateContext = oldIsTwoStateContext;
    2317                    isPrivateFieldAccessAllowed = oldIsPrivFieldAccessAllowed;
    2318                  }
    2319                }
    2320                break;
    2321              }
    2322
    2323
    2324            case TagConstants.MONITORED_BY: {
    2325              ExprModifierPragma emp = (ExprModifierPragma)p;
    2326
    2327              if (ctxt.getTag() != TagConstants.FIELDDECL) {
    2328                ErrorSet.error(emp.loc,
    2329                               "The monitored_by annotation can occur only on "+
    2330                               "field declarations");
    2331              } else {
    2332                FieldDecl fd = (FieldDecl)ctxt;
    2333
    2334                int oldAccessibilityLowerBound = accessibilityLowerBound;
    2335                ASTNode oldAccessibilityContext = accessibilityContext;
    2336                accessibilityLowerBound = getAccessibility(fd.modifiers);
    2337                accessibilityContext = fd;
    2338                emp.expr = checkExpr(env, emp.expr, Types.javaLangObject());
    2339                accessibilityLowerBound = oldAccessibilityLowerBound;
    2340                accessibilityContext = oldAccessibilityContext;
    2341              }
    2342              break;
    2343            }
    2344
    2345            case TagConstants.MODIFIESGROUPPRAGMA: {
    2346              ModifiesGroupPragma mg = (ModifiesGroupPragma)p;
    2347              if (ctxt instanceof InitBlock || ctxt instanceof RoutineDecl) {
    2348                CondExprModifierPragmaVec v = mg.items;
    2349                for (int i=0; i<v.size(); ++i) {
    2350                  checkModifierPragma(v.elementAt(i),ctxt,env);
    2351                }
    2352                if (mg.precondition != null)
    2353                  mg.precondition = checkPredicate(env,mg.precondition); // FIXME - pre environment ?
    2354              } else {
    2355                ErrorSet.error(mg.clauseLoc,
    2356                               "A modifies annotation " +
    2357                               "can occur only on " +
    2358                               "method and constructor declarations");
    2359              }
    2360              break;
    2361            }
    2362
    2363            case TagConstants.MODIFIES:
    2364            case TagConstants.ASSIGNABLE:
    2365            case TagConstants.MODIFIABLE:
    2366            case TagConstants.STILL_DEFERRED: {
    2367              CondExprModifierPragma emp = (CondExprModifierPragma)p;
    2368
    2369              if ((ctxt instanceof RoutineDecl ) ) {
    2370                RoutineDecl rd = (RoutineDecl)ctxt;
    2371
    2372                Assert.notFalse(!isSpecDesignatorContext);
    2373                isSpecDesignatorContext = true;
    2374                Env newenv = env;
    2375                /*
    2376                // But we do need to allow the fields of this in the modifies clause, which
    2377                // using the static context does not permit.
    2378                if (rd instanceof ConstructorDecl) {
    2379                // disallow "this" from constructor "modifies" clauses
    2380                newenv = env.asStaticContext();
    2381                }
    2382                */
    2383                emp.expr = checkDesignator(newenv, emp.expr);
    2384                switch (emp.expr.getTag()) {
    2385                case TagConstants.FIELDACCESS: {
    2386                  FieldAccess fa = (FieldAccess)emp.expr;
    2387                  if (fa.decl != null &&
    2388                      (ctxt instanceof MethodDecl) && // FIXME - what about constructors
    2389                      Modifiers.isFinal(fa.decl.modifiers) &&
    2390                      // The array "length" field has already been checked
    2391                      // insuper.checkDesignator().
    2392                      fa.decl != Types.lengthFieldDecl) {
    2393
    2394                    // java.lang.System has fields in, out, err that are special
    2395                    // cases.  Somehow, Java allows them to be final and yet be
    2396                    // modified by public routines.  Instead of a general
    2397                    // mechanism, we just do a special case here.
    2398                    if (fa.decl.parent != Types.javaLangSystem().getTypeDecl())
    2399                      ErrorSet.caution(fa.locId, "a final field is not allowed as " +
    2400                                       "the designator in a modifies clause");
    2401                  }
    2402                  break;
    2403                }
    2404
    2405                case TagConstants.ARRAYREFEXPR:
    2406                case TagConstants.ARRAYRANGEREFEXPR:
    2407                case TagConstants.WILDREFEXPR:
    2408                case TagConstants.EVERYTHINGEXPR:
    2409                case TagConstants.NOTHINGEXPR:
    2410                case TagConstants.NOTSPECIFIEDEXPR:
    2411                  break;
    2412
    2413                default:
    2414                  if (escjava.parser.EscPragmaParser.
    2415                      informalPredicateDecoration.get(emp.expr)==null) {
    2416                    // The expression is not a designator
    2417                    // but we allow an informal predicate
    2418                    if (!Types.isErrorType(getType(emp.expr)))
    2419                      ErrorSet.error(emp.expr.getStartLoc(),
    2420                                     "Not a specification designator expression");
    2421                  } else {
    2422                    emp.expr = null;
    2423                  }
    2424                }
    2425                if (rd instanceof MethodDecl && Utils.isPure(rd) &&
    2426                    emp.expr != null && emp.expr.getTag() != TagConstants.NOTHINGEXPR) {
    2427                  ErrorSet.error(p.getStartLoc(),
    2428                                 "A pure method may not have a modifies clause",
    2429                                 Utils.findPurePragma(rd).getStartLoc());
    2430                }
    2431                if (rd instanceof ConstructorDecl && Utils.isPure(rd) &&
    2432                    emp.expr != null &&
    2433                    !(emp.expr.getTag() == TagConstants.NOTHINGEXPR ||
    2434                      (emp.expr.getTag() == TagConstants.WILDREFEXPR &&
    2435                       (((WildRefExpr)emp.expr).var instanceof ThisExpr) &&
    2436                       ((ThisExpr)((WildRefExpr)emp.expr).var).classPrefix == null)
    2437                      ||
    2438                      ((emp.expr instanceof FieldAccess) &&
    2439                       Types.isSubclassOf(
    2440                                          TypeSig.getSig(rd.parent),
    2441                                          TypeSig.getSig(((FieldAccess)emp.expr).decl.parent)
    2442                                          )
    2443                       ))
    2444                    ) {
    2445                  ErrorSet.error(p.getStartLoc(),
    2446                                 "A pure constructor may not have a modifies clause",
    2447                                 Utils.findPurePragma(rd).getStartLoc());
    2448                }
    2449                isSpecDesignatorContext = false;
    2450                if (emp.cond != null) emp.cond = checkExpr(newenv, emp.cond);
    2451              }
    2452              break;
    2453            }
    2454
    2455            case TagConstants.ALSO:
    2456            case TagConstants.ALSO_REFINE:
    2457            case TagConstants.MODEL_PROGRAM:
    2458            case TagConstants.CODE_CONTRACT:
    2459            case TagConstants.BEHAVIOR:
    2460            case TagConstants.CLOSEPRAGMA:
    2461            case TagConstants.EXAMPLE:
    2462            case TagConstants.EXCEPTIONAL_BEHAVIOR:
    2463            case TagConstants.EXCEPTIONAL_EXAMPLE:
    2464            case TagConstants.FOR_EXAMPLE:
    2465            case TagConstants.IMPLIES_THAT:
    2466            case TagConstants.NORMAL_BEHAVIOR:
    2467            case TagConstants.NORMAL_EXAMPLE:
    2468            case TagConstants.OPENPRAGMA:
    2469              // Desugaring happens before type-checking,
    2470              // This shouldn't happen.
    2471              break;
    2472
    2473            case TagConstants.GHOST:
    2474            case TagConstants.MODEL:
    2475              break;
    2476
    2477            case TagConstants.NESTEDMODIFIERPRAGMA:
    2478              {
    2479                java.util.ArrayList list = ((NestedModifierPragma)p).list;
    2480                java.util.Iterator i = list.iterator();
    2481                while (i.hasNext()) {
    2482                  ModifierPragmaVec mpv = (ModifierPragmaVec)i.next();
    2483                  checkModifierPragmaVec(mpv,ctxt,env);
    2484                }
    2485                break;
    2486              }
    2487
    2488            case TagConstants.PARSEDSPECS:
    2489              {
    2490                escjava.ParsedRoutineSpecs pp = ((ParsedSpecs)p).specs;
    2491                java.util.Iterator i = pp.specs.iterator();
    2492                while (i.hasNext()) {
    2493                  checkModifierPragmaVec((ModifierPragmaVec)i.next(),ctxt,env);
    2494                }
    2495                i = pp.impliesThat.iterator();
    2496                while (i.hasNext()) {
    2497                  checkModifierPragmaVec((ModifierPragmaVec)i.next(),ctxt,env);
    2498                }
    2499                i = pp.examples.iterator();
    2500                while (i.hasNext()) {
    2501                  checkModifierPragmaVec((ModifierPragmaVec)i.next(),ctxt,env);
    2502                }
    2503                /* This duplicates stuff
    2504                // The last element is the ParsedSpecs containing all the
    2505                // clauses etc.
    2506                ModifierPragmaVec mpv = pp.modifiers;
    2507                ModifierPragma last = mpv.elementAt(mpv.size()-1);
    2508                mpv.removeElementAt(mpv.size()-1);
    2509                checkModifierPragmaVec(mpv,ctxt,env);
    2510                mpv.addElement(last);
    2511                */
    2512                break;
    2513              }
    2514
    2515            case TagConstants.MAPS: {
    2516              Identifier fid = ((FieldDecl)ctxt).id;
    2517              MapsExprModifierPragma ep = (MapsExprModifierPragma)p;
    2518              //System.out.println("FOUND " + TagConstants.toString(tag) + " for " + fid + " " + ep.id);
    2519              if (ep.expr != null) ep.expr = checkExpr(env,ep.expr);
    2520              isSpecDesignatorContext = true;
    2521              if (ep.mapsexpr != null) ep.mapsexpr = checkDesignator(env,ep.mapsexpr);
    2522              isSpecDesignatorContext = false;
    2523              Expr e = ep.expr;
    2524              if (e == null || TypeCheck.inst.getType(e) == Types.errorType) {
    2525                // skip
    2526              } else if (e instanceof FieldAccess) {
    2527                FieldAccess fe = (FieldAccess)e; // datagroup
    2528                FieldDecl fd = (FieldDecl)ctxt;  // field with which maps decl is associated
    2529                if (Modifiers.isStatic( fe.decl.modifiers)
    2530                    && !Modifiers.isStatic( fd.modifiers) ){
    2531                  ErrorSet.error(((FieldDecl)ctxt).getStartLoc(),
    2532                         "An instance field may not be added to a static datagroup",
    2533                         fe.decl.getStartLoc());
    2534                } else {
    2535                  Datagroups.add(fd.parent,fe.decl,ep.mapsexpr);
    2536                }
    2537              } else {
    2538                ErrorSet.error(e.getStartLoc(),
    2539                               "Expected a field reference here, found " +
    2540                               e.getClass());
    2541              }
    2542              break;
    2543            }
    2544
    2545            case TagConstants.IN: {
    2546              MapsExprModifierPragma ep = (MapsExprModifierPragma)p;
    2547              if (ep.expr != null) ep.expr = checkExpr(env,ep.expr);
    2548              Expr e = ep.expr;
    2549              if (e == null || TypeCheck.inst.getType(e) == Types.errorType) {
    2550              } else if (e instanceof FieldAccess) {
    2551                FieldAccess fe = (FieldAccess)e;  // datagroup
    2552                FieldDecl fd = (FieldDecl)ctxt;  // field being put in the datagroup
    2553                Expr eva = AmbiguousVariableAccess.make(
    2554                                        SimpleName.make(fd.id,fd.getStartLoc()));
    2555                eva = checkExpr(env,eva);
    2556                if (Modifiers.isStatic( fe.decl.modifiers ) &&
    2557                    !Modifiers.isStatic(fd.modifiers)) {
    2558                  ErrorSet.error(fd.getStartLoc(),
    2559                       "An instance field may not be added to a static datagroup",
    2560                        fe.decl.getStartLoc());
    2561                } else {
    2562                  Datagroups.add(fd.parent,fe.decl,eva);
    2563                }
    2564              } else {
    2565                ErrorSet.error(e.getStartLoc(),
    2566                               "Expected a field reference here, found " +
    2567                               e.getClass());
    2568              }
    2569              break;
    2570            }
    2571
    2572            case TagConstants.READONLY:
    2573            case TagConstants.PEER:
    2574            case TagConstants.REP:
    2575              // FIXME - need to support these
    2576              break;
    2577
    2578            default:
    2579              ErrorSet.error(p.getStartLoc(),
    2580                             "Ignored unexpected " +
    2581                             TagConstants.toString(tag) +
    2582                             " tag");
    2583              break;
    2584            }
    2585        } finally {
    2586          inAnnotation = savedInAnnotation;
    2587        }
    2588        return env;
    2589      }
    2590
    2591      /**
    2592       * @return whether or not <code>md</code> can be overridden in some possible
    2593       * subclass.
    2594       */
    2595
    2596      public static boolean isOverridable(/*@ non_null */ MethodDecl md) {
    2597        return !(Modifiers.isPrivate(md.modifiers) ||
    2598                 Modifiers.isFinal(md.modifiers) ||
    2599                 Modifiers.isFinal(md.parent.modifiers) ||
    2600                 Modifiers.isStatic(md.modifiers));
    2601      }
    2602
    2603      /**
    2604       * @return a value appropriate for assignment to
    2605       * <code>accessibilityLowerBound</code>, given member modifiers.
    2606       */
    2607
    2608      protected int getAccessibility(int modifiers) {
    2609        if (Modifiers.isPrivate(modifiers)) {
    2610          return ACC_LOW_BOUND_Private;
    2611        } else if (Modifiers.isPackage(modifiers)) {
    2612          return ACC_LOW_BOUND_Package;
    2613        } else if (Modifiers.isProtected(modifiers)) {
    2614          return ACC_LOW_BOUND_Protected;
    2615        } else {
    2616          Assert.notFalse(Modifiers.isPublic(modifiers));
    2617          return ACC_LOW_BOUND_Public;
    2618        }
    2619      }
    2620
    2621      protected Env checkStmtPragma(Env e, StmtPragma s) {
    2622        boolean savedInAnnotation = inAnnotation;
    2623        inAnnotation = true;        // Must be reset before we exit!
    2624        boolean savedTwoStateContext = isTwoStateContext;
    2625        isTwoStateContext = true;
    2626        try {
    2627          int tag = s.getTag();
    2628          switch(tag) {
    2629          case TagConstants.UNREACHABLE:
    2630            break;
    2631
    2632          case TagConstants.SETSTMTPRAGMA: {
    2633            SetStmtPragma set = (SetStmtPragma)s;
    2634            set.target = checkExpr(e, set.target);
    2635            set.value = checkExpr(e, set.value);
    2636            checkBinaryExpr(TagConstants.ASSIGN, set.target,
    2637                            set.value, set.locOp);
    2638            Expr t = set.target;
    2639            int nonGhostLoc = isGhost(t);
    2640            if (nonGhostLoc != 0) {
    2641              ErrorSet.error(s.getStartLoc(),"May use set only with assignment targets that are declared ghost",nonGhostLoc);
    2642            }
    2643            /*
    2644              if (t instanceof FieldAccess &&
    2645              ((FieldAccess)t).decl == Types.lengthFieldDecl) {
    2646              ErrorSet.error(s.getStartLoc(),"The length field of an array may not be set");
    2647              }
    2648            */
    2649            break;
    2650          }
    2651
    2652          case TagConstants.HENCE_BY:
    2653          case TagConstants.ASSUME:
    2654          case TagConstants.ASSERT:
    2655            {
    2656              ExprStmtPragma es = (ExprStmtPragma)s;
    2657              es.expr = checkPredicate(e, es.expr);
    2658              if (es.label != null)
    2659                es.label = checkExpr(e, es.label);
    2660              break;
    2661            }
    2662
    2663          case TagConstants.LOOP_INVARIANT:
    2664          case TagConstants.MAINTAINING:
    2665            {
    2666              ExprStmtPragma lis = (ExprStmtPragma)s;
    2667              loopInvariants.addElement(lis);
    2668              break;
    2669            }
    2670
    2671          case TagConstants.DECREASES:
    2672          case TagConstants.DECREASING:
    2673            {
    2674              ExprStmtPragma lis = (ExprStmtPragma)s;
    2675              loopDecreases.addElement(lis);
    2676              break;
    2677            }
    2678
    2679          case TagConstants.LOOP_PREDICATE:
    2680            {
    2681              ExprStmtPragma lis = (ExprStmtPragma)s;
    2682              loopPredicates.addElement(lis);
    2683              break;
    2684            }
    2685
    2686          case TagConstants.SKOLEMCONSTANTPRAGMA:
    2687            {
    2688              SkolemConstantPragma p = (SkolemConstantPragma)s;
    2689              skolemConstants.append(p.decls);
    2690              break;
    2691            }
    2692
    2693          default:
    2694            Assert.fail("Unexpected tag " + tag +" "+s +
    2695                        " " + Location.toString(s.getStartLoc()));
    2696          }
    2697        } finally {
    2698          inAnnotation = savedInAnnotation;
    2699          isTwoStateContext = savedTwoStateContext;
    2700        }
    2701        return e;
    2702      }
    2703
    2704
    2705      // Utility routines
    2706
    2707      /**
    2708       * Copy the Type associated with an expression by the typechecking pass to
    2709       * another Expr.  This is used by Substitute to ensure it returns an Expr of the
    2710       * same Type.
    2711       */
    2712      public static void copyType(VarInit from, VarInit to) {
    2713        Type t = getTypeOrNull(from);
    2714        if (t != null)
    2715          setType(to, t);
    2716      }
    2717
    2718      /**
    2719       * @return a set of *all* the methods a given method overrides. This includes
    2720       * transitivity.
    2721       */
    2722      //@ requires md != null;
    2723      //@ ensures \result != null;
    2724      //@ ensures \result.elementType == \type(MethodDecl);
    2725      public static Set getAllOverrides(MethodDecl md) {
    2726        Set direct = javafe.tc.PrepTypeDeclaration.inst.getOverrides(md.parent, md);
    2727        Set result = new Set();
    2728
    2729        Enumeration e = direct.elements();
    2730        while (e.hasMoreElements()) {
    2731          MethodDecl directMD = (MethodDecl)(e.nextElement());
    2732          result.add(directMD);
    2733          result.addEnumeration(getAllOverrides(directMD).elements());
    2734        }
    2735
    2736        return result;
    2737      }
    2738
    2739      public static javafe.util.Set getDirectOverrides(MethodDecl md) {
    2740        return javafe.tc.PrepTypeDeclaration.inst.getOverrides(md.parent, md);
    2741      }
    2742
    2743      /**
    2744       * @return If <code>md</code> is a method that overrides a method in a
    2745       * superclass, the overridden method is returned.  Otherwise, if <code>md</code>
    2746       * overrides a method in an interface, such a method is returned.  Otherwise,
    2747       * <code>null</code> is returned.
    2748       */
    2749
    2750      public static MethodDecl getSuperClassOverride(MethodDecl md) {
    2751        MethodDecl classOverride = null;
    2752        MethodDecl interfaceOverride = null;
    2753        Set direct = javafe.tc.PrepTypeDeclaration.inst.getOverrides(md.parent, md);
    2754        Enumeration e = direct.elements();
    2755        while (e.hasMoreElements()) {
    2756          MethodDecl directMD = (MethodDecl)(e.nextElement());
    2757          if (directMD.parent instanceof ClassDecl) {
    2758            if (classOverride == null) {
    2759              classOverride = directMD;
    2760            } else {
    2761              Assert.fail("we think this can no longer happen!");
    2762              // This suggests that the method is inherited from TWO classes!
    2763              // This can actually happen, if the method is one that is
    2764              // declared in Object, because every interface has the methods of
    2765              // Object.  In this case, pick the method override that does not
    2766              // reside in Object.
    2767              Type javaLangObject = Types.javaLangObject();
    2768              Type t0 = TypeSig.getSig(classOverride.parent);
    2769              Type t1 = TypeSig.getSig(directMD.parent);
    2770              Assert.notFalse(Types.isSameType(t0, javaLangObject) ||
    2771                              Types.isSameType(t1, javaLangObject));
    2772              Assert.notFalse(!Types.isSameType(t0, javaLangObject) ||
    2773                              !Types.isSameType(t1, javaLangObject));
    2774              if (!Types.isSameType(t1, javaLangObject)) {
    2775                classOverride = directMD;
    2776              }
    2777            }
    2778          } else {
    2779            interfaceOverride = directMD;
    2780          }
    2781        }
    2782        if (classOverride != null) {
    2783          return classOverride;
    2784        } else {
    2785          return interfaceOverride;
    2786        }
    2787      }
    2788
    2789      /**
    2790       * @return whether or not <code>rd</code> is a method override declaration, that
    2791       * is, whether or not <code>rd</code> overrides a method declared in a superclass
    2792       * or superinterface.
    2793       */
    2794
    2795      public static boolean isMethodOverride(RoutineDecl rd) {
    2796        return getOverrideStatus(rd) != MSTATUS_NEW_ROUTINE;
    2797      }
    2798
    2799      static public final int MSTATUS_NEW_ROUTINE = 0;
    2800      static public final int MSTATUS_CLASS_NEW_METHOD = 1;
    2801      static public final int MSTATUS_OVERRIDE = 2;
    2802
    2803      /**
    2804       * @return <code>MSTATUS_NEW_ROUTINE</code> if <code>rd</code> is a routine that
    2805       * doesn't override any other method.  This includes the case where
    2806       * <code>rd</code> is a constructor or a static method.
    2807       *
    2808       * <p> Returns <code>MSTATUS_CLASS_NEW_METHOD</code> if <code>rd</code> is a
    2809       * method declared in a class, doesn't override any method in any superclass, but
    2810       * overrides a method in an interface.
    2811       *
    2812       * <p> Otherwise, returns <code>MSTATUS_OVERRIDE</code>.
    2813       */
    2814
    2815      /*@ ensures \result == MSTATUS_NEW_ROUTINE ||
    2816        @         \result == MSTATUS_CLASS_NEW_METHOD ||
    2817        @         \result == MSTATUS_OVERRIDE;
    2818      */
    2819      public static int getOverrideStatus(/*@ non_null */ RoutineDecl rd) {
    2820        if (!(rd instanceof MethodDecl) || Modifiers.isStatic(rd.modifiers)) {
    2821          return MSTATUS_NEW_ROUTINE;
    2822        }
    2823        MethodDecl md = (MethodDecl)rd;
    2824
    2825        Set direct = javafe.tc.PrepTypeDeclaration.inst.getOverrides(md.parent, md);
    2826        if (direct.size() == 0) {
    2827          return MSTATUS_NEW_ROUTINE;
    2828        }
    2829        if (!(md.parent instanceof ClassDecl)) {
    2830          return MSTATUS_OVERRIDE;
    2831        }
    2832
    2833        Enumeration e = direct.elements();
    2834        while (e.hasMoreElements()) {
    2835          MethodDecl directMD = (MethodDecl)(e.nextElement());
    2836          if (directMD.parent instanceof ClassDecl) {
    2837            return MSTATUS_OVERRIDE;
    2838          }
    2839        }
    2840        return MSTATUS_CLASS_NEW_METHOD;
    2841      }
    2842
    2843      /**
    2844       * @return null if method md is allowed to declare its jth (counting from 0)
    2845       * formal parameter as non_null.  That is the case if the method does not
    2846       * override anything, or if in everything that it does override that parameter is
    2847       * declared non_null.  Otherwise returns the MethodDecl corresponding to the
    2848       * overridden method with which the argument rd is in conflict.
    2849       */
    2850      static public MethodDecl getSuperNonNullStatus(RoutineDecl rd, int j) {
    2851        if (!(rd instanceof MethodDecl) || Modifiers.isStatic(rd.modifiers)) {
    2852          return null;
    2853        }
    2854        MethodDecl md = (MethodDecl)rd;
    2855
    2856        Set direct = javafe.tc.PrepTypeDeclaration.inst.getOverrides(md.parent, md);
    2857        if (direct.size() == 0) {
    2858          return null;
    2859        }
    2860        return getSuperNonNullStatus(rd,j,direct);
    2861      }
    2862
    2863      static public MethodDecl getSuperNonNullStatus(RoutineDecl rd, int j, Set directOverrides) {
    2864        Enumeration e = directOverrides.elements();
    2865        while (e.hasMoreElements()) {
    2866          MethodDecl directMD = (MethodDecl)(e.nextElement());
    2867          FormalParaDecl f = directMD.args.elementAt(j);
    2868          if (Utils.findModifierPragma(f,TagConstants.NON_NULL) == null)
    2869            return directMD;
    2870        }
    2871        return null;
    2872      }
    2873
    2874      /** Returns non-zero if the expression is a ghost expression - that is, it
    2875          would not exist if all ghost declarations were removed.  Otherwise
    2876          returns a Location value of a relevant non-ghost declaration.
    2877      */
    2878      public int isGhost(Expr t) {
    2879        if (t instanceof ArrayRefExpr) {
    2880          t = ((ArrayRefExpr)t).array;
    2881        }
    2882        if (t instanceof FieldAccess) {
    2883          FieldAccess fa = (FieldAccess)t;
    2884          if (fa.decl == null || GhostEnv.isGhostField(fa.decl))
    2885            return 0;
    2886          int gl = isGhost(fa.od);
    2887          if (gl == 0) return 0;
    2888          if (gl == -1) return fa.decl.getStartLoc();
    2889          return gl;
    2890        } else if (t instanceof VariableAccess) {
    2891          VariableAccess va = (VariableAccess)t;
    2892          GenericVarDecl gd = va.decl;
    2893          if ( Utils.findModifierPragma(
    2894                                        gd.pmodifiers,TagConstants.GHOST) == null)
    2895            return gd.getStartLoc();
    2896        } else if (t instanceof ParenExpr) {
    2897          return isGhost( ((ParenExpr)t).expr );
    2898        } else if (t instanceof CastExpr) {
    2899          return isGhost( ((CastExpr)t).expr );
    2900        }
    2901        return 0;
    2902        // FIXME - need some test that the expression in advance of
    2903        // a . in a field reference or the [] in an array reference
    2904        // only designates ghost fields/variables
    2905        // e.g. what about method calls, operator expressions?
    2906
    2907      }
    2908
    2909      public int isGhost(ObjectDesignator od) {
    2910        if (od instanceof ExprObjectDesignator) {
    2911          Expr e = ((ExprObjectDesignator)od).expr;
    2912          if (e == null || e instanceof ThisExpr) return -1;
    2913          return isGhost(e);
    2914        }
    2915        return -1; // OK for TypeObjectDesignator and SuperObjectDesignator
    2916      }
    2917
    2918      protected boolean assignmentConvertable(Expr e, Type t) {
    2919        if (super.assignmentConvertable(e,t)) return true;
    2920        return Types.isTypeType(t) && Types.isTypeType(getType(e));
    2921      }
    2922
    2923    } // end of class FlowInsensitiveChecks
    2924
    2925    /*
    2926     * Local Variables:
    2927     * Mode: Java
    2928     * fill-column: 85
    2929     * End:
    2930     */