|
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 |
||||||||||
PREV NEXT | FRAMES NO FRAMES |
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 |
||||||||||
PREV NEXT | FRAMES NO FRAMES |