    001    // This class is generated as part of the 2003 Revision of the ESC Tools
    002    // Author: David Cok
    003
    004    package escjava;
    005
    006    import java.util.ArrayList;
    007    import java.util.Iterator;
    008
    009    import javafe.ast.ASTNode;
    010    import javafe.ast.BinaryExpr;
    011    import javafe.ast.CompilationUnit;
    012    import javafe.ast.ConstructorDecl;
    013    import javafe.ast.Expr;
    014    import javafe.ast.ExprObjectDesignator;
    015    import javafe.ast.ExprVec;
    016    import javafe.ast.FormalParaDecl;
    017    import javafe.ast.FormalParaDeclVec;
    018    import javafe.ast.Identifier;
    019    import javafe.ast.InstanceOfExpr;
    020    import javafe.ast.InterfaceDecl;
    021    import javafe.ast.LexicalPragma;
    022    import javafe.ast.LiteralExpr;
    023    import javafe.ast.MethodDecl;
    024    import javafe.ast.MethodInvocation;
    025    import javafe.ast.ModifierPragma;
    026    import javafe.ast.ModifierPragmaVec;
    027    import javafe.ast.NewInstanceExpr;
    028    import javafe.ast.PrettyPrint;
    029    import javafe.ast.RoutineDecl;
    030    import javafe.ast.ThisExpr;
    031    import javafe.ast.Type;
    032    import javafe.ast.TypeName;
    033    import javafe.ast.TypeNameVec;
    034    import javafe.ast.TypeDecl;
    035    import javafe.ast.TypeDeclElem;
    036    import javafe.ast.TypeDeclElemVec;
    037    import javafe.ast.TypeDeclVec;
    038    import javafe.ast.VariableAccess;
    039    import javafe.tc.TypeSig;
    040    import javafe.tc.Types;
    041    import javafe.util.ErrorSet;
    042    import javafe.util.Location;
    043    import escjava.ast.CondExprModifierPragma;
    044    import escjava.ast.EscPrettyPrint;
    045    import escjava.ast.EverythingExpr;
    046    import escjava.ast.ExprModifierPragma;
    047    import escjava.ast.GenericVarDeclVec;
    048    import escjava.ast.ImportPragma;
    049    import escjava.ast.LabelExpr;
    050    import escjava.ast.ModelConstructorDeclPragma;
    051    import escjava.ast.ModelMethodDeclPragma;
    052    import escjava.ast.ModelTypePragma;
    053    import escjava.ast.Modifiers;
    054    import escjava.ast.ModifiesGroupPragma;
    055    import escjava.ast.NaryExpr;
    056    import escjava.ast.NestedModifierPragma;
    057    import escjava.ast.NothingExpr;
    058    import escjava.ast.ParsedSpecs;
    059    import escjava.ast.QuantifiedExpr;
    060    import escjava.ast.ResExpr;
    061    import escjava.ast.SimpleModifierPragma;
    062    import escjava.ast.TagConstants;
    063    import escjava.ast.Utils;
    064    import escjava.ast.VarDeclModifierPragma;
    065    import escjava.ast.VarExprModifierPragma;
    066    import escjava.ast.WildRefExpr;
    067    import escjava.tc.FlowInsensitiveChecks;
    068
    069    /**
    070     * This class handles the desugaring of annotations.
    071     *
    072     */
    073    public class AnnotationHandler {
    074
    075      public AnnotationHandler() {}
    076
    077      protected TypeDecl td = null;
    078
    079      /**
    080       * This must be called on a compilation unit to get the model imports listed,
    081       * so that type names used in annotations can be found, and to get model
    082       * methods put into the class's signature. It is called as part of
    083       * EscSrcReader, a subclass of SrcReader, defined in EscTypeReader.
    084       */
    085      public void handlePragmas(CompilationUnit cu) {
    086        if (cu == null) return;
    087        // move any model imports into the list of imports
    088        for (int i = 0; i < cu.lexicalPragmas.size(); ++i) {
    089          LexicalPragma p = cu.lexicalPragmas.elementAt(i);
    090          if (p instanceof ImportPragma)
    091              cu.imports.addElement(((ImportPragma)p).decl);
    092        }
    093
    094        TypeDeclVec elems = cu.elems;
    095        for (int i = 0; i < elems.size(); ++i) {
    096          TypeDecl td = elems.elementAt(i);
    097          handleTypeDecl(td);
    098        }
    099      }
    100
    101      /**
    102       * After parsing, but before type checking, we need to convert model methods
    103       * to regular methods, so that names are resolved correctly; also need to set
    104       * ACC_PURE bits correctly in all classes so that later checks get done
    105       * correctly.
    106       */
    107      // FIXME - possibly should put these in GhostEnv??
    108      public void handleTypeDecl(TypeDecl td) {
    109        handlePragmas(td);
    110        for (int j = 0; j < td.elems.size(); ++j) {
    111          TypeDeclElem tde = td.elems.elementAt(j);
    112          // Handle nested types
    113          if (tde instanceof TypeDecl) {
    114            handleTypeDecl((TypeDecl)tde);
    115          }
    116          // move any model methods into the list of methods
    117          if (tde instanceof ModelMethodDeclPragma) {
    118            handlePragmas(tde);
    119            ModelMethodDeclPragma mmp = (ModelMethodDeclPragma)tde;
    120            td.elems.setElementAt(((ModelMethodDeclPragma)tde).decl, j);
    121          } else if (tde instanceof ModelConstructorDeclPragma) {
    122            handlePragmas(tde);
    123            ModelConstructorDeclPragma mmp = (ModelConstructorDeclPragma)tde;
    124            if (mmp.id == null) {
    125              // An error reported already - improper name cf. EscPragmaParser
    126            } else if (mmp.id.id != td.id) {
    127              ErrorSet
    128                  .error(
    129                      mmp.id.getStartLoc(),
    130                      "A constructor-like declaration has an id which is not the same as the id of the enclosing type: "
    131                          + mmp.id.id + " vs. " + td.id, td.locId);
    132            } else {
    133              td.elems.setElementAt(((ModelConstructorDeclPragma)tde).decl, j);
    134            }
    135          } else if (tde instanceof ModelTypePragma) {
    136            handlePragmas(tde);
    137            ModelTypePragma tdp = (ModelTypePragma)tde;
    138            td.elems.setElementAt(tdp.decl, j);
    139          }
    140          // handle PURE pragmas
    141          if (tde instanceof MethodDecl || tde instanceof ConstructorDecl) {
    142            handlePragmas(tde);
    143          }
    144        }
    145      }
    146
    147      public void handlePragmas(TypeDeclElem tde) {}
    148
    149      //-----------------------------------------------------------------------
    150      /*
    151       * public void process(TypeDecl td) { this.td = td;
    152       *
    153       * for (int i=0; i <td.elems.size(); ++i) { TypeDeclElem tde =
    154       * td.elems.elementAt(i); process(tde); } }
    155       */
    156
    157      public void process(TypeDeclElem tde) {
    158        int tag = tde.getTag();
    159        switch (tag) {
    160          // What about initially, monitored_by, readable_if clauses ??? FIXME
    161          // What about nested classes ??? FIXME
    162          // What about redundant clauses ??? FIXME
    163
    164          case TagConstants.CONSTRUCTORDECL:
    165          case TagConstants.METHODDECL:
    166            process((RoutineDecl)tde);
    167            break;
    168
    169          case TagConstants.FIELDDECL:
    170            break;
    171
    172          case TagConstants.GHOSTDECLPRAGMA:
    173          case TagConstants.MODELDECLPRAGMA:
    174          case TagConstants.INVARIANT:
    175          case TagConstants.INVARIANT_REDUNDANTLY:
    176          case TagConstants.CONSTRAINT:
    177            Context c = new Context();
    178            c.expr = null; // ((TypeDeclElemPragma)tde).expr;
    179            (new CheckPurity()).visitNode((ASTNode)tde, c);
    180            break;
    181
    182          case TagConstants.REPRESENTS:
    183          case TagConstants.AXIOM:
    184            (new CheckPurity()).visitNode((ASTNode)tde, null);
    185            break;
    186
    187          case TagConstants.DEPENDS:
    188          default:
    189        //System.out.println("TAG " + tag + " " + TagConstants.toString(tag) + " "
    190        // + tde.getClass() );
    191        }
    192
    193      }
    194
    195      protected void process(RoutineDecl tde) {
    196        ModifierPragmaVec pmodifiers = tde.pmodifiers;
    197        //System.out.println(" Mods " + Modifiers.toString(tde.modifiers));
    198        if (pmodifiers != null) {
    199          for (int i = 0; i < pmodifiers.size(); ++i) {
    200            ModifierPragma mp = pmodifiers.elementAt(i);
    201            (new CheckPurity()).visitNode((ASTNode)mp, null);
    202          }
    203        }
    204      }
    205
    206      //-----------------------------------------------------------------------
    207      // Desugaring is done as a last stage of type-checking. The desugar
    208      // methods below may presume that all expressions are type-checked.
    209      // As a result, any constructed expressions must have type information
    210      // inserted.
    211
    212      public void desugar(TypeDecl td) {
    213        int n = td.elems.size();
    214        for (int i = 0; i < n; ++i) {
    215          TypeDeclElem tde = td.elems.elementAt(i);
    216          if (tde instanceof RoutineDecl) desugar((RoutineDecl)tde);
    217          if (tde instanceof TypeDecl) desugar((TypeDecl)tde);
    218          // FIXME - what about model routines and types
    219        }
    220      }
    221
    222      public void desugar(RoutineDecl tde) {
    223        if ((tde.modifiers & Modifiers.ACC_DESUGARED) != 0) return;
    224
    225        // Now desugar this routine itself
    226
    227        ModifierPragmaVec pmodifiers = tde.pmodifiers;
    228        Identifier id = tde instanceof MethodDecl ? ((MethodDecl)tde).id : tde
    229            .getParent().id;
    230        //  javafe.util.Info.out("Desugaring specifications for " + tde.parent.id +
    231        // "." + id);
    232
    233        if (Main.options().desugaredSpecs) {
    234          System.out.println("Desugaring specifications for " + tde.parent.id + "."
    235              + id);
    236          printSpecs(tde);
    237          System.out.println("\n");
    238        }
    239
    240        try { // Just for safety's sake
    241          tde.pmodifiers = desugarAnnotations(pmodifiers, tde);
    242        } catch (Exception e) {
    243          tde.pmodifiers = ModifierPragmaVec.make();
    244          ErrorSet.error(tde.getStartLoc(),
    245              "Internal error while desugaring annotations: " + e);
    246          e.printStackTrace();
    247        }
    248        tde.modifiers |= Modifiers.ACC_DESUGARED;
    249
    250        if (Main.options().desugaredSpecs) {
    251          System.out.println("Desugared specifications for " + tde.parent.id + "."
    252              + id);
    253          printSpecs(tde);
    254        }
    255      }
    256
    257      static public void printSpecs(RoutineDecl tde) {
    258        if (tde.pmodifiers != null)
    259            for (int i = 0; i < tde.pmodifiers.size(); ++i) {
    260              ModifierPragma mp = tde.pmodifiers.elementAt(i);
    261              printSpec(mp);
    262            }
    263      }
    264
    265      static public void printSpec(ModifierPragma mp) {
    266        if (mp instanceof ModifiesGroupPragma) {
    267          EscPrettyPrint.inst.print(System.out, 0, (ModifiesGroupPragma)mp);
    268          System.out.println("");
    269          return;
    270        }
    271        System.out.print("   " + escjava.ast.TagConstants.toString(mp.getTag())
    272            + " ");
    273        if (mp instanceof ExprModifierPragma) {
    274          ExprModifierPragma mpe = (ExprModifierPragma)mp;
    275          print(mpe.expr);
    276        } else if (mp instanceof CondExprModifierPragma) {
    277          CondExprModifierPragma mpe = (CondExprModifierPragma)mp;
    278          print(mpe.expr);
    279          if (mpe.cond != null) {
    280            System.out.print(" if ");
    281            print(mpe.cond);
    282          }
    283        } else if (mp instanceof VarExprModifierPragma) {
    284          VarExprModifierPragma mpe = (VarExprModifierPragma)mp;
    285          System.out.print("("
    286              + Types.toClassTypeSig(mpe.arg.type).getExternalName()
    287              + (mpe.arg.id == TagConstants.ExsuresIdnName ? "" : " "
    288                  + mpe.arg.id.toString()) + ")");
    289          print(mpe.expr);
    290        } else {
    291          EscPrettyPrint.inst.print(System.out, 0, mp);
    292        }
    293        System.out.println("");
    294      }
    295
    296      protected ModifierPragmaVec desugarAnnotations(ModifierPragmaVec pm,
    297          RoutineDecl tde) {
    298        if (pm == null) {
    299          pm = ModifierPragmaVec.make();
    300        }
    301
    302        ModifierPragmaVec newpm = ModifierPragmaVec.make();
    303
    304        boolean isConstructor = tde instanceof ConstructorDecl;
    305
    306        // Get non_null specs
    307        ModifierPragmaVec nonnullBehavior = getNonNull(tde);
    308
    309        javafe.util.Set overrideSet = null;
    310        if (!isConstructor)
    311            overrideSet = FlowInsensitiveChecks.getDirectOverrides((MethodDecl)tde);
    312
    313        boolean overrides = !isConstructor && !overrideSet.isEmpty();
    314
    315        boolean defaultSpecs = false;
    316        if (!overrides && nonnullBehavior.size() == 0) {
    317          // Add a default 'requires true' clause if there are no
    318          // specs at all and the routine is not overriding anything
    319          boolean doit = pm.size() == 0;
    320          if (!doit) {
    321            // Need to determine if there are any clause specs
    322            doit = true;
    323            int k = pm.size();
    324            while ((--k) >= 0) {
    325              ModifierPragma mpp = pm.elementAt(k);
    326              if (!(mpp instanceof ParsedSpecs)) {
    327                break;
    328              }
    329              if (((ParsedSpecs)mpp).specs.specs.size() != 0) {
    330                doit = false;
    331                break;
    332              }
    333            }
    334            // FIXME - why do we get ExprModifierPragmas here (e.g. test8)
    335            //System.out.println("QT " + mpp.getClass());
    336          }
    337          if (doit) {
    338            defaultSpecs = true;
    339            ExprModifierPragma e = ExprModifierPragma.make(TagConstants.REQUIRES,
    340                T, tde.getStartLoc());
    341            newpm.addElement(e);
    342            newpm.addElement(defaultModifies(tde.getStartLoc(), T, tde));
    343            newpm.addElement(defaultSignalsOnly(tde, T));
    344          }
    345        }
    346
    347        RoutineDecl previousDecl = null;
    348        int pos = 0;
    349        while (pos < pm.size()) {
    350          ModifierPragma p = pm.elementAt(pos++);
    351          if (p.getTag() == TagConstants.PARSEDSPECS) {
    352            ParsedSpecs ps = (ParsedSpecs)p;
    353            previousDecl = ps.decl;
    354            if (overrides && ps.specs.initialAlso == null
    355                && ps.specs.specs.size() != 0) {
    356              ErrorSet
    357                  .caution(
    358                      ps.getStartLoc(),
    359                      "JML requires a specification to begin with 'also' when the method overrides other methods",
    360                      ((MethodDecl)overrideSet.elements().nextElement()).locType);
    361            }
    362            if (!overrides && ps.specs.initialAlso != null) {
    363              if (!(tde.parent instanceof InterfaceDecl)) {
    364                ErrorSet
    365                    .caution(ps.specs.initialAlso.getStartLoc(),
    366                        "No initial also expected since there are no overridden or refined methods");
    367              } else {
    368                MethodDecl omd = Types.javaLangObject().hasMethod(
    369                    ((MethodDecl)tde).id, tde.argTypes());
    370                if (omd == null || Modifiers.isPrivate(omd.modifiers))
    371                    ErrorSet
    372                        .caution(ps.specs.initialAlso.getStartLoc(),
    373                            "No initial also expected since there are no overridden or refined methods");
    374              }
    375            }
    376            break;
    377          }
    378        }
    379        while (pos < pm.size()) {
    380          ModifierPragma p = pm.elementAt(pos++);
    381          if (p.getTag() == TagConstants.PARSEDSPECS) {
    382            ParsedSpecs ps = (ParsedSpecs)p;
    383            if (ps.specs.initialAlso == null && ps.specs.specs.size() != 0) {
    384              ErrorSet
    385                  .caution(
    386                      ps.getStartLoc(),
    387                      "JML requires a specification to begin with 'also' when the declaration refines a previous declaration",
    388                      previousDecl.locId);
    389            }
    390            previousDecl = ps.decl;
    391          }
    392        }
    393
    394        ParsedRoutineSpecs accumulatedSpecs = new ParsedRoutineSpecs();
    395
    396        pos = 0;
    397        while (pos < pm.size()) {
    398          ModifierPragma p = pm.elementAt(pos++);
    399          if (p.getTag() == TagConstants.PARSEDSPECS) {
    400            ParsedRoutineSpecs ps = ((ParsedSpecs)p).specs;
    401            ParsedRoutineSpecs newps = new ParsedRoutineSpecs();
    402            deNest(ps.specs, nonnullBehavior, newps.specs);
    403            deNest(ps.impliesThat, nonnullBehavior, newps.impliesThat);
    404            deNest(ps.examples, nonnullBehavior, newps.examples);
    405            accumulatedSpecs.specs.addAll(newps.specs);
    406            accumulatedSpecs.impliesThat.addAll(newps.impliesThat);
    407            accumulatedSpecs.examples.addAll(newps.examples);
    408          } else {
    409            newpm.addElement(p);
    410          }
    411        }
    412
    413
    414        ModifierPragmaVec r = desugar(accumulatedSpecs.specs, tde);
    415        // accumulatedSpecs.impliesThat = desugar(accumulatedSpecs.impliesThat);
    416        // accumulatedSpecs.examples = desugar(accumulatedSpecs.examples); // FIXME
    417        // - not doing this because we are not doing anything with the result.
    418        newpm.append(r);
    419        if (defaultSpecs && (tde instanceof ConstructorDecl) && tde.implicit) {
    420          TypeSig td = TypeSig.getSig(tde.parent);
    421          TypeSig tds = td.superClass();
    422          if (tds != null && tde.pmodifiers != null && tde.pmodifiers.size() > 0)
    423              try {
    424                ConstructorDecl cd = tds.lookupConstructor(new Type[0], td);
    425                desugar(cd);
    426                // Only remove previous elements after successfully finding
    427                // a parent constructor
    428                newpm.removeAllElements();
    429                ModifierPragmaVec mp = cd.pmodifiers;
    430                for (int i = 0; i < mp.size(); ++i) {
    431                  ModifierPragma m = mp.elementAt(i);
    432                  int t = m.getTag();
    433                  if (t == TagConstants.REQUIRES || t == TagConstants.PRECONDITION
    434                      || t == TagConstants.MODIFIESGROUPPRAGMA
    435                      || t == TagConstants.MODIFIES || t == TagConstants.ASSIGNABLE) {
    436                    newpm.addElement(m);
    437                  }
    438                }
    439              } catch (Exception e) {
    440                // Purposely ignore this
    441              }
    442        }
    443        checkSignalsOnly(newpm,tde);
    444        return newpm;
    445      }
    446
    447      public void checkSignalsOnly(ModifierPragmaVec mpv, RoutineDecl tde) {
    448        Utils.exceptionDecoration.set(tde,new Integer(tde.raises.size()));
    449        int throwsLoc = tde.locThrowsKeyword;
    450        if (throwsLoc == Location.NULL) throwsLoc = tde.getStartLoc();
    451        for (int i=0; i<mpv.size(); i++) {
    452            ModifierPragma m = mpv.elementAt(i);
    453            int tag = m.originalTag();
    454            if (tag == TagConstants.SIGNALS_ONLY) {
    455                TypeNameVec tv = tde.raises;
    456                if (tv.size() == 0) tde.raises = tv = TypeNameVec.make();
    457                Expr e = ((VarExprModifierPragma)m).expr;
    458                checkMaybeAdd(e,tv,throwsLoc);
    459            }
    460        }
    461      }
    462
    463      private void checkMaybeAdd(Expr e, TypeNameVec tv, int locThrows) {
    464        int tag = e.getTag();
    465        if (tag == TagConstants.OR) {
    466            checkMaybeAdd( ((BinaryExpr)e).left, tv, locThrows);
    467            checkMaybeAdd( ((BinaryExpr)e).right, tv, locThrows);
    468        } else if (tag == TagConstants.INSTANCEOFEXPR) {
    469            Type t = ((InstanceOfExpr)e).type;
    470            TypeSig ts = Types.toClassTypeSig(t);
    471            boolean found = false;
    472            for (int i=0; i<tv.size(); ++i) {
    473                TypeSig tts = TypeSig.getSig(tv.elementAt(i));
    474                if (!ts.isSubtypeOf(tts)) continue;
    475                found = true;
    476                break;
    477            }
    478            if (!found) {
    479                // NOTE: The original Esc/java may have prefered that we warn about
    480                // every exception in a signals_only clause that was not listed
    481                // in the throws clause.  Instead, we silently add types that are
    482                // subtypes of RuntimeException or Error.
    483                boolean b = Main.options().useThrowable;
    484                if (b && !ts.isSubtypeOf(Types.javaLangRuntimeException()) &&
    485                    !ts.isSubtypeOf(Types.javaLangError()) &&
    486                    !Types.isSameType(ts,Types.javaLangThrowable())) {
    487                  ErrorSet.error(t.getStartLoc(),
    488                    "The signals_only clause may not contain an exception type " +
    489                    Types.printName(t) +
    490                    " that is not a subtype of either RuntimeException, Error or " +
    491                    "a type in the routine's throws clause",
    492                    locThrows);
    493                } else if (!b &&
    494                     !ts.isSubtypeOf(Types.javaLangRuntimeException()) ) {
    495                  ErrorSet.error(t.getStartLoc(),
    496                    "The signals_only clause may not contain an exception type " +
    497                    Types.printName(t) +
    498                    " that is not a subtype of either RuntimeException or " +
    499                    "a type in the routine's throws clause",
    500                    locThrows);
    501                } else {
    502                  tv.addElement((TypeName)t);
    503                }
    504            }
    505        } else if (tag == TagConstants.BOOLEANLIT) {
    506            // skip
    507        } else if (tag == TagConstants.IMPLIES) {
    508            // left side is the precondition
    509            checkMaybeAdd( ((BinaryExpr)e).right, tv, locThrows);
    510        } else {
    511            System.out.println("INTERNAL ERROR " + TagConstants.toString(tag));
    512        }
    513      }
    514
    515      // NOTE: We are doing desugaring after typechecking, so we need to
    516      // be sure to annotate any created expressions with types.
    517      // (If expressions are created before typechecking they must not be
    518      // annotated with types, so that typechecking happens properly).
    519
    520      public ModifierPragmaVec getNonNull(RoutineDecl rd) {
    521        ModifierPragmaVec result = ModifierPragmaVec.make(2);
    522        FormalParaDeclVec args = rd.args;
    523
    524        // Check that non_null on parameters is allowed
    525        if (rd instanceof MethodDecl) {
    526          MethodDecl md = (MethodDecl)rd;
    527          // Need to check all overrides, because we may not have processed a
    528          // given direct override yet, removing its spurious non_null
    529          javafe.util.Set overrides = FlowInsensitiveChecks.getAllOverrides(md);
    530          if (overrides != null && !overrides.isEmpty()) {
    531            for (int i = 0; i < args.size(); ++i) {
    532              FormalParaDecl arg = args.elementAt(i);
    533              ModifierPragma m = Utils.findModifierPragma(arg,
    534                  TagConstants.NON_NULL);
    535              if (m != null) { // overriding method has non_null for parameter i
    536                MethodDecl smd = FlowInsensitiveChecks.getSuperNonNullStatus(md, i,
    537                    overrides);
    538                if (smd != null) { // overridden method does not have non_null for i
    539                  FormalParaDecl sf = smd.args.elementAt(i);
    540                  ErrorSet
    541                      .caution(
    542                          m.getStartLoc(),
    543                          "The non_null annotation is ignored because this method overrides a method declaration in which this parameter is not declared non_null: ",
    544                          sf.getStartLoc());
    545                  Utils.removeModifierPragma(arg, TagConstants.NON_NULL);
    546                }
    547              }
    548            }
    549          }
    550        }
    551
    552        // Handle non_null on any parameter
    553        for (int i = 0; i < args.size(); ++i) {
    554          FormalParaDecl arg = args.elementAt(i);
    555          ModifierPragma m = Utils.findModifierPragma(arg.pmodifiers,
    556              TagConstants.NON_NULL);
    557          if (m == null) continue;
    558          int locNN = m.getStartLoc();
    559          result.addElement(ExprModifierPragma.make(TagConstants.REQUIRES,
    560              NonNullExpr.make(arg, locNN), locNN));
    561        }
    562
    563        // Handle non_null on the result
    564        // non_null is not allowed on constructors - an error should have
    565        // been previously given
    566        if (rd instanceof MethodDecl) {
    567          ModifierPragma m = Utils.findModifierPragma(rd.pmodifiers,
    568              TagConstants.NON_NULL);
    569          if (m != null) {
    570            int locNN = m.getStartLoc();
    571            Expr r = ResExpr.make(locNN);
    572            javafe.tc.FlowInsensitiveChecks.setType(r, ((MethodDecl)rd).returnType);
    573            Expr n = LiteralExpr.make(TagConstants.NULLLIT, null, locNN);
    574            javafe.tc.FlowInsensitiveChecks.setType(n, Types.nullType);
    575            Expr e = BinaryExpr.make(TagConstants.NE, r, n, locNN);
    576            javafe.tc.FlowInsensitiveChecks.setType(e, Types.booleanType);
    577            ExprModifierPragma emp = ExprModifierPragma.make(TagConstants.ENSURES,
    578                e, locNN);
    579            Utils.owningDecl.set(emp,rd);
    580            emp.errorTag = TagConstants.CHKNONNULLRESULT;
    581            result.addElement(emp);
    582          }
    583        }
    584        return result;
    585      }
    586
    587      // Argument is an ArrayList of ModifierPragmaVec corresponding to
    588      // also-connected de-nested specification cases
    589      // result is a single ModifierPragmaVec with all the requires
    590      // clauses combined and all the other clauses guarded by the
    591      // relevant precondition
    592      public ModifierPragmaVec desugar(ArrayList ps, RoutineDecl tde) {
    593        ArrayList requiresList = new ArrayList();
    594        ModifierPragmaVec resultList = ModifierPragmaVec.make();
    595        resultList.addElement(null); // replaced below
    596        Iterator i = ps.iterator();
    597        while (i.hasNext()) {
    598          ModifierPragmaVec m = (ModifierPragmaVec)i.next();
    599          desugar(m, requiresList, resultList, tde);
    600        }
    601        // combine all of the requires
    602        ExprModifierPragma requires = or(requiresList);
    603        resultList.setElementAt(requires, 0);
    604        if (requires == null) resultList.removeElementAt(0);
    605        return resultList;
    606      }
    607
    608      // requiresList is an ArrayList of ModifierPragma
    609      public void desugar(ModifierPragmaVec m, ArrayList requiresList,
    610          ModifierPragmaVec resultList, RoutineDecl tde) {
    611        GenericVarDeclVec foralls = GenericVarDeclVec.make();
    612        // First collect all the requires clauses together
    613        int pos = 0;
    614        ArrayList list = new ArrayList();
    615        boolean addTypeCheck = (!Modifiers.isStatic(tde.getModifiers()) && tde instanceof MethodDecl);
    616        TypeSig ts = TypeSig.getSig(tde.parent);
    617        int loc = Location.NULL;
    618
    619        while (pos < m.size()) {
    620          ModifierPragma mp = m.elementAt(pos++);
    621          // FIXME - what if some foralls happen after requires - not in scope?
    622          int tag = mp.getTag();
    623          if (tag == TagConstants.NO_WACK_FORALL)
    624              foralls.addElement(((VarDeclModifierPragma)mp).decl);
    625          if (tag != TagConstants.REQUIRES && tag != TagConstants.PRECONDITION)
    626              continue;
    627          if (((ExprModifierPragma)mp).expr.getTag() == TagConstants.NOTSPECIFIEDEXPR)
    628              continue;
    629          loc = mp.getStartLoc();
    630          list.add(forallWrap(foralls, mp));
    631        }
    632        if (addTypeCheck) {
    633            Expr e = ThisExpr.make(null, Location.NULL);
    634            javafe.tc.FlowInsensitiveChecks.setType(e, ts);
    635            e = InstanceOfExpr.make(e, ts, Location.NULL);
    636            javafe.tc.FlowInsensitiveChecks.setType(e, Types.booleanType);
    637            list.add(0,(ExprModifierPragma.make(TagConstants.REQUIRES,e,loc)));
    638        }
    639        ExprModifierPragma conjunction = and(list);
    640        boolean reqIsTrue = conjunction == null || isTrue(conjunction.expr);
    641        Expr reqexpr = conjunction == null ? null : conjunction.expr;
    642        Expr req = T;
    643        if (reqexpr != null) {
    644          ExprVec arg = ExprVec.make(new Expr[] { reqexpr });
    645          req = NaryExpr.make(Location.NULL, reqexpr.getStartLoc(),
    646              TagConstants.PRE, Identifier.intern("\\old"), arg);
    647          javafe.tc.FlowInsensitiveChecks.setType(req, Types.booleanType);
    648        }
    649
    650        if (reqIsTrue && m.size() == 0) return;
    651
    652        requiresList.add(reqIsTrue ? ExprModifierPragma.make(TagConstants.REQUIRES,
    653            T, Location.NULL) : andLabeled(list));
    654
    655        // Now transform each non-requires pragma
    656        boolean foundDiverges = false;
    657        VarExprModifierPragma foundSignalsOnly = null;
    658        ExprModifierPragma defaultDiverges = null;
    659        boolean foundModifies = false;
    660        boolean isLightweight = true;
    661        pos = 0;
    662        while (pos < m.size()) {
    663          ModifierPragma mp = m.elementAt(pos++);
    664          int tag = mp.getTag();
    665          if (tag == TagConstants.REQUIRES || tag == TagConstants.PRECONDITION)
    666              continue;
    667          switch (tag) {
    668            case TagConstants.DIVERGES:
    669              foundDiverges = true;
    670            // fall-through
    671            case TagConstants.ENSURES:
    672            case TagConstants.POSTCONDITION:
    673            case TagConstants.WHEN: {
    674              ExprModifierPragma mm = (ExprModifierPragma)mp;
    675              if (mm.expr.getTag() == TagConstants.NOTSPECIFIEDEXPR) break;
    676              if (mm.expr.getTag() == TagConstants.INFORMALPRED_TOKEN) break;
    677              if (isTrue(mm.expr)) break;
    678              if (!reqIsTrue) mm.expr = implies(req, mm.expr);
    679              resultList.addElement(mm);
    680              break;
    681            }
    682
    683            case TagConstants.SIGNALS: {
    684              if (mp.originalTag() == TagConstants.SIGNALS_ONLY) {
    685                 if (foundSignalsOnly != null) {
    686                     ErrorSet.error(mp.getStartLoc(),
    687                       "Only one signals_only clause is allowed per specification case",
    688                       foundSignalsOnly.getStartLoc());
    689                 } else {
    690                     foundSignalsOnly = (VarExprModifierPragma)mp;
    691                 }
    692              }
    693              VarExprModifierPragma mm = (VarExprModifierPragma)mp;
    694              if (mm.expr.getTag() == TagConstants.NOTSPECIFIEDEXPR) break;
    695              if (mm.expr.getTag() == TagConstants.INFORMALPRED_TOKEN) break;
    696              if (isTrue(mm.expr)) break;
    697              if (!reqIsTrue) mm.expr = implies(req, mm.expr);
    698              resultList.addElement(mm);
    699              break;
    700            }
    701            case TagConstants.MODIFIESGROUPPRAGMA: {
    702              foundModifies = true;
    703              ModifiesGroupPragma mm = (ModifiesGroupPragma)mp;
    704              mm.precondition = req;
    705              resultList.addElement(mm);
    706              break;
    707            }
    708            /*
    709             * case TagConstants.MODIFIES: case TagConstants.MODIFIABLE: case
    710             * TagConstants.ASSIGNABLE: { CondExprModifierPragma mm =
    711             * (CondExprModifierPragma)mp; if (mm.expr != null && mm.expr.getTag() ==
    712             * TagConstants.NOTSPECIFIEDEXPR) break; foundModifies = true; mm.cond =
    713             * and(mm.cond,req); resultList.addElement(mm); break; }
    714             */
    715
    716            case TagConstants.WORKING_SPACE:
    717            case TagConstants.DURATION: {
    718              CondExprModifierPragma mm = (CondExprModifierPragma)mp;
    719              if (mm.expr != null
    720                  && mm.expr.getTag() == TagConstants.NOTSPECIFIEDEXPR) break;
    721              mm.cond = and(mm.cond, req);
    722              resultList.addElement(mm);
    723              break;
    724            }
    725
    726            case TagConstants.ACCESSIBLE:
    727            case TagConstants.CALLABLE:
    728            case TagConstants.MEASURED_BY:
    729            case TagConstants.MODEL_PROGRAM:
    730            case TagConstants.CODE_CONTRACT:
    731              // Remember to skip if not specified
    732              // FIXME - not yet handled
    733              foundModifies = true; // Don't add a default modifies
    734              foundDiverges = true;
    735              break;
    736
    737            case TagConstants.NO_WACK_FORALL:
    738            case TagConstants.OLD:
    739              // These are handled elsewhere and don't get put into
    740              // the pragma list.
    741              break;
    742
    743            case TagConstants.MONITORED_BY:
    744              ErrorSet.error(mp.getStartLoc(),
    745                  "monitored_by is obsolete and only applies to fields");
    746              break;
    747
    748            case TagConstants.MONITORED:
    749              ErrorSet.error(mp.getStartLoc(), "monitored only applies to fields");
    750              break;
    751
    752            case TagConstants.BEHAVIOR:
    753              // Used to distinguish lightweight and heavyweight sequences
    754              isLightweight = false;
    755              break;
    756
    757            default:
    758              ErrorSet.error(mp.getStartLoc(),
    759                  "Unknown kind of pragma for a routine declaration: "
    760                      + TagConstants.toString(tag));
    761              break;
    762          }
    763        }
    764        if (foundSignalsOnly == null) {
    765            Expr defaultExpr = AnnotationHandler.F;
    766            // Create a default signals_only clause using the list of exceptions
    767            // prior to any adjustment
    768            foundSignalsOnly = defaultSignalsOnly(tde,req);
    769            resultList.addElement(foundSignalsOnly);
    770            m.insertElementAt(foundSignalsOnly,0);
    771        }
    772        if (!foundDiverges) {
    773          // The default diverges clause is 'false'
    774          resultList.addElement(ExprModifierPragma.make(TagConstants.DIVERGES,
    775              implies(req, AnnotationHandler.F), Location.NULL));
    776        }
    777
    778        if (!foundModifies) {
    779          resultList.addElement(defaultModifies(tde.getStartLoc(), req, tde));
    780        }
    781        Expr sexpr = foundSignalsOnly.expr;
    782        pos = 0;
    783        while (pos < m.size()) {
    784          ModifierPragma mp = m.elementAt(pos++);
    785          int tag = mp.getTag();
    786          if (tag != TagConstants.SIGNALS) continue;
    787          if (mp.originalTag() == TagConstants.SIGNALS_ONLY) continue;
    788          VarExprModifierPragma vmp = (VarExprModifierPragma)mp;
    789          if (isFalse(vmp.expr)) continue;
    790          if ((vmp.expr instanceof BinaryExpr) && ((BinaryExpr)vmp.expr).op == TagConstants.IMPLIES && isFalse(((BinaryExpr)vmp.expr).right)) continue;
    791          Type t = vmp.arg.type;
    792          if (!isInSignalsOnlyExpr(t,sexpr,true)) {
    793            if (Types.isCastable(t,Types.javaLangThrowable()) &&
    794              !Types.isCastable(t,Types.javaLangException())) {}
    795            else
    796              ErrorSet.error(t.getStartLoc(),
    797                "Exception type in signals clause must be listed in either a " +
    798                "corresponding signals_only clause or the method's throws list",
    799                foundSignalsOnly.getStartLoc());
    800          }
    801        }
    802      }
    803
    804      private boolean isInSignalsOnlyExpr(Type t, Expr e, boolean allowSuperTypes) {
    805        if (e == null) return false;
    806        if (e instanceof BinaryExpr) {
    807          BinaryExpr be = (BinaryExpr)e;
    808          if (be.op == TagConstants.IMPLIES) return isInSignalsOnlyExpr(t,be.right,allowSuperTypes);
    809          return isInSignalsOnlyExpr(t,be.left,allowSuperTypes) ||
    810                 isInSignalsOnlyExpr(t,be.right,allowSuperTypes);
    811        } else if (e instanceof NaryExpr) {
    812          NaryExpr ne = (NaryExpr)e;
    813          for (int i=0; i<ne.exprs.size(); ++i) {
    814            Expr ee = ne.exprs.elementAt(i);
    815            if (isInSignalsOnlyExpr(t,ee,allowSuperTypes)) return true;
    816          }
    817          return false;
    818        } else if (e instanceof LiteralExpr) {
    819          return false;
    820        } else if (e instanceof InstanceOfExpr) {
    821          InstanceOfExpr ie = (InstanceOfExpr)e;
    822          if (allowSuperTypes) {
    823             if (Types.isCastable(ie.type,t)) return true;
    824          }
    825          if ( Types.isCastable(t,ie.type) ) return true;
    826          return false;
    827        } else {
    828          System.out.println("UNHANDLED TYPE-A " + e.getClass());
    829          return false;
    830        }
    831      }
    832
    833      public final static VarExprModifierPragma defaultSignalsOnly(
    834                            RoutineDecl tde, Expr req) {
    835            int throwsLoc = tde.locThrowsKeyword;
    836            if (throwsLoc == Location.NULL) throwsLoc = tde.getStartLoc();
    837            Expr defaultExpr = AnnotationHandler.F;
    838            TypeNameVec tv = tde.raises;
    839            Identifier id = TagConstants.ExsuresIdnName;
    840            FormalParaDecl arg = FormalParaDecl.make(0, null, id,
    841                          Main.options().useThrowable ?
    842                          Types.javaLangThrowable() : Types.javaLangException(),
    843                          throwsLoc);
    844            for (int i=0; i<tv.size(); ++i) {
    845                TypeName tn =tv.elementAt(i);
    846                int loc = tn.getStartLoc();
    847                Expr e = InstanceOfExpr.make(
    848                      VariableAccess.make(id, loc, arg), tn, loc);
    849                FlowInsensitiveChecks.setType(e, Types.booleanType);
    850                defaultExpr = BinaryExpr.make(TagConstants.OR,
    851                               defaultExpr, e, loc);
    852                FlowInsensitiveChecks.setType(defaultExpr, Types.booleanType);
    853            }
    854            VarExprModifierPragma newmp = VarExprModifierPragma.make(
    855                  TagConstants.SIGNALS, arg, defaultExpr, throwsLoc);
    856            newmp.setOriginalTag(TagConstants.SIGNALS_ONLY);
    857            newmp.expr = implies(req, newmp.expr);
    858            return newmp;
    859      }
    860
    861      public final static ModifiesGroupPragma defaultModifies(int loc, Expr req,
    862          RoutineDecl rd) {
    863        boolean everythingIsDefault = true;
    864        boolean nothing = !everythingIsDefault;
    865        boolean isPure = Utils.isPure(rd);
    866
    867        if (isPure) nothing = true;
    868        Expr e;
    869        if (isPure && rd instanceof ConstructorDecl) {
    870          ExprObjectDesignator eod = ExprObjectDesignator.make(loc, ThisExpr.make(
    871              null, loc));
    872          FlowInsensitiveChecks.setType(eod.expr, TypeSig.getSig(rd.parent));
    873          e = WildRefExpr.make(null, eod);
    874        } else if (nothing) {
    875          e = NothingExpr.make(loc);
    876        } else {
    877          e = EverythingExpr.make(loc);
    878        }
    879
    880        // FIXME - need default for COnstructor, ModelConstructor
    881        ModifiesGroupPragma r = ModifiesGroupPragma
    882            .make(TagConstants.MODIFIES, loc);
    883        r.addElement(CondExprModifierPragma.make(TagConstants.MODIFIES, e, loc,
    884            null));
    885        r.precondition = req;
    886        return r;
    887      }
    888
    889      public ModifierPragma forallWrap(GenericVarDeclVec foralls, ModifierPragma mp) {
    890        if (mp instanceof ExprModifierPragma) {
    891          ExprModifierPragma emp = (ExprModifierPragma)mp;
    892          emp.expr = forallWrap(foralls, emp.expr);
    893          FlowInsensitiveChecks.setType(emp.expr, Types.booleanType);
    894        }
    895        return mp;
    896      }
    897
    898      public Expr forallWrap(GenericVarDeclVec foralls, Expr e) {
    899        if (foralls.size() == 0) return e;
    900        int loc = foralls.elementAt(0).getStartLoc();
    901        int endLoc = foralls.elementAt(foralls.size() - 1).getStartLoc();
    902        return QuantifiedExpr.make(loc, endLoc, TagConstants.FORALL, foralls, null,
    903            e, null, null);
    904      }
    905
    906      public void deNest(ArrayList ps, ModifierPragmaVec prefix,
    907          ArrayList deNestedSpecs) {
    908        if (ps.size() == 0 && prefix.size() != 0) {
    909          combineModifies(prefix);
    910          fixDefaultSpecs(prefix);
    911          deNestedSpecs.add(prefix);
    912        } else {
    913          Iterator i = ps.iterator();
    914          while (i.hasNext()) {
    915            ModifierPragmaVec m = (ModifierPragmaVec)i.next();
    916            deNest(m, prefix, deNestedSpecs);
    917          }
    918        }
    919      }
    920
    921      public void combineModifies(ModifierPragmaVec list) {
    922        ModifiesGroupPragma m = null;
    923        for (int i = 0; i < list.size(); ++i) {
    924          ModifierPragma mp = list.elementAt(i);
    925          if (mp.getTag() == TagConstants.MODIFIESGROUPPRAGMA) {
    926            ModifiesGroupPragma mm = (ModifiesGroupPragma)mp;
    927            if (m == null)
    928              m = mm;
    929            else {
    930              m.append(mm);
    931              list.removeElementAt(i);
    932              --i;
    933            }
    934          }
    935        }
    936      }
    937
    938      //@ requires (* m.size() > 0 *);
    939      // Uses the fact that if there is a nesting it is the last element of
    940      // the ModifierPragmaVec
    941      public void deNest(ModifierPragmaVec m, ModifierPragmaVec prefix,
    942          ArrayList deNestedSpecs) {
    943        ModifierPragma last = m.elementAt(m.size() - 1);
    944        if (last instanceof NestedModifierPragma) {
    945          m.removeElementAt(m.size() - 1);
    946          ModifierPragmaVec newprefix = prefix.copy();
    947          newprefix.append(m);
    948          m.addElement(last);
    949          ArrayList list = ((NestedModifierPragma)last).list;
    950          deNest(list, newprefix, deNestedSpecs);
    951        } else {
    952          ModifierPragmaVec mm = prefix.copy();
    953          mm.append(m);
    954          combineModifies(mm);
    955          fixDefaultSpecs(mm);
    956          deNestedSpecs.add(mm);
    957        }
    958      }
    959
    960      public void fixDefaultSpecs(ModifierPragmaVec prefix) {
    961        // This step is necessary because a singleton instance of a default
    962        // Pragma can be used.  Since we are going to change the expression.
    963        for (int i = 0; i < prefix.size(); ++i) {
    964          ModifierPragma mp = prefix.elementAt(i);
    965          if (mp.getTag() == TagConstants.SIGNALS) {
    966            VarExprModifierPragma vmp = (VarExprModifierPragma)mp;
    967            if (isFalse(vmp.expr)) {
    968              VarExprModifierPragma newvmp = VarExprModifierPragma.make(vmp.tag,
    969                  vmp.arg, vmp.expr, vmp.loc);
    970              newvmp.setOriginalTag(vmp.originalTag());
    971              prefix.setElementAt(newvmp, i);
    972            }
    973          }
    974          if (mp.getTag() == TagConstants.ENSURES) {
    975            ExprModifierPragma vmp = (ExprModifierPragma)mp;
    976            if (isFalse(vmp.expr)) {
    977              ExprModifierPragma newvmp = ExprModifierPragma.make(vmp.tag,
    978                  vmp.expr, vmp.loc);
    979              newvmp.setOriginalTag(vmp.originalTag());
    980              if (Utils.ensuresDecoration.isTrue(vmp))
    981                Utils.ensuresDecoration.set(newvmp,true);
    982              prefix.setElementAt(newvmp, i);
    983            }
    984          }
    985          // FIXME - perhaps diverges, modifies
    986        }
    987      }
    988
    989      /**
    990       * Produces an expression which is the conjunction of the two expressions. If
    991       * either input is null, the other is returned. If either input is literally
    992       * true or false, the appropriate constant folding is performed.
    993       */
    994      static public Expr and(Expr e1, Expr e2) {
    995        if (e1 == null || isTrue(e1)) return e2;
    996        if (e2 == null || isTrue(e2)) return e1;
    997        if (isFalse(e1)) return e1;
    998        if (isFalse(e2)) return e2;
    999        Expr e = BinaryExpr.make(TagConstants.AND, e1, e2, e1.getStartLoc());
    1000        javafe.tc.FlowInsensitiveChecks.setType(e, Types.booleanType);
    1001        return e;
    1002      }
    1003
    1004      /**
    1005       * Produces an ExprModifierPragma whose expression is the conjunction of the
    1006       * expressions in the input pragmas. If either input is null, the other is
    1007       * returned. If either input is literally true or false, the appropriate
    1008       * constant folding is performed.
    1009       */
    1010      static public ExprModifierPragma and(ExprModifierPragma e1,
    1011          ExprModifierPragma e2) {
    1012        if (e1 == null || isTrue(e1.expr)) return e2;
    1013        if (e2 == null || isTrue(e2.expr)) return e1;
    1014        if (isFalse(e1.expr)) return e1;
    1015        if (isFalse(e2.expr)) return e2;
    1016        Expr e = BinaryExpr.make(TagConstants.AND, e1.expr, e2.expr, e1
    1017            .getStartLoc());
    1018        javafe.tc.FlowInsensitiveChecks.setType(e, Types.booleanType);
    1019        return ExprModifierPragma.make(e1.getTag(), e, e1.getStartLoc());
    1020      }
    1021
    1022      /**
    1023       * Produces an ExprModifierPragma whose expression is the conjunction of all
    1024       * of the expressions in the ExprModifierPragmas in the argument. If the
    1025       * argument is empty, null is returned. Otherwise, some object is returned,
    1026       * though its expression might be a literal.
    1027       */
    1028      static public ExprModifierPragma and(/* @ non_null */ArrayList a) {
    1029        if (a.size() == 0) {
    1030          return null;
    1031        } else if (a.size() == 1) {
    1032          return (ExprModifierPragma)a.get(0);
    1033        } else {
    1034          ExprModifierPragma e = null;
    1035          Iterator i = a.iterator();
    1036          while (i.hasNext()) {
    1037            e = and(e, (ExprModifierPragma)i.next());
    1038          }
    1039          return e;
    1040        }
    1041      }
    1042
    1043      /**
    1044       * The same as and(ArrayList), but produces labelled expressions within the
    1045       * conjunction so that error messages come out with useful locations.
    1046       */
    1047      static public ExprModifierPragma andLabeled(/* @ non_null */ArrayList a) {
    1048        if (a.size() == 0) {
    1049          return null;
    1050        } else {
    1051          Expr e = null;
    1052          int floc = Location.NULL;
    1053          Iterator i = a.iterator();
    1054          while (i.hasNext()) {
    1055            ExprModifierPragma emp = (ExprModifierPragma)i.next();
    1056            int loc = emp.getStartLoc();
    1057            if (floc == Location.NULL) floc = loc;
    1058            boolean nn = emp.expr instanceof NonNullExpr;
    1059            Expr le = LabelExpr.make(emp.getStartLoc(), emp.getEndLoc(), false,
    1060                escjava.translate.GC.makeFullLabel(nn ? "NonNull" : "Pre", loc,
    1061                    Location.NULL), // FIXME - does this get translated to include
    1062                                    // an @ location ?
    1063                emp.expr);
    1064            javafe.tc.FlowInsensitiveChecks.setType(le, Types.booleanType);
    1065            if (!isTrue(emp.expr))
    1066              e = and(e, le);
    1067            else if (e == null) e = le;
    1068            javafe.tc.FlowInsensitiveChecks.setType(e, Types.booleanType);
    1069          }
    1070          return ExprModifierPragma.make(TagConstants.REQUIRES, e, floc);
    1071        }
    1072      }
    1073
    1074      /*
    1075       * static public Expr or(Expr e1, Expr e2) { if (e1 == null || isFalse(e1))
    1076       * return e2; if (e2 == null || isFalse(e2)) return e1; if (isTrue(e1)) return
    1077       * e1; if (isTrue(e2)) return e2; Expr e =
    1078       * BinaryExpr.make(TagConstants.OR,e1,e2,e1.getStartLoc());
    1079       * javafe.tc.FlowInsensitiveChecks.setType(e,Types.booleanType); return e; }
    1080       */
    1081      /**
    1082       * Produces an ExprModifierPragma whose expression is the disjunction of the
    1083       * expressions in the input pragmas. If either input is null, the other is
    1084       * returned. If either input is literally true or false, the appropriate
    1085       * constant folding is performed.
    1086       */
    1087      static public ExprModifierPragma or(ExprModifierPragma e1,
    1088          ExprModifierPragma e2) {
    1089        if (e1 == null || isFalse(e1.expr)) return e2;
    1090        if (e2 == null || isFalse(e2.expr)) return e1;
    1091        if (isTrue(e1.expr)) return e1;
    1092        if (isTrue(e2.expr)) return e2;
    1093        Expr e = BinaryExpr.make(TagConstants.OR, e1.expr, e2.expr, e1
    1094            .getStartLoc());
    1095        javafe.tc.FlowInsensitiveChecks.setType(e, Types.booleanType);
    1096        return ExprModifierPragma.make(e1.getTag(), e, e1.getStartLoc());
    1097      }
    1098
    1099      /**
    1100       * Produces an ExprModifierPragma whose expression is the disjunction of all
    1101       * of the expressions in the ExprModifierPragmas in the argument. If the
    1102       * argument is empty, null is returned. Otherwise, some object is returned,
    1103       * though its expression might be a literal.
    1104       */
    1105      static public ExprModifierPragma or(/* @ non_null */ArrayList a) {
    1106        if (a.size() == 0) {
    1107          return null;
    1108        } else if (a.size() == 1) {
    1109          return (ExprModifierPragma)a.get(0);
    1110        } else {
    1111          ExprModifierPragma e = null;
    1112          Iterator i = a.iterator();
    1113          while (i.hasNext()) {
    1114            e = or(e, (ExprModifierPragma)i.next());
    1115          }
    1116          return e;
    1117        }
    1118      }
    1119
    1120      /**
    1121       * Produces an expression which is the implication of the two expressions.
    1122       * Neither input may be null. If either input is literally true or false, the
    1123       * appropriate constant folding is performed.
    1124       */
    1125      static public Expr implies(/* @ non_null */Expr e1, /* @ non_null */Expr e2) {
    1126        if (isTrue(e1)) return e2;
    1127        if (isTrue(e2)) return e2; // Use e2 instead of T to keep location info
    1128        if (isFalse(e1)) return T;
    1129        Expr e = BinaryExpr.make(TagConstants.IMPLIES, e1, e2, e2.getStartLoc());
    1130        javafe.tc.FlowInsensitiveChecks.setType(e, Types.booleanType);
    1131        return e;
    1132      }
    1133
    1134      /**
    1135       * Returns true if the argument is literally true, and returns false if it is
    1136       * not a literal or is literally false.
    1137       */
    1138      static boolean isTrue(/* @ non_null */Expr e) {
    1139        return e == T
    1140            || (e instanceof LiteralExpr && ((LiteralExpr)e).value.equals(T.value));
    1141      }
    1142
    1143      /**
    1144       * Returns true if the argument is literally false, and returns false if it is
    1145       * not a literal or is literally true.
    1146       */
    1147      static boolean isFalse(/* @ non_null */Expr e) {
    1148        return e == F
    1149            || (e instanceof LiteralExpr && ((LiteralExpr)e).value.equals(F.value));
    1150      }
    1151
    1152      public final static LiteralExpr T = (LiteralExpr)FlowInsensitiveChecks
    1153          .setType(LiteralExpr.make(TagConstants.BOOLEANLIT, Boolean.TRUE,
    1154              Location.NULL), Types.booleanType);
    1155
    1156      public final static LiteralExpr F = (LiteralExpr)FlowInsensitiveChecks
    1157          .setType(LiteralExpr.make(TagConstants.BOOLEANLIT, Boolean.FALSE,
    1158              Location.NULL), Types.booleanType);
    1159
    1160      static public class Context {
    1161        public Expr expr;
    1162
    1163      }
    1164
    1165      static public class CheckPurity {
    1166
    1167        public void visitNode(ASTNode x, Context cc) {
    1168          if (x == null) return;
    1169          //System.out.println("CP TAG " + TagConstants.toString(x.getTag()));
    1170          switch (x.getTag()) {
    1171            case TagConstants.METHODINVOCATION:
    1172              MethodInvocation m = (MethodInvocation)x;
    1173              if (Main.options().checkPurity && !Utils.isPure(m.decl)) {
    1174                ErrorSet.error(m.locId, "Method " + m.id
    1175                               + " may not be used in an annotation since it is not pure",
    1176                               m.decl.loc);
    1177                if (Main.options().checkPurity && Utils.isAllocates(m.decl)) {
    1178                  ErrorSet.error(m.locId, "Method " + m.id
    1179                                 + " may not be used in an annotation since it allocates"
    1180                                 + " fresh storage");
    1181              }
    1182            }
    1183            break;
    1184            case TagConstants.NEWINSTANCEEXPR:
    1185              NewInstanceExpr c = (NewInstanceExpr)x;
    1186              // @review kiniry, chalin 21 Aug 2005 - If/when we revise assertion semantics,
    1187              // this will need to be updated appropriately.
    1188                      if (Main.options().checkPurity && !Utils.isPure(c.decl)) {
    1189                        ErrorSet.error(c.loc, "Constructor is used in an annotation"
    1190                                       + " but is not pure (" + Location.toFileLineString(c.decl.loc)
    1191                                       + ")");
    1192                      }
    1193                      break;
    1194            case TagConstants.WACK_DURATION:
    1195            case TagConstants.WACK_WORKING_SPACE:
    1196            case TagConstants.SPACE:
    1197              // The argument of these built-in functions is not
    1198              // evaluated, so it need not be pure.
    1199              return;
    1200
    1201            case TagConstants.ENSURES:
    1202            case TagConstants.POSTCONDITION:
    1203            case TagConstants.REQUIRES:
    1204            case TagConstants.PRECONDITION: {
    1205              // @bug kiniry 21 Aug 2005 - Won't this crash with a SOO if any of these spec
    1206              // expressions are recursive?
    1207              Context cn = new Context();
    1208              cn.expr = ((ExprModifierPragma)x).expr;
    1209              visitNode(cn.expr, cn);
    1210              ((ExprModifierPragma)x).expr = cn.expr;
    1211              return;
    1212            }
    1213
    1214            case TagConstants.SIGNALS:
    1215            case TagConstants.EXSURES:
    1216              // @review kiniry 21 Aug 2005 - Why are we not checking subexpressions of these
    1217              // spec expressions?
    1218              break;
    1219          }
    1220          {
    1221            int n = x.childCount();
    1222            for (int i = 0; i < n; ++i) {
    1223              if (x.childAt(i) instanceof ASTNode)
    1224                visitNode((ASTNode)x.childAt(i), cc);
    1225            }
    1226          }
    1227        }
    1228
    1229      }
    1230
    1231      static private void print(Expr e) {
    1232        if (e != null) PrettyPrint.inst.print(System.out, 0, e);
    1233      }
    1234
    1235      static public class NonNullExpr extends BinaryExpr {
    1236
    1237        static NonNullExpr make(FormalParaDecl arg, int locNN) {
    1238          NonNullExpr e = new NonNullExpr();
    1239          int loc = arg.getStartLoc();
    1240          Expr v = VariableAccess.make(arg.id, loc, arg);
    1241          javafe.tc.FlowInsensitiveChecks.setType(v, arg.type);
    1242          Expr n = LiteralExpr.make(TagConstants.NULLLIT, null, locNN);
    1243          javafe.tc.FlowInsensitiveChecks.setType(n, Types.nullType);
    1244          e.op = TagConstants.NE;
    1245          e.left = v;
    1246          e.right = n;
    1247          e.locOp = locNN;
    1248          javafe.tc.FlowInsensitiveChecks.setType(e, Types.booleanType);
    1249          return e;
    1250        }
    1251      }
    1252
    1253      //----------------------------------------------------------------------
    1254      // Parsing the sequence of ModifierPragmas for each method of a
    1255      // compilation unit happens as a part of the original parsing and
    1256      // refinement processing.
    1257
    1258      static NestedPragmaParser specparser = new NestedPragmaParser();
    1259
    1260      public void parseAllRoutineSpecs(CompilationUnit ccu) {
    1261        specparser.parseAllRoutineSpecs(ccu);
    1262      }
    1263
    1264      /**
    1265       * The routines in this class parse a sequence of ModifierPragma that occur
    1266       * prior to a method or constructor declaration. These consist of lightweight
    1267       * or heavyweight specifications, possibly nested or with consecutive
    1268       * spec-cases separated by 'also'. The parsing of the compilation unit simply
    1269       * produces a flat sequence of such ModifierPragmas, since they may occur in
    1270       * separate annotation comments and the Javafe parser does not provide
    1271       * mechanisms to associate them together. However, we do need to determine the
    1272       * nesting structure of the sequence of pragmas because the forall and old
    1273       * pragmas introduce new variable declarations that may be used in subsequent
    1274       * pragmas. This parsing into the nested structure (and checking of it) needs
    1275       * to be completed prior to type checking so that the variable references are
    1276       * properly determined. The ultimate desugaring then happens after
    1277       * typechecking.
    1278       *
    1279       * The resulting pmodifiers vector for each routine consists of a
    1280       * possibly-empty sequence of simple routine modifiers (e.g. pure, non_null)
    1281       * terminated with a single ParsedSpecs element.
    1282       */
    1283
    1284      static public class NestedPragmaParser {
    1285
    1286        /**
    1287         * Parses the sequence of pragma modifiers for each routine in the
    1288         * CompilationUnit, replacing the existing sequence with the parsed one in
    1289         * each case.
    1290         */
    1291        public void parseAllRoutineSpecs(CompilationUnit ccu) {
    1292          TypeDeclVec v = ccu.elems;
    1293          for (int i = 0; i < v.size(); ++i) {
    1294            parseAllRoutineSpecs(v.elementAt(i));
    1295          }
    1296        }
    1297
    1298        public void parseAllRoutineSpecs(TypeDecl td) {
    1299          TypeDeclElemVec v = td.elems;
    1300          for (int i = 0; i < v.size(); ++i) {
    1301            TypeDeclElem tde = v.elementAt(i);
    1302            if (tde instanceof RoutineDecl) {
    1303              parseRoutineSpecs((RoutineDecl)tde);
    1304            } else if (tde instanceof ModelMethodDeclPragma) {
    1305              parseRoutineSpecs(((ModelMethodDeclPragma)tde).decl);
    1306            } else if (tde instanceof ModelConstructorDeclPragma) {
    1307              parseRoutineSpecs(((ModelConstructorDeclPragma)tde).decl);
    1308            } else if (tde instanceof TypeDecl) {
    1309              parseAllRoutineSpecs((TypeDecl)tde);
    1310            }
    1311          }
    1312        }
    1313
    1314        public void parseRoutineSpecs(RoutineDecl rd) {
    1315          ModifierPragmaVec pm = rd.pmodifiers;
    1316          if (pm == null || pm.size() == 0) {
    1317            ParsedRoutineSpecs pms = new ParsedRoutineSpecs();
    1318            pms.modifiers.addElement(ParsedSpecs.make(rd, pms));
    1319            rd.pmodifiers = pms.modifiers;
    1320            return;
    1321          }
    1322          if (pm.elementAt(pm.size() - 1) instanceof ParsedSpecs) {
    1323            // It is a bit of a design problem that the parsing of the
    1324            // sequence of pragmas produces a new ModifierPragmaVec that
    1325            // overwrites the old one. That means that if we call
    1326            // parseRoutineSpecs twice on a routine we get problems.
    1327            // This test is here to avoid problems if a bug elsewhere
    1328            // causes this to happen.
    1329            System.out.println("OUCH - attempt to reparse "
    1330                + Location.toString(rd.getStartLoc()));
    1331            javafe.util.ErrorSet.dump("OUCH");
    1332            return;
    1333          }
    1334
    1335          // We add this (internal use only) END pragma so that we don't have
    1336          // to continually check the value of pos vs. the size of the array
    1337          pm.addElement(SimpleModifierPragma.make(TagConstants.END,
    1338              pm.size() == 0 ? Location.NULL : pm.elementAt(pm.size() - 1)
    1339                  .getStartLoc()));
    1340
    1341          ParsedRoutineSpecs pms = new ParsedRoutineSpecs();
    1342          int pos = 0;
    1343          if (pm.elementAt(0).getTag() == TagConstants.ALSO) {
    1344            pms.initialAlso = pm.elementAt(0);
    1345            ++pos;
    1346          }
    1347          pos = parseAlsoSeq(pos, pm, 1, null, pms.specs);
    1348          if (pm.elementAt(pos).getTag() == TagConstants.IMPLIES_THAT) {
    1349            ++pos;
    1350            pos = parseAlsoSeq(pos, pm, 1, null, pms.impliesThat);
    1351          }
    1352          if (pm.elementAt(pos).getTag() == TagConstants.FOR_EXAMPLE) {
    1353            ++pos;
    1354            pos = parseAlsoSeq(pos, pm, 2, null, pms.examples);
    1355          }
    1356          if (pm.elementAt(pos).getTag() == TagConstants.IMPLIES_THAT) {
    1357            ErrorSet
    1358                .caution(pm.elementAt(pos).getStartLoc(),
    1359                    "implies_that sections are expected to precede for_example sections");
    1360            ++pos;
    1361            pos = parseAlsoSeq(pos, pm, 1, null, pms.impliesThat);
    1362          }
    1363          while (true) {
    1364            ModifierPragma mp = pm.elementAt(pos);
    1365            int tag = mp.getTag();
    1366            if (tag == TagConstants.END) break;
    1367            // Turned off because of problems with annotations after the declaration
    1368            // - FIXME
    1369            if (false && !isRoutineModifier(tag)) {
    1370              int loc = Location.NULL;
    1371              if (pms.modifiers.size() > 0)
    1372                  loc = pms.modifiers.elementAt(0).getStartLoc();
    1373              ErrorSet
    1374                  .error(
    1375                      mp.getStartLoc(),
    1376                      "Unexpected or out of order pragma (expected a simple routine modifier)",
    1377                      loc);
    1378            } else {
    1379              pms.modifiers.addElement(mp);
    1380            }
    1381            ++pos;
    1382          }
    1383          pms.modifiers.addElement(ParsedSpecs.make(rd, pms));
    1384          rd.pmodifiers = pms.modifiers;
    1385        }
    1386
    1387        static public boolean isRoutineModifier(int tag) {
    1388          return tag == TagConstants.PURE || tag == TagConstants.SPEC_PUBLIC
    1389              || tag == TagConstants.SPEC_PROTECTED || tag == TagConstants.HELPER
    1390              || tag == TagConstants.GHOST || // Actually should not occur
    1391              tag == TagConstants.MODEL || tag == TagConstants.MONITORED
    1392              || tag == TagConstants.FUNCTION || tag == TagConstants.NON_NULL;
    1393        }
    1394
    1395        static public boolean isEndingModifier(int tag) {
    1396          return tag == TagConstants.END || tag == TagConstants.ALSO
    1397              || tag == TagConstants.IMPLIES_THAT
    1398              || tag == TagConstants.FOR_EXAMPLE;
    1399        }
    1400
    1401        // behaviorMode == 0 : nested call
    1402        // behaviorMode == 1 : outer call - non-example mode, model programs allowed
    1403        // behaviorMode == 2 : outer call - example mode
    1404        // The behaviorMode is used to determine which behavior/example keywords
    1405        // are valid - but this is only needed on the outermost nesting level.
    1406        // The behaviorTag is used to determine whether signals or ensures clauses
    1407        // are permitted; 0 means either are ok; not valid on outermost call
    1408        public int parseAlsoSeq(int pos, ModifierPragmaVec pm, int behaviorMode,
    1409            ModifierPragma behavior, ArrayList result) {
    1410          while (true) {
    1411            ModifierPragmaVec mpv = ModifierPragmaVec.make();
    1412            if (behaviorMode != 0) {
    1413              ModifierPragma mp = pm.elementAt(pos);
    1414              behavior = mp;
    1415              int behaviorTag = mp.getTag();
    1416              ++pos;
    1417              encounteredError = false;
    1418              switch (behaviorTag) {
    1419                case TagConstants.MODEL_PROGRAM:
    1420                  if (behaviorMode == 2) {
    1421                    ErrorSet.error(mp.getStartLoc(),
    1422                        "Model programs may not be in the examples section");
    1423                    encounteredError = true;
    1424                  } else if (!isEndingModifier(pm.elementAt(pos).getTag())
    1425                      && !isRoutineModifier(pm.elementAt(pos).getTag())) {
    1426                    ErrorSet.error(mp.getStartLoc(),
    1427                        "A model_program may not be combined with other clauses");
    1428                  } else {
    1429                    mpv.addElement(mp);
    1430                    result.add(mpv);
    1431                    break;
    1432                  }
    1433                  continue;
    1434                case TagConstants.CODE_CONTRACT:
    1435                  if (behaviorMode == 2) {
    1436                    ErrorSet.error(mp.getStartLoc(),
    1437                        "code_contract sections may not be in an examples section");
    1438                    encounteredError = true;
    1439                  } else {
    1440                    // FIXME - code_contract sections are ignored for now
    1441                    ModifierPragmaVec r = ModifierPragmaVec.make();
    1442                    pos = parseCCSeq(pos, pm, r);
    1443                    mpv.addElement(mp);
    1444                    result.add(mpv);
    1445                    break;
    1446                  }
    1447                  continue;
    1448
    1449                case TagConstants.BEHAVIOR:
    1450                  if (behaviorMode == 2)
    1451                      ErrorSet
    1452                          .error(mp.getStartLoc(),
    1453                              "Behavior keywords may not be in the for_example section");
    1454                  break;
    1455                case TagConstants.NORMAL_BEHAVIOR:
    1456                  if (behaviorMode == 2)
    1457                      ErrorSet
    1458                          .error(mp.getStartLoc(),
    1459                              "Behavior keywords may not be in the for_example section");
    1460                  mpv.addElement(VarExprModifierPragma.make(TagConstants.SIGNALS,
    1461                      FormalParaDecl.make(0, null, TagConstants.ExsuresIdnName,
    1462                          Types.javaLangException(), mp.getStartLoc()),
    1463                      AnnotationHandler.F, mp.getStartLoc()).
    1464                           setOriginalTag(TagConstants.SIGNALS_ONLY));
    1465                  break;
    1466                case TagConstants.EXCEPTIONAL_BEHAVIOR:
    1467                  if (behaviorMode == 2)
    1468                      ErrorSet
    1469                          .error(mp.getStartLoc(),
    1470                              "Behavior keywords may not be in the for_example section");
    1471                  ExprModifierPragma emp = ExprModifierPragma.make(
    1472                      TagConstants.ENSURES, AnnotationHandler.F, mp.getStartLoc());
    1473                  Utils.ensuresDecoration.set(emp, true);
    1474                  mpv.addElement(emp);
    1475                  break;
    1476                case TagConstants.EXAMPLE:
    1477                  if (behaviorMode == 1)
    1478                      ErrorSet
    1479                          .error(mp.getStartLoc(),
    1480                              "Example keywords may be used only in the for_example section");
    1481                  break;
    1482                case TagConstants.NORMAL_EXAMPLE:
    1483                  if (behaviorMode == 1)
    1484                      ErrorSet
    1485                          .error(mp.getStartLoc(),
    1486                              "Example keywords may be used only in the for_example section");
    1487                  mpv.addElement(VarExprModifierPragma.make(TagConstants.SIGNALS,
    1488                      FormalParaDecl.make(0, null, TagConstants.ExsuresIdnName,
    1489                          Types.javaLangException(), mp.getStartLoc()),
    1490                      AnnotationHandler.F, mp.getStartLoc()).
    1491                          setOriginalTag(TagConstants.SIGNALS_ONLY));
    1492                  break;
    1493                case TagConstants.EXCEPTIONAL_EXAMPLE:
    1494                  if (behaviorMode == 1)
    1495                      ErrorSet
    1496                          .error(mp.getStartLoc(),
    1497                              "Example keywords may be used only in the for_example section");
    1498                  ExprModifierPragma empp = ExprModifierPragma.make(
    1499                      TagConstants.ENSURES, AnnotationHandler.F, mp.getStartLoc());
    1500                  Utils.ensuresDecoration.set(empp, true);
    1501                  mpv.addElement(empp);
    1502                  break;
    1503                default:
    1504                  // lightweight
    1505                  --pos;
    1506                  behavior = null;
    1507              }
    1508            }
    1509            pos = parseSeq(pos, pm, 0, behavior, mpv);
    1510            if (behaviorMode != 0 && behavior != null) {
    1511              // Tag each heavyweight spec case
    1512              //if (mpv.size() > 0) mpv.addElement(heavyweightFlag);
    1513            }
    1514            if (mpv.size() != 0)
    1515              result.add(mpv);
    1516            else if (behaviorMode == 0 || result.size() != 0) {
    1517              if (!encounteredError)
    1518                  ErrorSet.error(pm.elementAt(pos).getStartLoc(),
    1519                      "JML does not allow empty clause sequences");
    1520              encounteredError = false;
    1521            }
    1522            if (pm.elementAt(pos).getTag() != TagConstants.ALSO) break;
    1523            ++pos;
    1524          }
    1525          if (behaviorMode != 0) {
    1526            while (pm.elementAt(pos).getTag() == TagConstants.CLOSEPRAGMA) {
    1527              ErrorSet.error(pm.elementAt(pos).getStartLoc(),
    1528                  "There is no opening {| to match this closing |}");
    1529              ++pos;
    1530            }
    1531          }
    1532          return pos;
    1533        }
    1534
    1535        private boolean encounteredError;
    1536
    1537        /** Parse the clauses in a code_contract section */
    1538        public int parseCCSeq(int pos, ModifierPragmaVec pm,
    1539            ModifierPragmaVec result) {
    1540          boolean badCCSection = false;
    1541          while (true) {
    1542            ModifierPragma mp = pm.elementAt(pos);
    1543            int loc = mp.getStartLoc();
    1544            int tag = mp.getTag();
    1545            // System.out.println("TAG " + TagConstants.toString(tag));
    1546            if (isRoutineModifier(tag)) return pos;
    1547            switch (tag) {
    1548              case TagConstants.END:
    1549              case TagConstants.IMPLIES_THAT:
    1550              case TagConstants.FOR_EXAMPLE:
    1551              case TagConstants.ALSO:
    1552                return pos;
    1553
    1554              case TagConstants.ACCESSIBLE:
    1555              case TagConstants.CALLABLE:
    1556              case TagConstants.MEASURED_BY:
    1557                result.addElement(mp);
    1558                ++pos;
    1559                break;
    1560
    1561              default:
    1562                if (!badCCSection)
    1563                    // Just one error message
    1564                    ErrorSet.error(loc,
    1565                        "Unexpected pragma in a code_contract section");
    1566                badCCSection = true;
    1567                ++pos;
    1568                break;
    1569            }
    1570          }
    1571        }
    1572
    1573        //@ requires (* pm.elementAt(pm.size()-1).getTag() == TagConstants.END *);
    1574        public int parseSeq(int pos, ModifierPragmaVec pm, int behaviorMode,
    1575            ModifierPragma behavior, ModifierPragmaVec result) {
    1576          int behaviorTag = behavior == null ? 0 : behavior.getTag();
    1577          //System.out.println("STARTING " + behaviorMode + " " + behaviorTag);
    1578          if (pm.elementAt(pos).getTag() == TagConstants.MODEL_PROGRAM) {
    1579            if (behaviorMode == 0) {
    1580              ErrorSet.error(pm.elementAt(pos).getStartLoc(),
    1581                  "Model programs may not be nested");
    1582              encounteredError = true;
    1583            }
    1584            ++pos;
    1585          }
    1586          if (pm.elementAt(pos).getTag() == TagConstants.CODE_CONTRACT) {
    1587            if (behaviorMode == 0) {
    1588              ErrorSet.error(pm.elementAt(pos).getStartLoc(),
    1589                  "code_contract sections may not be nested");
    1590              encounteredError = true;
    1591            }
    1592            ++pos;
    1593          }
    1594          while (true) {
    1595            ModifierPragma mp = pm.elementAt(pos);
    1596            int loc = mp.getStartLoc();
    1597            int tag = mp.getTag();
    1598            if (isRoutineModifier(tag)) return pos;
    1599            //System.out.println("TAG " + TagConstants.toString(tag));
    1600            switch (tag) {
    1601              case TagConstants.END:
    1602              case TagConstants.IMPLIES_THAT:
    1603              case TagConstants.FOR_EXAMPLE:
    1604              case TagConstants.ALSO:
    1605              case TagConstants.CLOSEPRAGMA:
    1606                return pos;
    1607
    1608              case TagConstants.MODEL_PROGRAM:
    1609                ErrorSet.error(mp.getStartLoc(),
    1610                    "Model programs may not be combined with other clauses");
    1611                ++pos;
    1612                break;
    1613
    1614              case TagConstants.CODE_CONTRACT:
    1615                ErrorSet
    1616                    .error(mp.getStartLoc(),
    1617                        "code_contract sections may not be combined with other clauses");
    1618                ++pos;
    1619                break;
    1620
    1621              case TagConstants.ACCESSIBLE:
    1622              case TagConstants.CALLABLE:
    1623              case TagConstants.MEASURED_BY:
    1624                ErrorSet.error(mp.getStartLoc(),
    1625                    "This clause may only be in a code_contract section");
    1626                ++pos;
    1627                break;
    1628
    1629              case TagConstants.BEHAVIOR:
    1630              case TagConstants.NORMAL_BEHAVIOR:
    1631              case TagConstants.EXCEPTIONAL_BEHAVIOR:
    1632              case TagConstants.EXAMPLE:
    1633              case TagConstants.NORMAL_EXAMPLE:
    1634              case TagConstants.EXCEPTIONAL_EXAMPLE:
    1635                if (behaviorMode == 0)
    1636                    ErrorSet.error(mp.getStartLoc(), "Misplaced "
    1637                        + TagConstants.toString(tag) + " keyword");
    1638                ++pos;
    1639                break;
    1640
    1641              case TagConstants.OPENPRAGMA: {
    1642                int openLoc = loc;
    1643                ++pos;
    1644                ArrayList s = new ArrayList();
    1645                pos = parseAlsoSeq(pos, pm, 0, behavior, s);
    1646                if (pm.elementAt(pos).getTag() != TagConstants.CLOSEPRAGMA) {
    1647                  ErrorSet.error(pm.elementAt(pos).getStartLoc(),
    1648                      "Expected a closing |}", openLoc);
    1649                } else {
    1650                  ++pos;
    1651                }
    1652                // Empty sequences are noted in parseAlsoSeq
    1653                if (s.size() != 0) {
    1654                  result.addElement(NestedModifierPragma.make(s));
    1655                }
    1656              }
    1657                break;
    1658
    1659              // Any clause keyword ends up in the default (as well as
    1660              // anything unrecognized). We do that because there are
    1661              // so many clause keywords. However, that means that we
    1662              // have to be sure to have the list of keywords in
    1663              // isRoutineModifier correct.
    1664              default:
    1665                if ((((behaviorTag == TagConstants.NORMAL_BEHAVIOR || behaviorTag == TagConstants.NORMAL_EXAMPLE) && (tag == TagConstants.SIGNALS || tag == TagConstants.EXSURES)))
    1666                    || (((behaviorTag == TagConstants.EXCEPTIONAL_BEHAVIOR || behaviorTag == TagConstants.EXCEPTIONAL_EXAMPLE) && (tag == TagConstants.ENSURES || tag == TagConstants.POSTCONDITION)))) {
    1667                  ErrorSet.error(loc, "A " + TagConstants.toString(tag)
    1668                      + " clause is not allowed in a "
    1669                      + TagConstants.toString(behaviorTag) + " section", behavior
    1670                      .getStartLoc());
    1671                } else {
    1672                  result.addElement(mp);
    1673                }
    1674                ++pos;
    1675            }
    1676          }
    1677        }
    1678      }
    1679
    1680      /*
    1681       * public static List findRepresents(FieldDecl fd) { TypeDecl td = fd.parent;
    1682       * TypeDeclElemVec tdepv = td.elems; for (int i=0; i <tdepv.size(); ++i) {
    1683       * TypeDeclElem tde = tdepv.elementAt(i); if (!(tde instanceof
    1684       * TypeDeclElemPragma)) continue; if (tde.getTag() != TagConstants.REPRESENTS)
    1685       * continue; Expr target = ((NamedExprDeclPragma)tde).target; if (!(target
    1686       * instanceof FieldAccess)) { ErrorSet.error(tde.getStartLoc(), "INTERNAL
    1687       * ERROR: Expected FieldAccess here"); continue; } FieldDecl fdd =
    1688       * ((FieldAccess)target).decl; if (fd != fdd) continue; results.add(
    1689       * ((NamedExprDeclPragma)tde).expr ); } return results; }
    1690       */
    1691      static private ModifierPragma heavyweightFlag = SimpleModifierPragma.make(
    1692          TagConstants.BEHAVIOR, Location.NULL);
    1693    }
    1694    // FIXME - things not checked
    1695    //      There should be no clauses after a |} (only |} only also or END or simple
    1696    // mods)
    1697    //      The order of clauses is not checked
    1698    //      JML only allows forall, old, requires prior to a nesting.