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     */