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

Packages that use JmlLoopAnnotations

org.eclipse.jdt.internal.compiler
org.jmlspecs.jml4.ast
org.jmlspecs.jml4.fspv
org.jmlspecs.jml4.fspv.phases
org.jmlspecs.jml4.rac

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

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

void	ASTVisitor.endVisit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
boolean	ASTVisitor.visit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)

Uses of JmlLoopAnnotations in org.jmlspecs.jml4.ast

Fields in org.jmlspecs.jml4.ast declared as JmlLoopAnnotations

JmlLoopAnnotations	JmlWhileStatement.annotations
JmlLoopAnnotations	JmlForStatement.annotations
JmlLoopAnnotations	JmlForeachStatement.annotations
JmlLoopAnnotations	JmlDoStatement.annotations

Constructors in org.jmlspecs.jml4.ast with parameters of type JmlLoopAnnotations

JmlDoStatement(JmlLoopAnnotations annotations, Expression condition, Statement action, int sourceStart, int sourceEnd)

JmlForeachStatement(JmlLoopAnnotations annotations, LocalDeclaration elementVariable, int start)

JmlForStatement(JmlLoopAnnotations annotations, Statement[] initializations, Expression condition, Statement[] increments, Statement action, boolean neededScope, int s, int e)

JmlWhileStatement(JmlLoopAnnotations annotations, Expression condition, Statement action, int s, int e)

Uses of JmlLoopAnnotations in org.jmlspecs.jml4.fspv

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

void	TraceAstVisitor.endVisit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
void	TheoryTranslator.endVisit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
boolean	TraceAstVisitor.visit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
boolean	TheoryTranslator.visit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)

Uses of JmlLoopAnnotations in org.jmlspecs.jml4.fspv.phases

Methods in org.jmlspecs.jml4.fspv.phases with parameters of type JmlLoopAnnotations

void	TheoryTranslation.endVisit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
boolean	TheoryTranslation.visit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)

Uses of JmlLoopAnnotations in org.jmlspecs.jml4.rac

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

void	JmlAstVisitor.endVisit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
void	DefaultRacAstVisitor.endVisit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
void	AstDirtyBitsRetriever.endVisit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
boolean	JmlAstVisitor.visit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
boolean	DefaultRacAstVisitor.visit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
boolean	AstDirtyBitsRetriever.visit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)