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

Packages that use JmlLoopInvariant

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 JmlLoopInvariant in org.eclipse.jdt.internal.compiler

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

void	ASTVisitor.endVisit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)
boolean	ASTVisitor.visit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)

Uses of JmlLoopInvariant in org.jmlspecs.jml4.ast

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

static JmlLoopInvariant[]	JmlLoopAnnotations.EMPTY_INVARIANTS
JmlLoopInvariant[]	JmlLoopAnnotations.invariants

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

JmlLoopAnnotations(JmlLoopInvariant[] invariants)

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

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

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

boolean

Ast2SugaredVisitor.visit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)

Uses of JmlLoopInvariant in org.jmlspecs.jml4.fspv

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

void	TraceAstVisitor.endVisit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)
void	TheoryTranslator.endVisit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)
boolean	TraceAstVisitor.visit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)
boolean	TheoryTranslator.visit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)

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

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

void	TheoryTranslation.endVisit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)
boolean	TheoryTranslation.visit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)

Uses of JmlLoopInvariant in org.jmlspecs.jml4.rac

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

void	JmlAstVisitor.endVisit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)
void	DefaultRacAstVisitor.endVisit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)
void	AstDirtyBitsRetriever.endVisit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)
boolean	JmlAstVisitor.visit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope) Is used to help prove partial correctness of a loop statement.
boolean	DefaultRacAstVisitor.visit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)
boolean	AstDirtyBitsRetriever.visit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)