Uses of Class
org.jmlspecs.checker.JmlMapsIntoClause

Packages that use JmlMapsIntoClause

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

Fields in org.jmlspecs.checker declared as JmlMapsIntoClause

private JmlMapsIntoClause[]	JmlFieldDeclaration.mapsIntoGroups
private JmlMapsIntoClause[]	JmlFieldDeclaration.combinedMapsIntoGroups

Methods in org.jmlspecs.checker that return JmlMapsIntoClause

JmlMapsIntoClause[]	JmlFieldDeclaration.mapsIntoClauses()
JmlMapsIntoClause[]	JmlFieldDeclaration.getCombinedMapsIntoClauses()
JmlMapsIntoClause[]	JmlDataGroupAccumulator.getMapsIntoClausesFor(String fieldId)

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

void	JmlAbstractVisitor.visitJmlMapsIntoClause(JmlMapsIntoClause self)
abstract void	JmlVisitor.visitJmlMapsIntoClause(JmlMapsIntoClause self)
void	JmlVisitorNI.visitJmlMapsIntoClause(JmlMapsIntoClause self)
void	JmlDataGroupAccumulator.addMapsInto(JmlMapsIntoClause fieldAssertion)
void	JmlExpressionChecker.visitJmlMapsIntoClause(JmlMapsIntoClause self) Checks visibility (and purity) of the given expression, self.

Uses of JmlMapsIntoClause in org.jmlspecs.jmlrac

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

void	RacPrettyPrinter.visitJmlMapsIntoClause(JmlMapsIntoClause self) Prints a JML maps into data group clause.