Uses of Class
org.jmlspecs.jml4.ast.JmlFreshExpression

Packages that use JmlFreshExpression

org.eclipse.jdt.internal.compiler
org.jmlspecs.jml4.rac

Uses of JmlFreshExpression in org.eclipse.jdt.internal.compiler

Methods in org.eclipse.jdt.internal.compiler with parameters of type JmlFreshExpression

void	ASTVisitor.endVisit(JmlFreshExpression jmlFreshExpression, BlockScope scope)
boolean	ASTVisitor.visit(JmlFreshExpression jmlFreshExpression, BlockScope scope)

Uses of JmlFreshExpression in org.jmlspecs.jml4.rac

Methods in org.jmlspecs.jml4.rac with parameters of type JmlFreshExpression

void	JmlAstVisitor.endVisit(JmlFreshExpression jmlFreshExpression, BlockScope scope)
void	AstDirtyBitsRetriever.endVisit(JmlFreshExpression jmlFreshExpression, BlockScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlFreshExpression jmlFreshExpression, BlockScope scope)
boolean	JmlAstVisitor.visit(JmlFreshExpression jmlFreshExpression, BlockScope scope) Asserts that objects were freshly allocated.
boolean	AstDirtyBitsRetriever.visit(JmlFreshExpression jmlFreshExpression, BlockScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlFreshExpression jmlFreshExpression, BlockScope scope)