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

Packages that use JmlLoopVariant

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

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

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

void	ASTVisitor.endVisit(JmlLoopVariant jmlLoopVariant, BlockScope scope)
boolean	ASTVisitor.visit(JmlLoopVariant jmlLoopVariant, BlockScope scope)

Uses of JmlLoopVariant in org.jmlspecs.jml4.ast

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

static JmlLoopVariant[]	JmlLoopAnnotations.EMPTY_VARIANTS
JmlLoopVariant[]	JmlLoopAnnotations.variants

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

JmlLoopAnnotations(JmlLoopInvariant[] invariants, JmlLoopVariant[] variants)

JmlLoopAnnotations(JmlLoopVariant[] variants)

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

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

boolean

Ast2SugaredVisitor.visit(JmlLoopVariant jmlLoopVariant, BlockScope scope)

Uses of JmlLoopVariant in org.jmlspecs.jml4.fspv

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

void	TraceAstVisitor.endVisit(JmlLoopVariant jmlLoopVariant, BlockScope scope)
void	TheoryTranslator.endVisit(JmlLoopVariant jmlLoopVariant, BlockScope scope)
boolean	TraceAstVisitor.visit(JmlLoopVariant jmlLoopVariant, BlockScope scope)
boolean	TheoryTranslator.visit(JmlLoopVariant jmlLoopVariant, BlockScope scope)

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

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

void	TheoryTranslation.endVisit(JmlLoopVariant jmlLoopVariant, BlockScope scope)
boolean	TheoryTranslation.visit(JmlLoopVariant jmlLoopVariant, BlockScope scope)

Uses of JmlLoopVariant in org.jmlspecs.jml4.rac

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

void	JmlAstVisitor.endVisit(JmlLoopVariant jmlLoopVariant, BlockScope scope)
void	DefaultRacAstVisitor.endVisit(JmlLoopVariant jmlLoopVariant, BlockScope scope)
void	AstDirtyBitsRetriever.endVisit(JmlLoopVariant jmlLoopVariant, BlockScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlLoopVariant jmlLoopVariant, BlockScope scope)
boolean	JmlAstVisitor.visit(JmlLoopVariant jmlLoopVariant, BlockScope scope) Is used to help prove termination of a loop statement.
boolean	DefaultRacAstVisitor.visit(JmlLoopVariant jmlLoopVariant, BlockScope scope)
boolean	AstDirtyBitsRetriever.visit(JmlLoopVariant jmlLoopVariant, BlockScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlLoopVariant jmlLoopVariant, BlockScope scope)