Uses of Class
org.jmlspecs.checker.JmlFieldDeclaration

Packages that use JmlFieldDeclaration

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

Methods in org.jmlspecs.checker that return JmlFieldDeclaration

static JmlFieldDeclaration	JmlFieldDeclaration.makeInstance(TokenReference where, JVariableDefinition var, JavadocComment javadoc, JavaStyleComment[] comment, JmlVarAssertion[] varAssertions, JmlDataGroupAccumulator dataGroups)
JmlFieldDeclaration	JmlFieldDeclaration.findDeclWithInitializer() Returns the field declaration in the refinement chain that has an initializer.
private JmlFieldDeclaration[]	TestJmlParser.fieldsFrom(JmlCompilationUnit unit)

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

void	JmlAbstractVisitor.visitJmlFieldDeclaration(JmlFieldDeclaration self)
abstract void	JmlVisitor.visitJmlFieldDeclaration(JmlFieldDeclaration self)
protected void	JmlFieldDeclaration.setRefiningField(JmlFieldDeclaration refiningField)
void	JmlFieldDeclaration.combineDataGroups(JmlFieldDeclaration refField)
void	JmlVisitorNI.visitJmlFieldDeclaration(JmlFieldDeclaration self)
void	JmlAccumSubclassingInfo.visitJmlFieldDeclaration(JmlFieldDeclaration self)

Constructors in org.jmlspecs.checker with parameters of type JmlFieldDeclaration

JmlFieldDeclaration.JmlFieldSpecsContext(CFlowControlContextType parent)

Uses of JmlFieldDeclaration in org.jmlspecs.jmldoc.jmldoc_142

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

void	SpecWriter.visitJmlFieldDeclaration(JmlFieldDeclaration self)

Uses of JmlFieldDeclaration in org.jmlspecs.jmlrac

Methods in org.jmlspecs.jmlrac that return JmlFieldDeclaration

protected JmlFieldDeclaration	TransType.translateField(JmlFieldDeclaration fieldDecl) Translates a JML field declaration, fieldDecl.
protected JmlFieldDeclaration	TransClass.translateField(JmlFieldDeclaration fieldDecl) Translates a JML field declaration, fieldDecl, e.g., handling final, model, spec_public, and spec_protected.
protected JmlFieldDeclaration	TransInterface.translateField(JmlFieldDeclaration fieldDecl) Translates the given JML field declaration, fieldDecl, by specially handling final, model, model, spec_public, and spec_protected fields.

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

void	RacPrettyPrinter.visitJmlFieldDeclaration(JmlFieldDeclaration self) Prints the given JML field declaration.
protected JmlFieldDeclaration	TransType.translateField(JmlFieldDeclaration fieldDecl) Translates a JML field declaration, fieldDecl.
protected JmlMethodDeclaration	TransType.ghostFieldAccessors(JmlFieldDeclaration fdecl) Returns a pair of ghost field accessor methods (getter and setter) for the given ghost field declaration.
protected JmlFieldDeclaration	TransClass.translateField(JmlFieldDeclaration fieldDecl) Translates a JML field declaration, fieldDecl, e.g., handling final, model, spec_public, and spec_protected.
protected JmlFieldDeclaration	TransInterface.translateField(JmlFieldDeclaration fieldDecl) Translates the given JML field declaration, fieldDecl, by specially handling final, model, model, spec_public, and spec_protected fields.
protected JmlMethodDeclaration	TransInterface.ghostFieldAccessors(JmlFieldDeclaration fdecl) Returns a pair of ghost field accessor methods (getter and setter) for the given ghost field declaration.

Uses of JmlFieldDeclaration in org.jmlspecs.racwrap

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

void	OrigPrettyPrinter.visitJmlFieldDeclaration(JmlFieldDeclaration self)
void	WrapperPrettyPrinter.visitJmlFieldDeclaration(JmlFieldDeclaration self)