Uses of Class
org.jmlspecs.checker.JmlVariantFunction

Packages that use JmlVariantFunction

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

Fields in org.jmlspecs.checker declared as JmlVariantFunction

private JmlVariantFunction[]

JmlLoopStatement.variantFunctions

Methods in org.jmlspecs.checker that return JmlVariantFunction

JmlVariantFunction[]	JmlLoopStatement.variantFunctions()
JmlVariantFunction[]	JmlParser.jmlVariantFunctionList()
JmlVariantFunction	JmlParser.jmlVariantFunction()

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

void	JmlAbstractVisitor.visitJmlVariantFunction(JmlVariantFunction self)
abstract void	JmlVisitor.visitJmlVariantFunction(JmlVariantFunction self)
void	JmlVisitorNI.visitJmlVariantFunction(JmlVariantFunction self)

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

JmlLoopStatement(TokenReference where, JmlLoopInvariant[] loopInvariants, JmlVariantFunction[] variantFunctions, JStatement stmt, JavaStyleComment[] comments)
Constructs a new instance with the given arguments.

Uses of JmlVariantFunction in org.jmlspecs.jmlrac

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

void	RacPrettyPrinter.visitJmlVariantFunction(JmlVariantFunction self) Prints a JML variant function.
private RacNode	TransMethodBody.variantCheckCode(JmlVariantFunction[] vars) Returns code that checks the given loop variants.