001    /*
002     * Created on Jan 8, 2005
003     *
004     */
005    package escjava.translate;
006    
007    import java.util.Hashtable;
008    import java.util.Iterator;
009    import java.util.LinkedList;
010    import java.util.List;
011    import java.util.NoSuchElementException;
012    
013    import javafe.ast.ASTNode;
014    import javafe.ast.ArrayRefExpr;
015    import javafe.ast.Expr;
016    import javafe.ast.ExprObjectDesignator;
017    import javafe.ast.ExprVec;
018    import javafe.ast.FieldAccess;
019    import javafe.ast.FieldDecl;
020    import javafe.ast.Identifier;
021    import javafe.ast.LiteralExpr;
022    import javafe.ast.ObjectDesignator;
023    import javafe.ast.RoutineDecl;
024    import javafe.ast.SuperObjectDesignator;
025    import javafe.ast.ThisExpr;
026    import javafe.ast.Type;
027    import javafe.ast.TypeDecl;
028    import javafe.ast.TypeObjectDesignator;
029    import javafe.ast.VariableAccess;
030    import javafe.tc.EnvForTypeSig;
031    import javafe.tc.TypeSig;
032    import javafe.util.ErrorSet;
033    import javafe.util.Location;
034    import escjava.Main;
035    import escjava.ast.ArrayRangeRefExpr;
036    import escjava.ast.CondExprModifierPragmaVec;
037    import escjava.ast.EverythingExpr;
038    import escjava.ast.Modifiers;
039    import escjava.ast.ModifiesGroupPragma;
040    import escjava.ast.ModifiesGroupPragmaVec;
041    import escjava.ast.NaryExpr;
042    import escjava.ast.NothingExpr;
043    import escjava.ast.TagConstants;
044    import escjava.ast.WildRefExpr;
045    import escjava.tc.Datagroups;
046    import escjava.tc.FlowInsensitiveChecks;
047    import escjava.tc.TypeCheck;
048    import escjava.tc.Types;
049    
050    
051    /**
052     * @author David Cok
053     *
054     * This class contains methods for handling frame conditions.
055     * <p>
056     * Note the following about the implementation of Modifies Pragmas.
057     * The desugared frame specifications of a method are contained in a
058     * ModifiesGroupPragmaVec, which is a vector of ModifiesGroupPragma elements.
059     * Each ModifiesGroupPragma instance corresponds to the frame conditions for
060     * a single specification case.  Since each specification case of a method
061     * must be independently satisfied, each ModifiesGroupPragma must be 
062     * satisfied.
063     * <p>
064     * A ModifiesGroupPragma contains a precondition (the Expr <obj>.precondition)
065     * and a set of CondExprModifierPragma elements in a CondExprModifierPragmaVec.
066     * Each CondExprModifierPragma corresponds to one store-ref location as might
067     * be listed in an assignable clause (e.g. a field, an array reference, 
068     * wild-card items such as obj.* or array[*], array ranges such as array[i..j]).
069     * The Expr that is in a CondExprModifierPragma is obsolete. [It used to be
070     * that an assignable clause had an optional conditional expression, but that
071     * has been deprecated.] The list of store-refs in a ModifierGroupPragma is
072     * essentially a union - within a specification case a specifier can list 
073     * multiple store-ref locations that may be assigned.  A particular assignment
074     * statement will have a lhs which must match one of the store-ref locations
075     * in the ModifiesGroup Pragma, and must do so for each ModifiesGroupPragma
076     * in the ModifiesGroupPragmaVec.
077     * <p>
078     * 
079     */
080    public class Frame {
081      
082      /** The Translate instance that owns this instance of Frame */
083      final private Translate translator;
084      
085      /** The value of issueCautions obtained from the Translate owner */
086      final private boolean issueCautions;
087      
088      /** The RoutineDecl whose body is in the process of being translated */
089      final private RoutineDecl rdCurrent;
090      
091      /** The mapping to be used for \old variables to get pre-state values */
092      final private Hashtable premap;
093      
094      /** This holds a value across recursive invocations of methods
095       * within this class; it designates that the object whose field
096       * is being assigned is known to be fresh.
097       */
098      private boolean pFreshResult = false;
099      
100      /** A precomputed Identifier for 'this', to be used in constructing
101       *  Expressions.
102       */
103      static private final Identifier thisId = Identifier.intern("this");
104      
105      /** The constructor of a Frame instance; should be called only from
106       *  Translate
107       * @param t The instance of Translate to which this Frame belongs
108       * @param issueCautions Whether to issue Caution messages to the user
109       * @param rdCurrent The RoutineDecl whose body is being translated
110       * @param premap The mapping to pre-state values to be used in translation
111       */
112      public Frame(Translate t, boolean issueCautions, RoutineDecl rdCurrent,
113          Hashtable premap) {
114        translator = t; 
115        this.issueCautions = issueCautions;
116        this.rdCurrent = rdCurrent;
117        this.premap = premap;
118      }
119      
120      // These fields are used in the course of generating checks
121      
122      /** The kind of expression being checked, e.g. assignment or method call.
123       *  Used in the message displayed to the user when the check fails.
124       */
125      private String kindOfModCheck = "assignment";
126      
127      /** This method returns whether the given field (fd) of the given object
128       * (eod) (which is null if the field is static) is definitely not allowed
129       * to be assigned according to the specs of the current RoutineDecl.  By
130       * definitely not allowed, we mean that it can be determined without needing
131       * to prove the truth or falsity of a given expression.  For example, if
132       * the FieldDecl is nowhere mentioned in the ModifiesGroupPragma, then it
133       * definitely may not be assigned.  In a situation where the assignable
134       * clause contained something like <expr>.field where field matches fd,
135       * then the assignment is allowed if <expr> == eod.  But that would have
136       * to be proved: it might be that the assignment is not allowed, if 
137       * <expr> != eod, but we don't definitely know for sure.
138       * @param eod The object whose field is being assigned, or null if the field
139       *    is static
140       * @param fd The declaration corresponding to the field being assigned.
141       * @return true if it is known without a prover that the field may not be
142       *    assigned; false if it may or possibly may be assigned
143       */
144      public boolean isDefinitelyNotAssignable(Expr eod, FieldDecl fd) {
145        definitelyNotAssignable = true;
146        modifiesCheckFieldHelper(eod, Location.NULL, fd,
147            Location.NULL, null, false, null, null, null);
148        boolean r = definitelyNotAssignable;
149        definitelyNotAssignable = false;
150        return r;
151      }
152    
153      /** A private variable used to get information without using the
154       * return value, in support of method isDefinitelylNotAssignable.
155       */
156      private boolean definitelyNotAssignable = false;
157      
158      /** This method generates checks that the field in lhs is allowed to be
159       *  assigned according to the specification of the current RoutineDecl
160       *  (rdCurrent).  This may depend on the object whose field is being
161       *  assigned.  This is called for both static and instance fields.
162       * @param lhs The expression being assigned to (which will be a field
163       *              dereference).
164       * @param callLoc The location of the field access expression (the lhs).
165       * @param fd The location of the declaration of the field being assigned
166       */
167      void modifiesCheckField(Expr lhs, int callLoc, FieldDecl fd) {
168        kindOfModCheck = "assignment";
169        // FIXME - I don't think this handles this and super that are not the
170        // prefix.
171        if (!issueCautions) return;
172        // eod is the object part of the FieldAccess, as in an assigment of the
173        // form  <eod>.<field> = expr;
174        Expr eod = null;
175        if (lhs instanceof NaryExpr) {
176          eod = (Expr)((NaryExpr)lhs).childAt(2);
177        } else if (lhs instanceof VariableAccess) {
178          // static field
179          // eod stays null
180        } else {
181          ErrorSet.caution(callLoc,"INTERNAL ERROR: Unhandled type of lhs in Frame.modifiesCheckField "
182              + lhs.getClass());
183          escjava.ast.EscPrettyPrint.inst.println(System.out,lhs);
184          return;
185        }
186        modifiesCheckFieldHelper(eod,callLoc,fd,Location.NULL,
187            null,false,null,null,null);
188      }
189      
190      /** This is a helper method to generate checks that a particular
191       * field assignment is allowed by the frame conditions.
192       * @param eod The object owning the field being assigned; null if the field
193       *              is static
194       * @param callLoc The location of the field access being assigned to
195       * @param fd   The declaration of the field being assigned to
196       * @param calleeLoc The location of the assignment or method call 
197       * @param callee_tprecondition The precondition under which the callee might
198       *          assign this field; null is equivalent to true
199       * @param genExpr true if an Expr containing the formjula to be checked is
200       *          to be returned, false if checks are to be inserted in the code
201       * @param mg  the set of specifications against which the assignment of the
202       *          field is to be tested
203       * @param thisexpr the expression to be used for 'this' in translating
204       *          input expressions, or null if no translation is to be done
205       * @param args the set of variable mappings to be used in translation
206       * @return the expression that must be true to allow the assignment, if 
207       *    genExpr is true; if genExpr is false, null is returned
208       */
209      private Expr modifiesCheckFieldHelper(Expr eod, int callLoc,
210          FieldDecl fd, int calleeLoc, 
211          Expr callee_tprecondition, boolean genExpr,
212          ModifiesGroupPragmaVec mg,
213          Expr thisexpr, Hashtable args) {
214        
215        // We need to create a translated predicate expression that is true
216        // if the lhs is allowed to be modified and false if it is not
217        // allowed to be modified.  This will be an OR across each of the
218        // modify pragmas.  Each pragma will contribute
219        //   - obviously false if it is not the same declaration or same type
220        //   - obviously true if is is the same declaration and both have 'this'
221        //  as the od and the condition is true
222        //   - obviously true (and then no check) if it is modifies everything
223        //  with a true condition
224        //   - some expression which is the AND of the condition and that
225        //  the lhs matches the modifies expression:
226        //      fields must have the same object designator
227        //      arrays must have the same array expression and same index
228        
229        // Loop over each specification case in turn
230        if (mg == null) mg = GetSpec.getCombinedMethodDecl(rdCurrent).modifies;
231        ExprVec eev = ExprVec.make(mg.size());
232        for (int kk=0; kk<mg.size(); ++kk) {
233          ModifiesGroupPragma mge = mg.elementAt(kk); // The ModifiesGroupPragma
234          // for the current specification case
235          int callerLoc = mge.clauseLoc;  // Location of one of the modifies 
236          // clauses for this specification case
237          // ev collects assertions - if any one of them is true then the
238          // assignment is allowed; if nothing is in it then it is equivalent
239          // to 'false'; if ev is later set to null it means that a literal
240          // 'true' would have been added, so the composite meaning is true
241          ExprVec ev = ExprVec.make(10);
242    
243          // If the field is not a static field, then the assignment is
244          // ok if the owning object is fresh since the pre-state.
245          if (!definitelyNotAssignable && !genExpr && !Modifiers.isStatic(fd.modifiers)) addAllocExpression(ev,eod);
246          // FIXME - why this check on definitelyNotAssignable????
247          
248          // Now iterate over all the store-refs in this specification case,
249          // including store-refs that are in datagroups - we use this
250          // iterator to hide the expansion of the datagroups
251          ModifiesIterator caller_iterator = new ModifiesIterator(
252                                              rdCurrent.parent,mge.items,true);
253          while (ev != null && caller_iterator.hasNext()) {
254            Object ex = caller_iterator.next();
255            if (ex instanceof FieldAccess || ex instanceof FieldDecl) {
256              FieldDecl fdd;
257              ObjectDesignator odd;
258              if (ex instanceof FieldAccess) {
259                fdd = ((FieldAccess)ex).decl;
260                odd = ((FieldAccess)ex).od;
261              } else {
262                fdd = (FieldDecl)ex;
263                odd = null;
264              }
265              if (fd == fdd) {
266                // The declaration for the assigned field is the same as the
267                // declaration in the assignable clause
268                if (Modifiers.isStatic(fd.modifiers)) {
269                  // The matching declarations are static - so they match.
270                  ev = null; 
271                } else {
272                  // Instance references, so the objects need to be equal in order
273                  // for the store-refs to match
274                  Expr e1 = eod;
275                  Expr e2 = odd instanceof ExprObjectDesignator ?
276                      ((ExprObjectDesignator)odd).expr:
277                        ThisExpr.make(null,Location.NULL);
278                  if ( ((e1 instanceof ThisExpr) || 
279                      ((e1 instanceof VariableAccess) && 
280                          ((VariableAccess)e1).id == thisId)) && 
281                          e2 instanceof ThisExpr) {
282                    // The objects references are both 'this'
283                    ev = null;
284                  } else {
285                    // Create a check that the two object references are equal
286                    ExprVec evv = ExprVec.make(1);
287                    evv.addElement(e2);
288                    e1 = eod;
289                    e2 = modTranslate(e2,!genExpr,thisexpr,args);
290                    Expr e = GC.nary(TagConstants.REFEQ,e1,e2);
291                    ev.addElement(e);
292                  }
293                }
294              }
295            } else if (ex instanceof ArrayRefExpr) {
296              // skip - not a match
297            } else if (ex instanceof NothingExpr) {
298              // skip - not a match
299            } else if (ex instanceof EverythingExpr) {
300              // anything matches \everything
301              ev = null;
302            } else if (ex instanceof ArrayRangeRefExpr) {
303              // skip - not a match
304            } else if (ex instanceof WildRefExpr) {
305              ObjectDesignator odd = ((WildRefExpr)ex).od;
306              if (odd instanceof TypeObjectDesignator) {
307                if (Modifiers.isStatic(fd.modifiers)) {
308                  // A static field reference matches <Type>.* if
309                  // the static field is a field of the Type or its subtypes
310                  TypeSig t = TypeCheck.inst.getSig(fd.parent); // type in which the field is declared
311                  Type tt = ((TypeObjectDesignator)odd).type;
312                  if (t == tt || Types.isSubclassOf(tt,t)) {
313                    ev = null;
314                  }
315                } // If not static then is not a match
316              } else if (odd instanceof ExprObjectDesignator) {
317                if (!Modifiers.isStatic(fd.modifiers)) {
318                  // An instance field matches <obj>.* if the 
319                  // object references are equal
320                  Expr e1 = eod;
321                  Expr e2 = modTranslate(((ExprObjectDesignator)odd).expr,
322                      !genExpr,thisexpr,args);
323                  e1 = GC.nary(TagConstants.REFEQ,e1,e2);
324                  ev.addElement(e1);
325                }  // If not an instance reference then not a match
326              } else {
327                ErrorSet.caution("INTERNAL ERROR: Unhandled ObjectDesignator case in modifiesCheckFieldHelper " + odd.getClass());
328                escjava.ast.EscPrettyPrint.inst.println(System.out,odd);
329              }
330            } else {
331              ErrorSet.caution("INTERNAL ERROR: Unhandled case in modifiesCheckFieldHelper " + ex.getClass());
332              escjava.ast.EscPrettyPrint.inst.println(System.out,ex);
333            }
334          }
335          // We have looped over all of the assignable store-refs in the
336          // specification case.  If ev is null, there has been a definite
337          // match and the assignment is ok for this case; if ev is empty
338          // then there is no store-ref that is even a possible match;
339          // otherwise the assignment is ok if the disjunction of the contents of ev
340          // is true - and that needs to be proven by the checker.
341          
342          // Two conditions
343          // if this method has been called on an assignment, we just have
344          //    a callerLoc
345          // if the method has been called on a method call, we have a
346          //    calleeLoc and a callerLoc and we want the calleeLoc to be
347          //    the first associated location
348    
349          // definitelyNotAssignable must be true on return if there is any 
350          // specification case that does not allow the assignment
351     
352          if (definitelyNotAssignable) {
353            //TrAnExpr.closeForClause();
354            // FIXME - why don't we check the preconditions here
355            if (ev != null && ev.size() == 0) return null;
356            
357          } else {
358            
359            Expr e = modChecksComplete(mge.precondition,
360                callee_tprecondition,ev,callLoc,
361                calleeLoc==Location.NULL ? callerLoc : calleeLoc,
362                    calleeLoc==Location.NULL ? Location.NULL: callerLoc, genExpr);
363            if (genExpr && ev != null) eev.addElement(e);
364          }
365        }
366        definitelyNotAssignable = false;
367        return !genExpr ? null : eev.size() == 0 ? null : GC.and(eev);
368      }
369      
370      /* Implementation note on frame conditions when methods are called.
371       * 
372       * We have frame conditions for the callee.  Any store-ref that
373       * might be assigned by the callee at this point in the program
374       * must be allowed to be assigned by the caller.  So we iterate
375       * over each store-ref in each ModifiesGroupPragma in each
376       * specification case of the callee, testing to see whether that
377       * store-ref is allowed to be assigned by the caller.
378       * <p>
379       * There are a couple wrinkles.  First, there is a callee_precondition
380       * that states under what circumstances the callee's store-ref might
381       * possibly be assigned.  Only if that is true does the store-ref need
382       * to be assignable by the caller.
383       * <p>
384       * Second, just because a store-ref is listed as assignable in a spec case
385       * of the callee does not mean that the callee is actually allowed to assign
386       * to it.  Such assignment may be precluded by another spec case of the callee.
387       * For example, given
388       * <pre>
389             requires P;
390             modifies i,j;
391             also
392             requires Q;
393             modifies i,k;
394         </pre>
395       * j may be assigned only if P && !Q, since if Q is true only
396       * i and k, but not j may be assigned.  Thus we have to test each store-ref
397       * of the callee against all of the spec cases of its own specification.
398       */
399      
400      /** This method generates checks that the locations possibly assigned by
401       *  a called method are allowed to be assigned by the caller.
402       * @param calleeFrameConditions the frame conditions of the callee
403       * @param eod the receiver object of the call
404       * @param loccall the location of the call
405       * @param args the mapping of the arguments of the call
406       * @param freshResult - true if eod is known to be fresh since the prestate
407       * @param td_callee The TypeDecl in which the called method is declared
408       */
409      void modifiesCheckMethodI(ModifiesGroupPragmaVec calleeFrameConditions, 
410          Expr eod, int loccall, Hashtable args, boolean freshResult,
411          TypeDecl td_callee) {
412        if (!issueCautions) return;
413        kindOfModCheck = "method call";
414        for (int i=0; i<calleeFrameConditions.size(); ++i) {
415          ModifiesGroupPragma mg = calleeFrameConditions.elementAt(i);
416          // FIXME - the precondition should not be null - guarding against bugs
417          // upstream - e.g. current ArcType, but that may be because of model type problems
418          if (mg.precondition == null) {
419            //System.out.println("ADDING LIT " + Location.toString(mg.clauseLoc));
420            mg.precondition = LiteralExpr.make(TagConstants.BOOLEANLIT, 
421                Boolean.TRUE, Location.NULL);
422            javafe.tc.FlowInsensitiveChecks.setType(mg.precondition,Types.booleanType);
423          }
424          Expr tp = modTranslate(mg.precondition,false,eod,args);
425          ModifiesIterator callee_iterator = new ModifiesIterator(td_callee,mg.items,false);
426          while (callee_iterator.hasNext()) {
427            Object ex = callee_iterator.next();
428            Expr e = modifiesCheckMethod(eod, Location.NULL, 
429                args, false, 
430                ex, 
431                tp,true,calleeFrameConditions);
432            if (e == GC.falselit) {
433              continue;
434            }
435     
436            ModifiesGroupPragmaVec mge = GetSpec.getCombinedMethodDecl(rdCurrent).modifies;
437            modifiesCheckMethod(eod, loccall, 
438                args, freshResult, 
439                ex, 
440                e == null ? tp : GC.and(tp,e),false,mge);
441          }
442        }
443      }
444      
445      /**
446       * Helper method that checks that a particular store-ref in
447       * the frame conditions of a
448       * called method against the frame conditions of the caller.
449       * 
450       * @param eod The receiver object of the called method
451       * @param loccall  The location of the call
452       * @param args  The mapping to be used for callee variables
453       * @param freshResult true if the receiver is known to be fresh (allocated
454       *          since the pre-state of the caller)
455       * @param calleeStoreRef the store-ref of the callee to check
456       * @param callee_tprecondition  The precondition of the store-ref under investigation
457       * @param genExpr if true, an expression is returned that must be true to allow
458       *    the store-ref; if false, a check is created and null is returned
459       * @param mg the caller frame conditions against which to check
460       * @return if genExpr is true, the expression that constitutes the condition
461       *  that must be true if the frame condition is to be allowed is returned;
462       *  if genExpr is false, null is returned (a assertion check is inserted into
463       *  the generated guarded commands)
464       */
465      private Expr modifiesCheckMethod(Expr eod, int loccall, 
466          Hashtable args, 
467          boolean freshResult,
468          Object calleeStoreRef,
469          Expr callee_tprecondition, boolean genExpr,
470          ModifiesGroupPragmaVec mg) {
471        
472        int calleeLoc = ((ASTNode)calleeStoreRef).getStartLoc();
473        pFreshResult = freshResult;
474        ExprVec eev = ExprVec.make(mg.size());
475        try {
476          // Iterating over specification cases
477          for (int kk=0; kk<mg.size(); ++kk) {
478            // Check that ex is assignable for each specification case
479            // in the caller.  Need to issue an error if ex is not assignable;
480            // need to issue a check to be proven if it might or might not be
481            // assignable; can skip the iteration if ex is definitely assignable
482            ModifiesGroupPragma mge = mg.elementAt(kk);
483            int callerLoc = mge.getStartLoc();
484            ExprVec ev = ExprVec.make(10);
485            
486            if (calleeStoreRef instanceof EverythingExpr) {
487              ModifiesIterator caller_iterator = new ModifiesIterator(
488                                                   rdCurrent.parent,mge.items,true);
489              while (caller_iterator.hasNext()) {
490                Object callerStoreRef = caller_iterator.next();
491                if (callerStoreRef instanceof EverythingExpr) {
492                  // calleeStoreRef is \everything but there is also an \everything in 
493                  // the caller, so there is a match
494                  ev = null;
495                  break;
496                }
497              }
498            } else if (calleeStoreRef instanceof NothingExpr) {
499              ev = null; // Anything in the caller will match
500            } else if (calleeStoreRef instanceof FieldAccess) {
501              FieldAccess fa = (FieldAccess)calleeStoreRef;
502              Expr eeod = (fa.od instanceof ExprObjectDesignator) ? 
503                  ((ExprObjectDesignator)fa.od).expr : null;
504              Expr lval = eeod == null ? null 
505                  : modTranslate(eeod, false,  eod, args);
506              
507              Expr e = modifiesCheckFieldHelper(lval,loccall, fa.decl, calleeLoc, 
508                  callee_tprecondition,genExpr,mg,eod,args);
509              if (genExpr && e != null) eev.addElement(e);
510              // A bit of a hack - the FieldHelper routine iterates over
511              // all of the caller frame conditions, so we short-circuit
512              // that here.  Skip the modChecksComplete at the end as well.
513              break;
514            } else if (calleeStoreRef instanceof ArrayRefExpr) {
515              Expr array= modTranslate(((ArrayRefExpr)calleeStoreRef).array, false,  eod, args );
516              Expr index= modTranslate(((ArrayRefExpr)calleeStoreRef).index, false,  eod, args );
517              modifiesCheckArray(array,index,loccall,calleeLoc, callee_tprecondition,
518                  genExpr,mg,eod,args);
519              // A bit of a hack - the helper routine iterates over
520              // all of the caller frame conditions, so we short-circuit
521              // that here.  Skip the modChecksComplete at the end as well.
522              break;
523            } else if (calleeStoreRef instanceof WildRefExpr) {
524              ObjectDesignator odd = ((WildRefExpr)calleeStoreRef).od;
525              Expr e1 = null;
526              if (odd instanceof ExprObjectDesignator) {
527                e1 = modTranslate(((ExprObjectDesignator)odd).expr,
528                    false,eod,args);
529                if (!genExpr) addAllocExpression(ev,e1);
530              }
531              ModifiesIterator caller_iterator = new ModifiesIterator(
532                                                     rdCurrent.parent,mge.items,true);
533              while (caller_iterator.hasNext()) {
534                Object callerStoreRef = caller_iterator.next();
535                //System.out.println("CALLER " + callerStoreRef);
536                if (callerStoreRef instanceof EverythingExpr) {
537                  ev = null;
538                  break;
539                } else if (callerStoreRef instanceof WildRefExpr) {
540                  ObjectDesignator oddd = ((WildRefExpr)callerStoreRef).od;
541                  if ((odd instanceof TypeObjectDesignator) && (oddd instanceof TypeObjectDesignator)) {
542                    Type t = ((TypeObjectDesignator)odd).type;
543                    Type tt = ((TypeObjectDesignator)oddd).type;
544                    if (t == tt || ((t instanceof TypeSig) && Types.isSubclassOf(tt,(TypeSig)t)) ) {
545                      ev = null;
546                      break;
547                    }
548                  } else if (odd instanceof ExprObjectDesignator && oddd instanceof ExprObjectDesignator) {
549                    Expr e2 = modTranslate(((ExprObjectDesignator)oddd).expr,
550                        !genExpr, eod, args);
551                    e1 = GC.nary(TagConstants.REFEQ,e1,e2);
552                    ev.addElement(e1);
553                  } else if (odd instanceof SuperObjectDesignator || oddd instanceof SuperObjectDesignator) {
554                    ErrorSet.caution("INTERNAL ERROR: Unhandled ObjectDesignator in Frame.modifiesCheckMethod: " + odd.getClass());
555                  }
556                }
557              }
558            } else if (calleeStoreRef instanceof ArrayRangeRefExpr) {
559              ArrayRangeRefExpr aexpr = (ArrayRangeRefExpr)calleeStoreRef;
560              Expr array = aexpr.array;
561              Expr lowIndex = aexpr.lowIndex;
562              Expr highIndex = aexpr.highIndex;
563              Expr ao = modTranslate(array,false,eod,args);
564              Expr al = lowIndex == null ? null :
565                modTranslate(lowIndex,false,eod,args); 
566              Expr ah = highIndex == null ? null :
567                modTranslate(highIndex,false,eod,args); 
568              if (!genExpr) addAllocExpression(ev,ao);
569              ModifiesIterator caller_iterator = new ModifiesIterator(
570                                              rdCurrent.parent,mge.items,true);
571              while (caller_iterator.hasNext()) {
572                Object callerStoreRef = caller_iterator.next();
573                if (callerStoreRef instanceof EverythingExpr) {
574                  ev = null;
575                } else if (callerStoreRef instanceof ArrayRangeRefExpr) {
576                  ArrayRangeRefExpr aaexpr = (ArrayRangeRefExpr)callerStoreRef;
577                  Expr aarray = aaexpr.array;
578                  Expr alowIndex = aaexpr.lowIndex;
579                  Expr ahighIndex = aaexpr.highIndex;
580                  Expr aao = modTranslate(aarray,!genExpr,eod,args);
581                  Expr aal = alowIndex == null ? null :
582                    modTranslate(alowIndex,!genExpr,eod,args); 
583                  Expr aah = ahighIndex == null ? null :
584                    modTranslate(ahighIndex,!genExpr,eod,args);
585                  // ao, aao are the callee/caller array expressions
586                  // al, aal are the callee/caller low index expressions, or
587                  //      null if the low index is not specified
588                  // ah, aah are the callee/caller high index expressions, or
589                  //      null if the high index is not specified
590                  // All expressions are already translated
591                  // We need to have the array expressions be equal
592                  // AND   aal <= al  AND ah <= aah
593                  // A null low index is equivalent to 0
594                  // A null high index is equivalent to the length-1
595                  // (since the arrays have to be the same, the lengths can be
596                  // presumed to be the same)
597                  if (ah == null && aah != null) continue; // FIXME - could compare against the length of ao
598                  aao = GC.nary(TagConstants.REFEQ,ao,aao);
599                  aal = aal == null ? null :
600                    GC.nary(TagConstants.INTEGRALLE,aal,
601                        al != null ? al: GC.zerolit);
602                  aah = aah == null ? null :
603                    GC.nary(TagConstants.INTEGRALLE,ah,aah);
604                  aal = aal == null ? aah : aah == null ? aal : GC.and(aal,aah);
605                  aao = aal == null ? aao : GC.and(aao,aal);
606                  ev.addElement(aao);
607                } else if (callerStoreRef instanceof ArrayRefExpr) {
608                  // Here the callee is an array range;
609                  // the caller is an array element; they match if
610                  // the range is just the single element.
611                  // FIXME: Note that we don't find matches of a
612                  // callee array range against the corresponding list
613                  // of individual array elements in the caller (or against
614                  // a list of caller array range store refs that when
615                  // combined match the callee)
616                  if (ah == null) continue; // FIXME - could compare against the length of ao
617                  ArrayRefExpr aaexpr = (ArrayRefExpr)callerStoreRef;
618                  Expr aarray = aaexpr.array;
619                  Expr aindex = aaexpr.index;
620                  Expr aao = modTranslate(aarray,!genExpr,eod,args);
621                  aindex = modTranslate(aindex,!genExpr,eod,args); 
622                  aao = GC.nary(TagConstants.REFEQ,ao,aao);
623                  Expr aal = GC.nary(TagConstants.INTEGRALLE,aindex,
624                      al != null ? al: GC.zerolit);
625                  Expr aah = GC.nary(TagConstants.INTEGRALLE,ah,aindex);
626                  aal = GC.and(aal,aah);
627                  aao = GC.and(aao,aal);
628                  ev.addElement(aao);
629                }
630              }
631            } else {
632              // Leaving ev empty is equivalent to false
633              ErrorSet.caution("INTERNAL ERROR: Modifies Check not implemented for " + calleeStoreRef.getClass());
634            }
635            Expr e = modChecksComplete(mge.precondition,callee_tprecondition,ev,
636                loccall,calleeLoc,callerLoc,genExpr);
637            if (genExpr && e != null) eev.addElement(e);
638          }  // end of iterating over spec cases
639        } finally {
640          pFreshResult = false;
641        }
642        return !genExpr ? null : eev.size() == 0 ? null : GC.and(eev);
643      }
644      
645    
646      /** This adds checks for whether the given array with the given
647       * index may be assigned to.
648       * 
649       * @param array the array object whose element is being assigned
650       * @param arrayIndex the index of the elemtn being assigned
651       * @param callLoc the location of the assignment
652       */  
653      void modifiesCheckArray(Expr array, Expr arrayIndex, int callLoc) {
654        if (!issueCautions) return;
655        kindOfModCheck = "assignment";
656        modifiesCheckArray(array,arrayIndex,callLoc,Location.NULL,null,false,null,null,null);
657      }
658    
659      /** This adds checks for whether the given array with the given
660       * index may be assigned to.
661       * 
662       * @param array the array object whose element is being assigned
663       * @param arrayIndex the index of the elemtn being assigned
664       * @param callLoc the location of the assignment
665       * @param calleeLoc
666       * @param callee_tprecondition The precondition under which the callee might
667       *          assign this array element; null is equivalent to true
668       * @param genExpr true if an Expr containing the formula to be checked is
669       *          to be returned, false if checks are to be inserted in the code
670       * @param mg  the set of specifications against which the assignment of the
671       *          field is to be tested
672       * @param thisexpr the expression to be used for 'this' in translating
673       *          input expressions, or null if no translation is to be done
674       * @param args the set of variable mappings to be used in translation
675       * @return the expression that must be true to allow the assignment, if 
676       *    genExpr is true; if genExpr is false, null is returned
677       */
678      private Expr modifiesCheckArray(Expr array, Expr arrayIndex, 
679          int callLoc, int calleeLoc,
680          Expr callee_tprecondition,
681          boolean genExpr, ModifiesGroupPragmaVec mg,
682          Expr thisexpr, Hashtable args) {
683        
684        if (mg == null) mg = GetSpec.getCombinedMethodDecl(rdCurrent).modifies;
685        ExprVec eev = ExprVec.make(mg.size());
686         
687        // FIXME - I don't think this handles this and super that are not the
688        // prefix.
689    
690        // We need to create a translated predicate expression that is true
691        // if the lhs is allowed to be modified and false if it is not
692        // allowed to be modified.  Each specification case must be
693        // satisfied.  Within a specification case there will be an OR across 
694        // each of the store-ref expressions within the ModifiesGroupPragma
695        // Each store-ref expression will contribute
696        //   - obviously false if it is not the same declaration or same type
697        //   - obviously true in some cases, such as if the store-ref location
698        //      is \everything
699        //   - some expression which is the AND of the condition and that
700        //  the lhs matches the modifies expression:
701        //      fields must have the same object designator
702        //      arrays must have the same array expression and same index
703    
704        for (int kk=0; kk<mg.size(); ++kk) {
705          ModifiesGroupPragma mge = mg.elementAt(kk);
706          int callerLoc = mge.clauseLoc;
707          // The composite condition is the OR of everything in ev.
708          // This is false if there is nothing in ev.
709          // ev is set to null if a literal TRUE would be added
710          ExprVec ev = ExprVec.make(10);
711          // The assignment is ok if the array whose element is assigned
712          // is fresh since the prestate
713          if (!genExpr) addAllocExpression(ev,array); 
714          ModifiesIterator caller_iterator = new ModifiesIterator(
715                                                 rdCurrent.parent,mge.items,true);
716          while (ev != null && caller_iterator.hasNext()) {
717            Object ex = caller_iterator.next();
718            if (ex instanceof FieldAccess) {
719              // skip - no match
720            } else if (ex instanceof FieldDecl) {
721              // skip - no match
722            } else if (ex instanceof ArrayRefExpr) {
723              if (array != null) {  // FIXME - why would array be null?
724                Expr ao = ((ArrayRefExpr)ex).array;
725                Expr ai = ((ArrayRefExpr)ex).index;
726                ao = modTranslate(ao,!genExpr,thisexpr,args);
727                ai = modTranslate(ai,!genExpr,thisexpr,args); 
728                ao = GC.nary(TagConstants.REFEQ,array,ao);
729                ai = GC.nary(TagConstants.INTEGRALEQ,arrayIndex,ai);
730                ao = GC.and(ao,ai);
731                ev.addElement(ao);
732              }
733            } else if (ex instanceof NothingExpr) {
734              // skip - no match
735            } else if (ex instanceof EverythingExpr) {
736              ev = null;
737            } else if (ex instanceof ArrayRangeRefExpr) {
738              if (array != null) { // FIXME - why would array be null?
739                ArrayRangeRefExpr a = (ArrayRangeRefExpr)ex;
740                Expr ao = modTranslate(a.array,!genExpr,thisexpr,args);
741                Expr al = a.lowIndex == null ? null :
742                  modTranslate(a.lowIndex,!genExpr,thisexpr,args); 
743                Expr ah = a.highIndex == null ? null :
744                  modTranslate(a.highIndex,!genExpr,thisexpr,args); 
745                ao = GC.nary(TagConstants.REFEQ,array,ao);
746                al = al == null ? null :
747                  GC.nary(TagConstants.INTEGRALLE,al,arrayIndex);
748                ah = ah == null ? null :
749                  GC.nary(TagConstants.INTEGRALLE,arrayIndex,ah);
750                al = al == null ? ah : ah == null ? al :
751                  GC.and(al,ah);
752                ao = al == null ? ao : GC.and(ao,al);
753                ev.addElement(ao);
754              }
755            } else if (ex instanceof WildRefExpr) {
756              // skip - an array reference does not match against a <obj>.*
757            } else {
758              ErrorSet.caution("INTERNAL ERROR: Unhandled store-ref type in Frame.modifiesCheckArray: " + ex.getClass());
759            }
760          }
761          if (ev != null) {
762            Expr e = modChecksComplete(mge.precondition,
763                callee_tprecondition,ev,callLoc,
764                calleeLoc==Location.NULL ? callerLoc : calleeLoc,
765                    calleeLoc==Location.NULL ? Location.NULL: callerLoc,genExpr);
766            if (genExpr && ev != null) eev.addElement(e);
767          }
768        }
769        return !genExpr ? null : eev.size() == 0 ? null : GC.and(eev);
770      }
771      
772    
773      /** Adds an expression into ev stating that e is allocated now but was
774       * not allocated in the pre-state.  No expression is added to ev if it
775       * is definitely false that e is fresh - such as if e is this or is null
776       * (meaning the field is static).  Otherwise if pFreshResult is true,
777       * a literal True expression is added.  Otherwise some non-trivial 
778       * expression is added.
779       * <p>
780       * Also uses pFreshResult, which must be true iff e is known to be fresh
781       * since the prestate.
782       * @param ev A vector to accumulate assertions
783       * @param e  An expression to be tested for freshness
784       */
785      private void addAllocExpression(ExprVec ev, Expr e) {
786        if (e == null) return;
787        if (e instanceof ThisExpr) return;
788        if ((e instanceof VariableAccess) && 
789            (((VariableAccess)e).id == thisId)) return;
790        if (pFreshResult) {
791          ev.addElement(GC.truelit);
792          return;
793        }
794        ev.addElement (
795            GC.and(
796                GC.nary(TagConstants.ISALLOCATED,e,
797                    TrAnExpr.trSpecExpr(GC.allocvar)),
798                    GC.not(GC.nary(TagConstants.ISALLOCATED,e,
799                        TrAnExpr.trSpecExpr(GC.allocvar,premap,premap)))
800            )
801        );
802      }
803       
804      /**
805       * Generates the actual check with the condition
806       *   'if (precondition && tprecond2) then (disjunction of ev)'
807       * 
808       * @param precondition A precondition, not yet translated
809       * @param tprecond2  A second, already translated, precondition
810       *            (possibly null, meaning true)
811       * @param ev  Disjunction of conditions to be proven; an empty list means false 
812       * @param callLoc  Location of the assignment statement or method call
813       * @param aloc  First associated location, possibly null
814       * @param aloc2  Second associated location, possibly null
815       * @param genExpr if true, returns an Expr that must be true; 
816       *          if false, creates a check for that expression and
817       *          returns null
818       * @return The expr to be proved true, if genExpr is true; if
819       *          genExpr is false, returns null
820       */
821      private Expr modChecksComplete(
822          /*@ non_null */ Expr precondition, 
823          Expr tprecond2, 
824          ExprVec ev, 
825          int callLoc, int aloc, int aloc2, boolean genExpr) {
826        if (ev == null) {
827          // always true, so we don't need to prove anything
828          return genExpr ? GC.truelit : null;
829        }
830    
831        boolean genCheck = true;
832        
833        // Check to see if the modifies check is disabled in general or
834        // for the callLoc or aloc lines - if so just exit
835        if (!genExpr && NoWarn.getChkStatus(TagConstants.CHKMODIFIES,callLoc,aloc==Location.NULL?callLoc:aloc)
836            != TagConstants.CHK_AS_ASSERT) {
837          TrAnExpr.closeForClause();
838          genCheck = false;
839        }
840        // If aloc2 is not null, check to see if the warning is disabled for that
841        // line - if so just exit
842        if (aloc2 != Location.NULL && !genExpr) {
843          if (NoWarn.getChkStatus(TagConstants.CHKMODIFIES,callLoc,aloc2)
844              != TagConstants.CHK_AS_ASSERT) {
845            TrAnExpr.closeForClause();
846            genCheck = false;
847          }
848        }
849        if (!genExpr && !genCheck) return null;
850        
851        Expr tprecondition = modTranslate(precondition,true,null,null);  // FIXME!!!
852        if (tprecond2 != null  && !isTrueLiteral(tprecond2)) {
853          tprecondition = GC.and(tprecondition, tprecond2);
854        }
855    
856        Expr expr = 
857            ev.size() != 0 ? GC.implies(tprecondition,GC.or(ev)) :
858            !isTrueLiteral(tprecondition) ? GC.not(tprecondition) :
859                              GC.falselit;
860        if (genExpr) {
861          // skip generating checks
862        } else if (expr == GC.falselit) {
863          // We need to prove (false), which we know without
864          // benefit of the prover is false - so we immediately issue
865          // an error
866          if (aloc == TagConstants.NULL) {
867            ErrorSet.error(callLoc, 
868              "There is no assignable clause allowing this " +
869              kindOfModCheck);
870          } else {
871            ErrorSet.error(callLoc, 
872                "There is no assignable clause allowing this "
873                + kindOfModCheck,aloc);
874          }
875          if (aloc2 != Location.NULL) ErrorSet.assocLoc(aloc2);
876        } else if (aloc == Location.NULL) {
877          //System.out.println("Generating a modifies check " + ev.size());    
878          translator.addNewAssumptionsNow();
879          translator.addCheck(callLoc,TagConstants.CHKMODIFIES, 
880              expr);
881        } else {
882          //System.out.println("Generating a modifies check " + ev.size());    
883          translator.addNewAssumptionsNow();
884          translator.addCheck(callLoc,TagConstants.CHKMODIFIES, 
885              expr,
886              aloc,aloc2);
887          // FIXME - could also include a list of locations from the caller modifies group
888        }
889        TrAnExpr.closeForClause();
890        return genExpr ? expr : null;
891      }
892      
893      /** Translates the Expr e into guarded commands:<BR>
894       * if old is true, uses the premap to map variables
895       * if old is false, uses args as the variable mapping
896       * 
897       * @param e  the Expr to translate
898       * @param old if true, translates in the context of the pre-state (using the
899       *    mapping in the class field 'premap'
900       * @param thisexpr the Expr to use for 'this'
901       * @param args the mapping to use if old is false (if args is not null)
902       * @return the translated expression
903       */
904      private Expr modTranslate(
905          /*@ non_null */Expr e, 
906          boolean old, 
907          Expr thisexpr, 
908          Hashtable args) {
909        TrAnExpr.initForClause(true);
910        if (old) return TrAnExpr.trSpecExpr(e,premap,premap,null);
911        else if (args == null)  return TrAnExpr.trSpecExpr(e,thisexpr);
912        else     return TrAnExpr.trSpecExpr(e,args,args,thisexpr);
913      }
914      
915      /** A utility function that returns true if the argument 
916       * expression is null or strictly equal to a boolean TRUE.
917       * 
918       * @param p The expression to be tested
919       * @return true if the argument is null or a Boolean LiteralExpr
920       *      with value true
921       */
922      private boolean isTrueLiteral(Expr p) {
923        if (p == null) return true;
924        if (!(p instanceof LiteralExpr)) return false;
925        LiteralExpr lit = (LiteralExpr)p;
926        if (lit.getTag() != TagConstants.BOOLEANLIT) return false;
927        Object value = lit.value;
928        return ((Boolean)value).booleanValue() ;
929      }
930      
931      /** This class enables iterating over the set of store-ref
932       * locations in a ModifiesGroupPragma.  It also has the ability
933       * to include in the iteration the contents of datagroups that
934       * are part of the set of store-ref locations.
935       * 
936       * @author David Cok
937       *
938       */
939      static class ModifiesIterator {
940    
941        /** The TypeDecl whose view of any datagroups is to be used.*/
942        final private TypeDecl td;
943        
944        /** The set of store-ref locations over which to iterate. */
945        final private CondExprModifierPragmaVec mp;
946        
947        /** Fields that have yet to be iterated over.  This
948         * is a list of FieldAccess objects. */
949        final private List others = new LinkedList();
950        
951        /** The datagroups that have already been expanded */
952        final private List done = new LinkedList();
953        
954        /** If true, then datagroups are expanded and their contents
955         * made part of the iteration.
956         */
957        final private boolean expandDatagroups;
958        
959        /** If true, then field wild card store refs (obj.* and
960         * Type.*) are expanded and their contents made part of the
961         * iteration.
962         */
963        final private boolean expandWild;
964        
965        /** An array index into mp */
966        private int i = 0;
967        
968        /** Creates an iterator over the store-ref locations in
969         * the CondExprModifierPragmaVec.  The expandWild parameter
970         * is set false.
971         * @param mp The set of store-ref locations over which to
972         *      iterate
973         * @param expandDatagroups if true, then datagroups are 
974         *      expanded and their contents (recursively) become
975         *      steps in the iteration
976         */
977        public ModifiesIterator(TypeDecl td,
978                    CondExprModifierPragmaVec mp, boolean expandDatagroups) {
979          this(td,mp,expandDatagroups,false);
980        }
981    
982        
983        /** Creates an iterator over the store-ref locations in
984         * the CondExprModifierPragmaVec.
985         * @param mp The set of store-ref locations over which to
986         *      iterate
987         * @param expandDatagroups if true, then datagroups are 
988         *      expanded and their contents (recursively) become
989         *      steps in the iteration
990         * @param expandWild if true, then store-ref expressions
991         *      of the form  obj.* are expanded into their
992         *      individual fields
993         */
994        public ModifiesIterator(TypeDecl td, CondExprModifierPragmaVec mp, 
995            boolean expandDatagroups, boolean expandWild) {
996          this.td = td;
997          this.mp = mp;
998          this.expandDatagroups = expandDatagroups;
999          this.expandWild = expandWild;
1000          i = 0;
1001        }
1002        
1003        /** Resets the iteration back to the beginning */
1004        public void reset() {
1005          i = 0;
1006          others.clear();
1007          done.clear();
1008        }
1009        
1010        /** Returns true if there is more to the iteration 
1011         * @return true if there is more to the iteration
1012         */
1013        public boolean hasNext() {
1014          return i < mp.size() || !others.isEmpty();
1015        }
1016        
1017        /** Returns the next element of the iteration; only valid
1018         * if hasNext returns true, otherwise throws an exception
1019         * @return the next element of the iteration
1020         * @throws NoSuchElementException if there are no more elements
1021         *      in the iteration
1022         */
1023        public Object next() throws NoSuchElementException {
1024          Object ex;
1025          if (!others.isEmpty()) {
1026            ex = others.remove(0);
1027          } else if (i >= mp.size()) {
1028            throw new NoSuchElementException();
1029          } else {
1030            ex = mp.elementAt(i).expr;
1031            ++i;
1032            done.clear();
1033          }
1034          if (ex instanceof FieldAccess) {
1035            if (expandDatagroups) add(((FieldAccess)ex).od,((FieldAccess)ex).decl);
1036          } else if (expandWild && (ex instanceof WildRefExpr)) {
1037            //System.out.println("EXPANDING " + Location.toString(((WildRefExpr)ex).getStartLoc()));
1038            ObjectDesignator od = ((WildRefExpr)ex).od;
1039            addFields(od);
1040          }
1041          
1042          return ex;
1043        }
1044        
1045        /** The maximum number of times to unroll a maps reference. */
1046        private int limit = Main.options().mapsUnrollCount;
1047        // FIXME - should find a better way of testing than using a limited unrolling
1048        
1049        /** Adds all the fields of the od (whether it is a type
1050         * or an object) into the 'others' list as FieldAccess
1051         * items.
1052         * @param od
1053         */
1054        private void addFields(ObjectDesignator od) {
1055          Type type;
1056          boolean stat;
1057          if (od instanceof TypeObjectDesignator) {
1058            type = ((TypeObjectDesignator)od).type;
1059            stat = true;
1060          } else if (od instanceof ExprObjectDesignator) {
1061            type = TypeCheck.inst.getType(((ExprObjectDesignator)od).expr);
1062            stat = false;
1063          } else {
1064            ErrorSet.caution("INTERNAL ERROR: Unhandled ObjectDesignator (od) in ModifiesIterator.addFields: " + od.getClass());
1065            return;
1066          }
1067          if (type instanceof javafe.tc.TypeSig) {
1068            TypeSig ts = (TypeSig)type;
1069            EnvForTypeSig env;
1070            if (stat)
1071              env = (EnvForTypeSig)FlowInsensitiveChecks.staticenvDecoration.get(ts.getTypeDecl());
1072            else
1073              env = (EnvForTypeSig)FlowInsensitiveChecks.envDecoration.get(ts.getTypeDecl());
1074            if (env == null) env = ((TypeSig)type).getEnv(stat);
1075            // The true in the following means all fields are gotten,
1076            // whether or not they are visible or inherited.
1077            // It does also return ghost and model fields.
1078            javafe.ast.FieldDeclVec fds = env.getFields(true);
1079            for (int i=0; i<fds.size(); ++i) {
1080              FieldDecl fd = fds.elementAt(i);
1081              if (stat != Modifiers.isStatic(fd.modifiers)) continue;
1082              FieldAccess fa = FieldAccess.make(od,fd.id,Location.NULL);
1083              fa.decl = fd;
1084              fa = (FieldAccess)javafe.tc.FlowInsensitiveChecks.setType(fa,fd.type);
1085              others.add(fa);
1086              //System.out.println("ADDING " + fd.id + " " + fd.type);
1087            }
1088          } else {
1089            ErrorSet.caution("INTERNAL ERROR: Unhandled Type in ModifiesIterator.addFields: " + type.getClass());
1090          }
1091        }
1092        
1093        /** Adds the contents of the datagroup d (of object od, which
1094         * may not be null) to the 'others' list.
1095         * @param od Object reference
1096         * @param d  Declaration of the datagroup
1097         */
1098        //@ requires od != null && d != null;
1099        private void add(ObjectDesignator od, FieldDecl d) {
1100          if (count(d) >= limit) return;
1101          done.add(d);
1102          if (od == null) {
1103            System.out.println("UNSUPPORTED OPTION IN FRAME.ModifiesIterator");
1104            others.addAll(Datagroups.get(td,d));
1105          } else if (od instanceof TypeObjectDesignator) {
1106            TypeSig ts = (TypeSig)((TypeObjectDesignator)od).type;
1107            TypeDecl tdd = ts.getTypeDecl();
1108            if (TypeSig.getSig(td).isSubtypeOf(ts)) tdd = td;
1109            others.addAll(Datagroups.get(tdd,d));
1110          } else if (od instanceof ExprObjectDesignator) {
1111            Expr e = ((ExprObjectDesignator)od).expr;
1112            Type t = javafe.tc.FlowInsensitiveChecks.getType(e);
1113            TypeDecl tdd = ((TypeSig)t).getTypeDecl();
1114            if (TypeSig.getSig(td).isSubtypeOf((TypeSig)t)) tdd = td;
1115            Iterator i = Datagroups.get(tdd,d).iterator();
1116            // FIXME - need to determine what the permissible content
1117            // of Datagroups.get() is
1118            Hashtable h = new Hashtable();
1119            h.put(Substitute.thisexpr,e);
1120            while (i.hasNext()) {
1121              Object o = i.next();
1122              if (o instanceof FieldDecl) {
1123                ErrorSet.caution("INTERNAL ERROR: Unhandled FieldDecl in ModifiesIterator.add: " + o);
1124              } else if (o instanceof Expr) {
1125                Expr ee = (Expr)o;
1126                ee = Substitute.doSubst(h,ee);
1127                others.add(ee);
1128              } else {
1129                ErrorSet.caution("INTERNAL ERROR: Unhandled case in ModifiesIterator.add: " + o.getClass());
1130              }
1131            }
1132          } else if (od instanceof SuperObjectDesignator) {
1133            TypeSig ts = (TypeSig)((SuperObjectDesignator)od).type;
1134            TypeDecl tdd = ts.getTypeDecl();
1135            if (TypeSig.getSig(td).isSubtypeOf(ts)) tdd = td;
1136            others.addAll(Datagroups.get(tdd,d));
1137          }
1138        }
1139        
1140        /** Returns the number of times the argument is in the 'done'
1141         * list
1142         * @param d Object to be checked
1143         * @return The number of times the argument is in the 'done' list
1144         */
1145        private int count(FieldDecl d) {
1146          int k = 0;
1147          Iterator i = done.iterator();
1148          while (i.hasNext()) {
1149            if (i.next() == d) ++k;
1150          }
1151          return k;
1152        }
1153        
1154      }
1155      
1156    
1157    }