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

Packages that use JmlEnsuresClause

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

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

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

void	ASTVisitor.endVisit(JmlEnsuresClause ensuresClause, BlockScope scope)
boolean	ASTVisitor.visit(JmlEnsuresClause ensuresClause, BlockScope scope)

Uses of JmlEnsuresClause in org.jmlspecs.eclipse.jdt.internal.esc2

Methods in org.jmlspecs.eclipse.jdt.internal.esc2 with parameters of type JmlEnsuresClause

boolean

PrintVisitor.visit(JmlEnsuresClause ensuresClause, BlockScope scope) Deprecated.

Uses of JmlEnsuresClause in org.jmlspecs.jml4.fspv

Methods in org.jmlspecs.jml4.fspv with parameters of type JmlEnsuresClause

void	TraceAstVisitor.endVisit(JmlEnsuresClause ensuresClause, BlockScope scope)
boolean	TraceAstVisitor.visit(JmlEnsuresClause ensuresClause, BlockScope scope)

Uses of JmlEnsuresClause in org.jmlspecs.jml4.rac

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

void	JmlAstVisitor.endVisit(JmlEnsuresClause ensuresClause, BlockScope scope)
void	DefaultRacAstVisitor.endVisit(JmlEnsuresClause ensuresClause, BlockScope scope)
void	AstDirtyBitsRetriever.endVisit(JmlEnsuresClause ensuresClause, BlockScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlEnsuresClause ensuresClause, BlockScope scope)
boolean	JmlAstVisitor.visit(JmlEnsuresClause ensuresClause, BlockScope scope) An ensures clause specifies a normal postcondition, i.e., a property that is guaranteed to hold at the end of the method (or constructor) invocation in the case that this method (or constructor) invocation returns without throwing an exception.
boolean	DefaultRacAstVisitor.visit(JmlEnsuresClause ensuresClause, BlockScope scope)
boolean	AstDirtyBitsRetriever.visit(JmlEnsuresClause ensuresClause, BlockScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlEnsuresClause ensuresClause, BlockScope scope)