Uses of Class
org.jmlspecs.checker.JmlRefinePrefix

Packages that use JmlRefinePrefix

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.

Uses of JmlRefinePrefix in org.jmlspecs.checker

Fields in org.jmlspecs.checker declared as JmlRefinePrefix

private JmlRefinePrefix

JmlCompilationUnit.refinePrefix

Methods in org.jmlspecs.checker that return JmlRefinePrefix

JmlRefinePrefix	JmlCompilationUnit.refinePrefix()
JmlRefinePrefix	JmlParser.jmlRefinePrefix()

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

void	JmlAbstractVisitor.visitJmlRefinePrefix(JmlRefinePrefix self)
abstract void	JmlVisitor.visitJmlRefinePrefix(JmlRefinePrefix self)
void	JmlVisitorNI.visitJmlRefinePrefix(JmlRefinePrefix self)

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

JmlCompilationUnit(TokenReference where, JPackageName packageName, CCompilationUnit export, JPackageImportType[] importedPackages, ArrayList importedUnits, JTypeDeclarationType[] typeDeclarations, ArrayList tlMethods, JmlRefinePrefix refinePrefix)
Constructs a CompilationUnit with the specified top level context

Uses of JmlRefinePrefix in org.jmlspecs.jmlrac

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

void	RacPrettyPrinter.visitJmlRefinePrefix(JmlRefinePrefix self) Prints a JML refine prefix.