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.