Uses of Class
org.jmlspecs.checker.JmlConstructorDeclaration

Packages that use JmlConstructorDeclaration

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

Methods in org.jmlspecs.checker that return JmlConstructorDeclaration

static JmlConstructorDeclaration

JmlConstructorDeclaration.makeInstance(TokenReference where, long modifiers, String ident, JFormalParameter[] params, CClassType[] exceptions, JConstructorBlock body, JavadocComment javadoc, JavaStyleComment[] comments, JmlMethodSpecification methodSpecification)

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

void	JmlAbstractVisitor.visitJmlConstructorDeclaration(JmlConstructorDeclaration self)
abstract void	JmlVisitor.visitJmlConstructorDeclaration(JmlConstructorDeclaration self)
void	JmlVisitorNI.visitJmlConstructorDeclaration(JmlConstructorDeclaration self)

Uses of JmlConstructorDeclaration in org.jmlspecs.jmlrac

Methods in org.jmlspecs.jmlrac that return JmlConstructorDeclaration

private JmlConstructorDeclaration

TransClass.defaultConstructor() Returns a default constructor for the target class declaration.

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

void	RacPrettyPrinter.visitJmlConstructorDeclaration(JmlConstructorDeclaration self) Prints a JML constructor declaration.
private JmlMethodDeclaration	TransClass.specPublicConstructorAccessor(JmlConstructorDeclaration mdecl) Returns an access method for the given spec_public (or spec_protected) constructor declaration.

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

ConstructorWrapper(String typeName, JmlConstructorDeclaration mdecl)
Construct a new instance.

Uses of JmlConstructorDeclaration in org.jmlspecs.racwrap

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

void	OrigPrettyPrinter.visitJmlConstructorDeclaration(JmlConstructorDeclaration self)
void	WrapperPrettyPrinter.visitJmlConstructorDeclaration(JmlConstructorDeclaration self)