Uses of Class
org.jmlspecs.checker.JmlFreshExpression

Packages that use JmlFreshExpression

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.jmlrac.qexpr	Translates JML quantified expressions into Java source code to evaluate them at runtime.

Uses of JmlFreshExpression in org.jmlspecs.checker

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

void	JmlAbstractVisitor.visitJmlFreshExpression(JmlFreshExpression self)
abstract void	JmlVisitor.visitJmlFreshExpression(JmlFreshExpression self)
void	JmlVisitorNI.visitJmlFreshExpression(JmlFreshExpression self)
void	JmlExpressionChecker.visitJmlFreshExpression(JmlFreshExpression self) Checks visibility (and purity) of the given expression, self.
private static void	NonNullStatistics.handleFreshExpression(JmlFreshExpression jf, JmlContext context, int clause, String fn)

Uses of JmlFreshExpression in org.jmlspecs.jmldoc.jmldoc_142

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

void	SpecWriter.visitJmlFreshExpression(JmlFreshExpression self)

Uses of JmlFreshExpression in org.jmlspecs.jmlrac

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

void	RacPrettyPrinter.visitJmlFreshExpression(JmlFreshExpression self) Prints a JML fresh expression.
void	TransExpression.visitJmlFreshExpression(JmlFreshExpression self) Translates a JML \fresh expression.
void	TransExpression2.visitJmlFreshExpression(JmlFreshExpression self) Translates a JmlFreshExpression expression.

Uses of JmlFreshExpression in org.jmlspecs.jmlrac.qexpr

Methods in org.jmlspecs.jmlrac.qexpr with parameters of type JmlFreshExpression

void	AbstractExpressionVisitor.visitJmlFreshExpression(JmlFreshExpression self) Visits the given fresh expression, self.