Uses of Class
org.jmlspecs.checker.JmlClassDeclaration

Packages that use JmlClassDeclaration

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

Uses of JmlClassDeclaration in org.jmlspecs.checker

Methods in org.jmlspecs.checker that return JmlClassDeclaration

static JmlClassDeclaration	JmlClassDeclaration.makeInstance(TokenReference where, long modifiers, String ident, CTypeVariable[] typevariables, CClassType superType, boolean isWeakSubtype, CClassType[] interfaces, boolean[] interfaceWeaklyFlags, ArrayList methods, ArrayList inners, JPhylum[] fieldsAndInits, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JavadocComment javadoc, JavaStyleComment[] comment, boolean isRefinedType) Constructs a class declaration in the parsing tree.
JmlClassDeclaration	JmlTypeLoader.superClassOf(JmlClassDeclaration cdecl) Returns the superclass of a given JML class declaration.
JmlClassDeclaration	JmlTypeLoader.superClassOf(CClass cls) Returns the superclass of a given JML class declaration.

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

void	JmlAbstractVisitor.visitJmlClassDeclaration(JmlClassDeclaration self)
abstract void	JmlVisitor.visitJmlClassDeclaration(JmlClassDeclaration self)
void	JmlVisitorNI.visitJmlClassDeclaration(JmlClassDeclaration self)
void	JmlAccumSubclassingInfo.visitJmlClassDeclaration(JmlClassDeclaration self)
JmlClassDeclaration	JmlTypeLoader.superClassOf(JmlClassDeclaration cdecl) Returns the superclass of a given JML class declaration.

Uses of JmlClassDeclaration in org.jmlspecs.jmlrac

Fields in org.jmlspecs.jmlrac declared as JmlClassDeclaration

private JmlClassDeclaration

TransClass.classDecl Target class declaration to be translated.

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

void	JmlRacGenerator.visitJmlClassDeclaration(JmlClassDeclaration self) Translate a JML class declaration.
void	RacPrettyPrinter.visitJmlClassDeclaration(JmlClassDeclaration self) Prints a JML class declaration.

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

TransClass(JmlClassDeclaration classDecl)
Constructs a TransClass object.

Uses of JmlClassDeclaration in org.jmlspecs.racwrap

Fields in org.jmlspecs.racwrap declared as JmlClassDeclaration

JmlClassDeclaration

WrapperPrettyPrinter.current_class

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

void	OrigPrettyPrinter.visitJmlClassDeclaration(JmlClassDeclaration self) Prints the modified class declaration of the orig file.
void	WrapperPrettyPrinter.visitJmlClassDeclaration(JmlClassDeclaration self) Prints the wrapper declaration