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 }