Uses of Class
org.jmlspecs.checker.JmlTypeDeclaration

Packages that use JmlTypeDeclaration

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 JmlTypeDeclaration in org.jmlspecs.checker

Subclasses of JmlTypeDeclaration in org.jmlspecs.checker

class	JmlClassDeclaration This type represents a java class declaration in the syntax tree.
class	JmlInterfaceDeclaration This class represents a java interface in the syntax tree

Methods in org.jmlspecs.checker that return JmlTypeDeclaration

JmlTypeDeclaration	JmlTypeDeclaration.findTypeWithRepresentsFor(CField field) Finds the applicable representsclause for a given model field by searching through the superclass and interface hierachies starting from the given type declaration.
private JmlTypeDeclaration	JmlTypeDeclaration.checkRedundantRepresents(JmlRepresentsDecl redundantRep, String ident)
JmlTypeDeclaration	JmlTypeLoader.typeDeclarationOf(CClass typ) Returns the JML type declaration corresponding to the given source class; null is returned if no corresponding JML type declaration is found in the database.
JmlTypeDeclaration	JmlTypeLoader.refinedDeclOf(JmlTypeDeclaration cdecl) Returns the refined declaration of a given JML class declaration.

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

void	JmlTypeDeclaration.setRefinedType(JmlTypeDeclaration refinedType) Registers that the given type declaration, refinedType, is refined by this type declaration.
private void	JmlTypeDeclaration.checkForCycles(JmlTypeDeclaration refinedType) Sets the refinedType field of this JmlTypeDeclaration object.
private void	JmlTypeDeclaration.setRefiningType(JmlTypeDeclaration refiningDecl)
protected void	JmlAccumSubclassingInfo.visitClassBody(JmlTypeDeclaration self)
void	JmlTypeLoader.addTypeDeclAST(JmlTypeDeclaration decl) Adds a JML type declaration into the database.
JmlTypeDeclaration	JmlTypeLoader.refinedDeclOf(JmlTypeDeclaration cdecl) Returns the refined declaration of a given JML class declaration.
JmlInterfaceDeclaration[]	JmlTypeLoader.interfacesOf(JmlTypeDeclaration typeDecl) Returns the interfaces of a given JML type declaration.

Uses of JmlTypeDeclaration in org.jmlspecs.jmldoc.jmldoc_142

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

protected void	JmlHTML.classSpecs(JmlTypeDeclaration jmltype, StringBuffer sb, boolean inherited, String title) This method generates the html describing the specifications of class/interface jmltype.
protected String	JmlHTML.generateClassSpecification(JmlTypeDeclaration jmltype, com.sun.tools.doclets.standard.HtmlStandardWriter writer) This generates the full html insert for the class level specifications, including those for any super classes and including the leading jmlbegin and jmlend strings.
(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(JmlTypeDeclaration jmltype, String fileString, ArrayList insertions) This method generates the html text for the specifications of the methods for type jmlType, with reference to the original file content in fileString.
protected void	JmlHTML.insertFieldSpecs(JmlTypeDeclaration jmltype, String fileString, ArrayList insertions) This method generates the html text for the specifications of the fields for type jmlType, with reference to the original file content in fileString.
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.

Uses of JmlTypeDeclaration in org.jmlspecs.jmlrac

Fields in org.jmlspecs.jmlrac declared as JmlTypeDeclaration

protected JmlTypeDeclaration	AssertionMethod.typeDecl target type declaration for generating assertion methods
private JmlTypeDeclaration	TransInvariant.typeDecl taget type declaration that has this invariant specification.
protected JmlTypeDeclaration	TransType.typeDecl Target type declaration to be translated.
protected JmlTypeDeclaration	TransMethod.typeDecl Target type declaration whose methods are to be translated.
private JmlTypeDeclaration	TransConstraint.typeDecl The host type declaration containing the target constraint clause to be translated by this translator.

Methods in org.jmlspecs.jmlrac that return JmlTypeDeclaration

protected JmlTypeDeclaration

TransType.findTypeWithRepresentsFor(JmlTypeDeclaration tdecl, CField field) Finds the applicable representsclause for a given model field by searching through the superclass and interface hierachies starting from the given type declaration.

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

static String	TransUtils.evalOldName(JmlTypeDeclaration tdecl, boolean isStatic) Returns the name of an old-expression evaluation method for the type declaration.
static boolean	Main.isSpecMode(JmlTypeDeclaration decl) Returns true if this type should be processed in spec mode - that is if methods and constructors without bodies are allowed.
static String	LocalConstraintMethod.postfix(boolean isStatic, JmlTypeDeclaration typeDecl, int suffix) Returns the postfix to be used for constraint check method's name.
private static String	MotherConstraintMethod.postfix(boolean isStatic, JmlTypeDeclaration typeDecl) Returns the postfix to be used for constraint check method's name.
protected void	RacPrettyPrinter.visitClassBody(JmlTypeDeclaration self) Prints a JML type declaration.
static String	SubtypeConstraintMethod.postfix(JmlTypeDeclaration tdecl, boolean forWeakSubtype) Returns the postfix to be used for constraint check method's name.
protected JmlTypeDeclaration	TransType.findTypeWithRepresentsFor(JmlTypeDeclaration tdecl, CField field) Finds the applicable representsclause for a given model field by searching through the superclass and interface hierachies starting from the given type declaration.
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.

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

TransInvariant(JmlTypeDeclaration typeDecl, VarGenerator varGen)
Constructs a TransInvariant object.

InvariantLikeMethod(boolean isStatic, JmlTypeDeclaration typeDecl)
Construct a new InvariantLikeMethod object.

ConstraintMethod(boolean isStatic, JmlTypeDeclaration typeDecl, String postfix)
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.

InvariantMethod(boolean isStatic, JmlTypeDeclaration typeDecl)
Construct a new InvariantMethod object.

LocalConstraintMethod(VarGenerator varGen, boolean isStatic, JmlTypeDeclaration typeDecl, JmlMethodName[] names, int suffix)
Construct a new instance.

MotherConstraintMethod(boolean isStatic, JmlTypeDeclaration typeDecl, List restoreMethods)
Construct a new instance.

MotherConstraintMethod(boolean isStatic, JmlTypeDeclaration typeDecl, String postfix, List restoreMethods)
Construct a new instance.

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

SubtypeConstraintMethod(JmlTypeDeclaration tdecl, boolean forWeakSubtype, List restoreMethods)
Construct a new instance.

TransType(JmlTypeDeclaration typeDecl)
Constructs a TransType object.

TransMethod(JmlTypeDeclaration typeDecl, VarGenerator varGen)
Constructs a new TransMethod object.

TransConstraint(JmlTypeDeclaration typeDecl, VarGenerator varGen)
Constructs a TransConstraint object.

TransConstructor(JmlTypeDeclaration typeDecl, VarGenerator varGen)
Construct a new TransConstructor object.

Uses of JmlTypeDeclaration in org.jmlspecs.racwrap

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

void	FactoryPrinter.print_class(JmlTypeDeclaration clazz)
void	FactoryPrinter.printConstructor(JmlTypeDeclaration clazz, JMethodDeclarationType method) This prints out the factory method that corresponds to a constructor in the original object.
private void	InterfacePrinter.print_class(JmlTypeDeclaration clazz)
protected void	WrapperPrettyPrinter.visitClassBody(JmlTypeDeclaration self) Prints the body of the class.