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