Uses of Class
org.jmlspecs.checker.JmlMethodDeclaration

Packages that use JmlMethodDeclaration

org.jmlspecs.checker	Contains the source code for a parser and typechecker for JML annotations and java code.
org.jmlspecs.jmldoc.jmldoc_142
org.jmlspecs.jmlrac	Generates Java classes from JML specifications that check assertions at runtime.
org.jmlspecs.racwrap

Uses of JmlMethodDeclaration in org.jmlspecs.checker

Subclasses of JmlMethodDeclaration in org.jmlspecs.checker

class

JmlConstructorDeclaration JmlConstructorDeclaration.java

Methods in org.jmlspecs.checker that return JmlMethodDeclaration

static JmlMethodDeclaration	JmlMethodDeclaration.makeInstance(TokenReference where, long modifiers, CTypeVariable[] typevariables, CType returnType, String ident, JFormalParameter[] parameters, CClassType[] exceptions, JBlock body, JavadocComment javadoc, JavaStyleComment[] comments, JmlMethodSpecification methodSpecification)
JmlMethodDeclaration	JmlMethodDeclaration.findDeclWithBody() Returns the method declaration in the refinement chain that has a body.
private JmlMethodDeclaration[]	TestJmlParser.methodDeclsFrom(JmlCompilationUnit unit)

Methods in org.jmlspecs.checker with parameters of type JmlMethodDeclaration

void	JmlAbstractVisitor.visitJmlMethodDeclaration(JmlMethodDeclaration self)
abstract void	JmlVisitor.visitJmlMethodDeclaration(JmlMethodDeclaration self)
private void	JmlTypeDeclaration.combineParameterModifiers(JmlMethodDeclaration meth)
protected void	JmlMethodDeclaration.setRefiningMethod(JmlMethodDeclaration refiningMethod)
void	JmlVisitorNI.visitJmlMethodDeclaration(JmlMethodDeclaration self)
void	JmlAccumSubclassingInfo.visitJmlMethodDeclaration(JmlMethodDeclaration self)
static void	NonNullStatistics.checkSpecification(JmlMethodDeclaration jmd, Object[] jscArr, JmlContext context, String fn)
static void	NonNullStatistics.handleMethodDeclaration(JmlMethodDeclaration jmd, JMethodDeclaration delegee, String fileName, JmlContext context)
static Vector	NonNullStatistics.getSuperSpec(JmlMethodDeclaration jmd, String key)

Uses of JmlMethodDeclaration in org.jmlspecs.jmldoc.jmldoc_142

Methods in org.jmlspecs.jmldoc.jmldoc_142 that return JmlMethodDeclaration

(package private) static JmlMethodDeclaration

JmlHTML.findMatchingMethod(JmlTypeDeclaration jt, JmlMethodDeclaration jm) Looks for method jm in class/interface jt; returns null if not found, otherwise returns the corresponding JmlMethodDeclaration.

Methods in org.jmlspecs.jmldoc.jmldoc_142 with parameters of type JmlMethodDeclaration

(package private) static String	JmlHTML.makeSig(JmlMethodDeclaration m, JmlTypeDeclaration jmltype) This function returns a String giving the signature of a method - the method name and fully qualified argument types, but not formal parameter names.
(package private) static JmlMethodDeclaration	JmlHTML.findMatchingMethod(JmlTypeDeclaration jt, JmlMethodDeclaration jm) Looks for method jm in class/interface jt; returns null if not found, otherwise returns the corresponding JmlMethodDeclaration.
protected void	JmlHTML.insertMethodSpecs(JmlMethodDeclaration jm, String fileString, ArrayList insertions, String sig, JmlTypeDeclaration jmltype) This method generates the specification text for the method jm with signature string sig belonging to class jmltype, and with reference to the original html file in fileString.
String	JmlHTML.generateMethodSpecification(JmlMethodDeclaration jm, CClass cclass, String sig, com.sun.tools.doclets.standard.HtmlStandardWriter writer)
protected boolean	JmlHTML.superSpecification(StringBuffer s, CClass sclass, JmlMethodDeclaration jm, String sig, boolean isclass, com.sun.tools.doclets.standard.HtmlStandardWriter writer) Generates the html for any specifications for the method 'jm' in the super class 'sclass'.

Uses of JmlMethodDeclaration in org.jmlspecs.jmlrac

Subclasses of JmlMethodDeclaration in org.jmlspecs.jmlrac

static class

RacParser.RacMethodDeclaration A RAC node class for representing method declarations.

Fields in org.jmlspecs.jmlrac declared as JmlMethodDeclaration

protected JmlMethodDeclaration	WrapperMethod.methodDecl target method to be wrapped.
protected JmlMethodDeclaration	PreOrPostconditionMethod.methodDecl target method for which assertion method is generated
protected JmlMethodDeclaration	TransMethod.methodDecl target method to be transformed.
protected JmlMethodDeclaration	TransMethodBody.methodDecl method declaration whose body is being translated

Methods in org.jmlspecs.jmlrac that return JmlMethodDeclaration

protected JmlMethodDeclaration	TransType.ghostFieldAccessors(JmlFieldDeclaration fdecl) Returns a pair of ghost field accessor methods (getter and setter) for the given ghost field declaration.
protected JmlMethodDeclaration	TransType.initFlags() Returns declarations of class/instance initialization flags.
private JmlMethodDeclaration	TransType.modelFieldAccessor(JmlSourceField field, JExpression expr) Returns a model accessor method for a model field with the given expression (of the represents clause).
protected JmlMethodDeclaration	TransType.dynamicInvocationMethod() Returns a method declaration that makes a dynamic call to the given method using the Java's reflection facility.
protected JmlMethodDeclaration	TransType.forNameMethod() Returns a method declaration that returns the class object associated with the class or interface with the given string name.
private JmlMethodDeclaration	TransClass.specPublicMethodAccessor(JmlMethodDeclaration mdecl) Returns an access method for the given spec_public (or spec_protected) method declaration, mdecl.
private JmlMethodDeclaration	TransClass.specPublicConstructorAccessor(JmlConstructorDeclaration mdecl) Returns an access method for the given spec_public (or spec_protected) constructor declaration.
protected JmlMethodDeclaration	TransClass.staticInvariantCheckInitializer() Returns a static initializer that checks whether static invariants are established by the initialization of this class.
protected JmlMethodDeclaration	TransClass.constructionStatusAccessor() Returns declarations of a private instance field and a protected access method for storing and accessing the status of an instance construction.
private JmlMethodDeclaration	TransClass.defaultModelFieldAccessor(CField field) Returns a default accessor method for a model field.
private JmlMethodDeclaration	TransClass.modelFieldDelegationMethod(CField field, JmlTypeDeclaration tdecl) Returns a model field delegation method for model field, field, whose represents clause is found in type tdecl.
protected JmlMethodDeclaration	TransClass.specPublicAccessor(CField field) Returns a default access method for a spec_public field.
protected JmlMethodDeclaration	TransClass.assertionInheritanceMethod() Returns a method declaration implementing dynamic inheritance using the Java's reflection facility.
protected JmlMethodDeclaration	TransClass.surrogateCacheDeclaration() Returns a field declaration for an interface surroagte cache with a cache lookup method and a cache update method.
protected JmlMethodDeclaration	TransClass.dynamicInvocationMethod() Returns a method declaration that makes a dynamic call to the given method using the Java's reflection facility.
private JmlMethodDeclaration	TransInterface.specPublicMethodAccessor(JmlMethodDeclaration mdecl) Returns an access method for the given spec_public (or spec_protected) method declaration, mdecl.
private JmlMethodDeclaration	TransInterface.concreteMethod(CMethod mdecl) Returns a concrete (delegation) method that implements the abstract method declaration, mdecl.
private JmlMethodDeclaration	TransInterface.defaultModelFieldAccessor(CField field) Returns a default accessor method for a model field, field.
protected JmlMethodDeclaration	TransInterface.ghostFieldAccessors(JmlFieldDeclaration fdecl) Returns a pair of ghost field accessor methods (getter and setter) for the given ghost field declaration.
protected JmlMethodDeclaration	TransInterface.assertionInheritanceMethod() Returns a method declaration implementing dynamic inheritance using the Java's reflection facility.

Methods in org.jmlspecs.jmlrac with parameters of type JmlMethodDeclaration

static boolean	TransUtils.isMain(JmlMethodDeclaration mdecl) Returns true if the argument is a main method declaration
protected static String	PreOrPostconditionMethod.methodName(JmlMethodDeclaration mdecl) Returns the name of assertion check method to be generated for the given method declaration.
void	RacPrettyPrinter.visitJmlMethodDeclaration(JmlMethodDeclaration self) Prints a JML method declaration.
void	RacPrettyPrinter.visitRacJmlMethodDeclaration(JmlMethodDeclaration self) Prints a JML method declaration in Racc.
protected void	TransType.translateModelMethod(JmlMethodDeclaration mdecl) Translates the given model method (or constructor), mdecl. !
protected abstract void	TransType.translateMethod(JmlMethodDeclaration mdecl) Translates a JML method declaration.
protected abstract void	TransType.addNewMethod(JmlMethodDeclaration mdecl) Adds a new method declaration, mdecl, to the instrumented type.
protected void	TransClass.translateMethod(JmlMethodDeclaration mdecl) Translates a JML method declaration.
protected TransMethod	TransClass.createMethodTranslator(JmlMethodDeclaration mdecl) Creates a method translator for the given method declaration.
protected void	TransClass.translateModelMethod(JmlMethodDeclaration mdecl) Translates the given model method (or constructor), mdecl. !
private JmlMethodDeclaration	TransClass.specPublicMethodAccessor(JmlMethodDeclaration mdecl) Returns an access method for the given spec_public (or spec_protected) method declaration, mdecl.
protected void	TransClass.addNewMethod(JmlMethodDeclaration mdecl) Adds a new method declaration, mdecl, to the instrumented class.
void	TransMethod.perform(JmlMethodDeclaration methodDecl) Peforms translation leaving the results in appropriate instance variables.
protected void	TransInterface.translateMethod(JmlMethodDeclaration mdecl) Translates a JML method declaration.
protected void	TransInterface.translateModelMethod(JmlMethodDeclaration mdecl) Translates the given model method (or constructor), mdecl. !
private JmlMethodDeclaration	TransInterface.specPublicMethodAccessor(JmlMethodDeclaration mdecl) Returns an access method for the given spec_public (or spec_protected) method declaration, mdecl.
protected void	TransInterface.addNewMethod(JmlMethodDeclaration mdecl) Adds a new method declaration, mdecl, to the surrogate class to be generated in the finalization step of this translation.

Constructors in org.jmlspecs.jmlrac with parameters of type JmlMethodDeclaration

WrapperMethod(String typeName, JmlMethodDeclaration mdecl)
Construct a new instance.

PreOrPostconditionMethod(JmlTypeDeclaration typeDecl, JmlMethodDeclaration mdecl, String stackMethod)
Construct a new PreOrPostconditionMethod object.

PostconditionMethod(JmlTypeDeclaration typeDecl, JmlMethodDeclaration mdecl, String restoreMethod)
Construct a new PostconditionMethod object.

ExceptionalPostconditionMethod(JmlTypeDeclaration typeDecl, JmlMethodDeclaration mdecl, String restoreMethod)
Construct a new ExceptionalPostconditionMethod object.

FinalizerWrapper(String typeName, JmlMethodDeclaration mdecl)
Construct a new instance.

PreconditionMethod(JmlTypeDeclaration typeDecl, JmlMethodDeclaration mdecl, boolean hasAssertion, String saveMethod)
Construct a new PreconditionMethod object.

TransMethodBody(VarGenerator varGen, JmlMethodDeclaration mdecl, JTypeDeclarationType typeDecl)
Construct an object of TransMethodBody.

TransConstructorBody(VarGenerator varGen, JmlMethodDeclaration mdecl, JTypeDeclarationType typeDecl)
Construct an object of TransConstructorBody.

Uses of JmlMethodDeclaration in org.jmlspecs.racwrap

Methods in org.jmlspecs.racwrap with parameters of type JmlMethodDeclaration

void	OrigPrettyPrinter.visitJmlMethodDeclaration(JmlMethodDeclaration self)
void	WrapperPrettyPrinter.visitJmlMethodDeclaration(JmlMethodDeclaration self)