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    }