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

Packages that use JmlAssumeStatement

org.eclipse.jdt.internal.compiler
org.jmlspecs.jml4.esc.gc
org.jmlspecs.jml4.fspv
org.jmlspecs.jml4.rac

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

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

void	ASTVisitor.endVisit(JmlAssumeStatement assertStatement, BlockScope scope)
boolean	ASTVisitor.visit(JmlAssumeStatement assertStatement, BlockScope scope)

Uses of JmlAssumeStatement in org.jmlspecs.jml4.esc.gc

Methods in org.jmlspecs.jml4.esc.gc with parameters of type JmlAssumeStatement

boolean

Ast2SugaredVisitor.visit(JmlAssumeStatement assumeStatement, BlockScope scope)

Uses of JmlAssumeStatement in org.jmlspecs.jml4.fspv

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

void	TraceAstVisitor.endVisit(JmlAssumeStatement assertStatement, BlockScope scope)
boolean	TraceAstVisitor.visit(JmlAssumeStatement assertStatement, BlockScope scope)

Uses of JmlAssumeStatement in org.jmlspecs.jml4.rac

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

void	JmlAstVisitor.endVisit(JmlAssumeStatement assumeStatement, BlockScope scope)
void	DefaultRacAstVisitor.endVisit(JmlAssumeStatement assertStatement, BlockScope scope)
void	AstDirtyBitsRetriever.endVisit(JmlAssumeStatement assertStatement, BlockScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlAssumeStatement assertStatement, BlockScope scope)
boolean	JmlAstVisitor.visit(JmlAssumeStatement assumeStatement, BlockScope scope) Statements which are assumed to be true (in static analysis tools).
boolean	InlineAssertionVisitor.visit(JmlAssumeStatement stmt, BlockScope scope) Overridden here to visit and translate the given JML assume statement into RAC code.
boolean	DefaultRacAstVisitor.visit(JmlAssumeStatement assertStatement, BlockScope scope)
boolean	AstDirtyBitsRetriever.visit(JmlAssumeStatement assertStatement, BlockScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlAssumeStatement assertStatement, BlockScope scope)