    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    }