    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.ast;
    004
    005
    006    import java.util.Hashtable;
    007
    008    import javafe.ast.*;
    009    import javafe.util.Assert;
    010    import javafe.util.Location;
    011    import escjava.Main;
    012    import escjava.translate.Substitute;
    013
    014
    015    /** This class represents the intermediate method declaration/specification
    016     ** structure used in escjava.translate.GetSpec as described in
    017     ** section 7 of ESCJ 16.
    018     **/
    019
    020    public class DerivedMethodDecl {
    021      /*@ non_null */ public RoutineDecl original;
    022
    023      public FormalParaDeclVec args;
    024      public Type returnType;
    025      public TypeNameVec throwsSet;
    026      public boolean usesFresh;
    027      public ExprModifierPragmaVec requires;
    028      public ModifiesGroupPragmaVec modifies;
    029      public boolean modifiesEverything = false;
    030      public ExprModifierPragmaVec ensures;
    031      public VarExprModifierPragmaVec exsures;
    032      public SimpleModifierPragma nonnull;  // refers to any one of the method's non_null pragmas, or null if none
    033
    034      public DerivedMethodDecl(/*@ non_null */ RoutineDecl rd) {
    035        original = rd;
    036      }
    037
    038      //@ ensures \result == (original instanceof ConstructorDecl);
    039      public boolean isConstructor() {
    040        return original instanceof ConstructorDecl;
    041      }
    042
    043      // The following method should be called only when generating a spec
    044      // for a body, in which case it is known that "body" is not null.
    045      //@ requires original.body != null;
    046      //@ ensures \result ==> (original instanceof ConstructorDecl);
    047      public boolean isConstructorThatCallsSibling() {
    048        if (! isConstructor()) {
    049          return false;
    050        }
    051        if (original.body.getTag() == TagConstants.BLOCKSTMT) {
    052          GenericBlockStmt body = (GenericBlockStmt)original.body;
    053          if (1 <= body.stmts.size()) {
    054            Stmt s0 = body.stmts.elementAt(0);
    055            if (s0.getTag() == TagConstants.CONSTRUCTORINVOCATION) {
    056              ConstructorInvocation ccall = (ConstructorInvocation)s0;
    057              if (ccall.decl.parent == original.parent) {
    058                return true;
    059              }
    060            }
    061          }
    062        }
    063        return false;
    064      }
    065
    066      public boolean isStaticMethod() {
    067        return original instanceof MethodDecl &&
    068               Modifiers.isStatic(original.modifiers);
    069      }
    070
    071      public boolean isInstanceMethod() {
    072        return original instanceof MethodDecl &&
    073               !Modifiers.isStatic(original.modifiers);
    074      }
    075
    076      public boolean isSynchronized() {
    077        return Modifiers.isSynchronized(original.modifiers);
    078      }
    079
    080      public Identifier getId() {
    081        if (original instanceof MethodDecl)
    082          return ((MethodDecl)original).id;
    083        else
    084          return original.parent.id;
    085      }
    086
    087      public TypeDecl getContainingClass() {
    088        return original.parent;
    089      }
    090
    091      public int getRoutineDeclStartLoc() {
    092        return original.getStartLoc();
    093      }
    094
    095      public int getRoutineDeclEndLoc() {
    096        return original.getEndLoc();
    097      }
    098
    099      public void computeFreshUsage() {
    100        usesFresh = false;
    101        if (!Main.options().allocUseOpt) {
    102          // continue as if "fresh" (and hence "alloc") were used
    103          usesFresh = true;
    104          return;
    105        }
    106        if (original instanceof ConstructorDecl) {
    107          // constructors always need to be considered as mentioning "fresh"
    108          usesFresh = true;
    109          return;
    110        }
    111        int n = ensures.size();
    112        for (int i = 0; i < n; i++) {
    113          ExprModifierPragma emp = ensures.elementAt(i);
    114          if (Substitute.mentionsFresh(emp.expr)) {
    115            usesFresh = true;
    116            return;
    117          }
    118        }
    119        n = exsures.size();
    120        for (int i = 0; i < n; i++) {
    121          VarExprModifierPragma vemp = exsures.elementAt(i);
    122          if (Substitute.mentionsFresh(vemp.expr)) {
    123            usesFresh = true;
    124            return;
    125          }
    126        }
    127      }
    128    }