ESC/Java2
© 2003,2004,2005 David Cok and Joseph Kiniry
© 2005 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

Uses of Class
javafe.ast.RoutineDecl

Packages that use RoutineDecl
escjava   
escjava.ast   
escjava.backpred   
escjava.gui   
escjava.tc   
escjava.translate   
javafe.ast   
javafe.reader   
javafe.tc   
 

Uses of RoutineDecl in escjava
 

Methods in escjava with parameters of type RoutineDecl
(package private)  boolean RefinementSequence.match(RoutineDecl newrd, RoutineDecl rd)
           
(package private)  void RefinementSequence.combineRoutine(RoutineDecl newrd, RoutineDecl rd)
           
private  java.lang.String Main.processRoutineDecl(RoutineDecl r, TypeSig sig, InitialState initState)
          Run stages 3+..6 as requested on a RoutineDeclElem; returns a short (~ 1 word) status message.
 int Main.doProving(Expr vc, RoutineDecl r, Set directTargets, FindContributors scope)
           
protected  GuardedCmd Main.computeBody(RoutineDecl r, InitialState initState)
          This method computes the guarded command (including assuming the precondition, the translated body, the checked postcondition, and the modifies constraints) for the method or constructor r in scope scope.
protected  void AnnotationHandler.process(RoutineDecl tde)
           
 void AnnotationHandler.desugar(RoutineDecl tde)
           
static void AnnotationHandler.printSpecs(RoutineDecl tde)
           
protected  ModifierPragmaVec AnnotationHandler.desugarAnnotations(ModifierPragmaVec pm, RoutineDecl tde)
           
 void AnnotationHandler.checkSignalsOnly(ModifierPragmaVec mpv, RoutineDecl tde)
           
 ModifierPragmaVec AnnotationHandler.getNonNull(RoutineDecl rd)
           
 ModifierPragmaVec AnnotationHandler.desugar(java.util.ArrayList ps, RoutineDecl tde)
           
 void AnnotationHandler.desugar(ModifierPragmaVec m, java.util.ArrayList requiresList, ModifierPragmaVec resultList, RoutineDecl tde)
           
static VarExprModifierPragma AnnotationHandler.defaultSignalsOnly(RoutineDecl tde, Expr req)
           
static ModifiesGroupPragma AnnotationHandler.defaultModifies(int loc, Expr req, RoutineDecl rd)
           
 void AnnotationHandler.NestedPragmaParser.parseRoutineSpecs(RoutineDecl rd)
           
 

Uses of RoutineDecl in escjava.ast
 

Fields in escjava.ast declared as RoutineDecl
 RoutineDecl ParsedSpecs.decl
           
 RoutineDecl DerivedMethodDecl.original
           
 RoutineDecl Call.rd
           
 

Methods in escjava.ast with parameters of type RoutineDecl
static boolean Utils.isPure(RoutineDecl rd)
           
static void Utils.setPure(RoutineDecl rd)
           
static ModifierPragma Utils.findPurePragma(RoutineDecl rd)
           
static boolean Utils.isAllocates(RoutineDecl rd)
           
static boolean Utils.isFunction(RoutineDecl rd)
           
static ModifierPragmaVec Utils.getAllSpecs(RoutineDecl rd)
           
static ModifierPragmaVec Utils.getInheritedSpecs(RoutineDecl rd)
           
static ModifierPragmaVec Utils.addInheritedSpecs(RoutineDecl rd, ModifierPragmaVec mp)
           
static ParsedSpecs ParsedSpecs.make(RoutineDecl decl, ParsedRoutineSpecs specs)
           
 

Constructors in escjava.ast with parameters of type RoutineDecl
DerivedMethodDecl(RoutineDecl rd)
           
 

Uses of RoutineDecl in escjava.backpred
 

Methods in escjava.backpred with parameters of type RoutineDecl
private  boolean FindContributors.isNonRecursiveHelperInvocation(RoutineDecl r)
          Returns true if and only if r is a helper routine that has not been visited by this FindContributor object.
private  void FindContributors.backedgeToRoutineDecl(RoutineDecl rd, FieldDeclVec fields, boolean addTypes, int inlined, java.util.LinkedList visited)
          Calculate the fields and types "mentioned" by a backedge to a RoutineDecl and then add them as per walk(,,).
 

Constructors in escjava.backpred with parameters of type RoutineDecl
FindContributors(RoutineDecl rd)
          Generate the contributors for a given RoutineDecl.
 

Uses of RoutineDecl in escjava.gui
 

Fields in escjava.gui declared as RoutineDecl
 RoutineDecl GUI.RDTreeValue.rd
           
 

Methods in escjava.gui with parameters of type RoutineDecl
static javax.swing.tree.DefaultMutableTreeNode GUI.RDTreeValue.makeNode(RoutineDecl rd)
           
 

Constructors in escjava.gui with parameters of type RoutineDecl
GUI.RDTreeValue(RoutineDecl rd)
           
 

Uses of RoutineDecl in escjava.tc
 

Methods in escjava.tc with parameters of type RoutineDecl
static boolean FlowInsensitiveChecks.isMethodOverride(RoutineDecl rd)
           
static int FlowInsensitiveChecks.getOverrideStatus(RoutineDecl rd)
           
static MethodDecl FlowInsensitiveChecks.getSuperNonNullStatus(RoutineDecl rd, int j)
           
static MethodDecl FlowInsensitiveChecks.getSuperNonNullStatus(RoutineDecl rd, int j, Set directOverrides)
           
 

Uses of RoutineDecl in escjava.translate
 

Fields in escjava.translate declared as RoutineDecl
private  RoutineDecl Translate.rdCurrent
          References the routine currently being checked by trBody.
private  RoutineDecl Frame.rdCurrent
          The RoutineDecl whose body is in the process of being translated
 

Methods in escjava.translate with parameters of type RoutineDecl
 GuardedCmd Translate.trBody(RoutineDecl rd, FindContributors scope, java.util.Hashtable premap, Set predictedSynTargs, Translate inlineParent, boolean issueCautions)
          Translates the body of a method or constructor, as described in ESCJ 16, section 8.
private  boolean Translate.isStandaloneConstructor(RoutineDecl rd)
           
private  boolean Translate.isRecursiveInvocation(RoutineDecl r)
           
private  Call Translate.call(RoutineDecl rd, ExprVec argsRaw, ExprVec args, FindContributors scope, int scall, int ecall, int locOpenParen, boolean superOrSiblingConstructorCall, InlineSettings inline, Expr eod, boolean freshResult)
          Creates and desugars a call node, extended to allow the possibility of inlining a call.
private  InlineSettings Translate.computeInlineSettings(RoutineDecl rd, ExprVec argsRaw, InlineSettings inline, int scall)
          Computes the inlining settings for a given call.
static Expr TrAnExpr.resultEqualsCall(GenericVarDecl vd, RoutineDecl rd, java.util.Hashtable sp)
           
static void TrAnExpr.getCalledSpecs(RoutineDecl decl, ObjectDesignator od, ExprVec ev, Expr resultVar, java.util.Hashtable sp, java.util.Hashtable st)
           
static Identifier TrAnExpr.fullName(RoutineDecl rd, boolean useSuper)
           
private static java.util.ArrayList TrAnExpr.makeBounds(RoutineDecl rd, GenericVarDecl newThis)
           
private static Expr TrAnExpr.createFunctionCall(RoutineDecl rd, java.util.ArrayList bounds, java.util.Hashtable sp)
           
(package private) static java.lang.String Suggestion.generate(int warningTag, java.lang.Object auxInfo, RoutineDecl rd, Set directTargets, SList cc, int locDecl)
           
private static java.lang.String Suggestion.gNull(VarInit E, RoutineDecl rd)
           
private static java.lang.String Suggestion.gNeg(VarInit E, RoutineDecl rd, Set directTargets)
           
private static java.lang.String Suggestion.gArrStore(VarInit E, RoutineDecl rd)
           
private static java.lang.String Suggestion.gInvariant(Expr E, RoutineDecl rd, SList cc, int locDecl)
           
private static Type InlineConstructor.copyType(Type t, RoutineDecl rd)
           
private static TypeName InlineConstructor.copyTypeName(TypeName tn, RoutineDecl rd)
           
private static Name InlineConstructor.copyName(Name n, RoutineDecl rd)
           
static boolean Helper.isHelper(RoutineDecl r)
          Provides support for appropriately handling the 'helper' pragma during translation.
static void Helper.abort(RoutineDecl rd)
           
static Spec GetSpec.getSpecForCall(RoutineDecl rd, FindContributors scope, Set predictedSynTargs)
           
static Spec GetSpec.getSpecForInline(RoutineDecl rd, FindContributors scope)
           
static Spec GetSpec.getSpecForBody(RoutineDecl rd, FindContributors scope, Set synTargs, java.util.Hashtable premap)
           
private static Spec GetSpec.getCommonSpec(RoutineDecl rd, FindContributors scope, java.util.Hashtable premap)
           
static DerivedMethodDecl GetSpec.getCombinedMethodDecl(RoutineDecl rd)
          * Implement GetCombinedMethodDecl from ESCJ 16c section 7: * * Precondition: the type declaring rd has been typechecked.
private static void GetSpec.addModifiersToDMD(DerivedMethodDecl dmd, RoutineDecl rd)
          * Add the modifiers of rd to dmd, making any necessary substitions * of parameter names.
static void ErrorMsg.print(java.lang.String name, SList labelList, SList counterexampleContext, RoutineDecl rd, Set directTargets, java.io.PrintStream out)
          Prints an error message for proof obligation name, where labelList and counterexampleContext are labels and counterexample from Simplify.
private static void ErrorMsg.printErrorMessage(java.lang.String s, SList counterexampleContext, RoutineDecl rd, Set directTargets, java.io.PrintStream out, boolean assocOnly)
          Parses s and prints a nice error message to out.
 

Constructors in escjava.translate with parameters of type RoutineDecl
RepHelper(TypeDecl td, RoutineDecl rd)
           
Frame(Translate t, boolean issueCautions, RoutineDecl rdCurrent, java.util.Hashtable premap)
          The constructor of a Frame instance; should be called only from Translate
 

Uses of RoutineDecl in javafe.ast
 

Subclasses of RoutineDecl in javafe.ast
 class ConstructorDecl
          Represents a ConstructorDeclaration.
 class MethodDecl
           
 

Methods in javafe.ast with parameters of type RoutineDecl
 java.lang.Object VisitorArgResult.visitRoutineDecl(RoutineDecl x, java.lang.Object o)
           
 void Visitor.visitRoutineDecl(RoutineDecl x)
           
 void DefaultVisitor.visitRoutineDecl(RoutineDecl x)
           
 

Uses of RoutineDecl in javafe.reader
 

Fields in javafe.reader declared as RoutineDecl
private  RoutineDecl[] ASTClassFileParser.routines
          The methods and constructors of the class being parsed.
 

Uses of RoutineDecl in javafe.tc
 

Methods in javafe.tc with parameters of type RoutineDecl
static boolean Types.routineMoreSpecific(RoutineDecl x, RoutineDecl y)
           
static java.lang.String TypeCheck.getSignature(RoutineDecl r)
          Construct a String listing the signature of a RoutineDecl, omitting the return type and throws causes if any.
 java.lang.String TypeCheck.getName(RoutineDecl r)
          Returns the user-readable name for a RoutineDecl.
 java.lang.String TypeCheck.getRoutineName(RoutineDecl r)
          Returns the user-readable simple name for a RoutineDecl.
 


ESC/Java2
© 2003,2004,2005 David Cok and Joseph Kiniry
© 2005 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

The ESC/Java2 Project Homepage