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

Packages that use JmlResultReference

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

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

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

void	ASTVisitor.endVisit(JmlResultReference resultReference, BlockScope scope)
boolean	ASTVisitor.visit(JmlResultReference resultReference, BlockScope scope)

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

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

boolean

PrintVisitor.visit(JmlResultReference resultReference, BlockScope scope) Deprecated.

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

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

boolean

Ast2SugaredVisitor.visit(JmlResultReference resRef, BlockScope scope)

Uses of JmlResultReference in org.jmlspecs.jml4.fspv

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

void	TraceAstVisitor.endVisit(JmlResultReference resultReference, BlockScope scope)
void	TheoryTranslator.endVisit(JmlResultReference resultReference, BlockScope scope)
boolean	TraceAstVisitor.visit(JmlResultReference resultReference, BlockScope scope)
boolean	TheoryTranslator.visit(JmlResultReference resultReference, BlockScope scope)

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

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

void	TheoryTranslation.endVisit(JmlResultReference resultReference, BlockScope scope)
boolean	TheoryTranslation.visit(JmlResultReference resultReference, BlockScope scope)

Uses of JmlResultReference in org.jmlspecs.jml4.rac

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

void	JmlNullifier.endVisit(JmlResultReference resultReference, BlockScope scope)
void	JmlAstVisitor.endVisit(JmlResultReference resultReference, BlockScope scope)
void	DefaultRacAstVisitor.endVisit(JmlResultReference resultReference, BlockScope scope)
void	AstDirtyBitsRetriever.endVisit(JmlResultReference resultReference, BlockScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlResultReference resultReference, BlockScope scope)
boolean	JmlNullifier.visit(JmlResultReference resultReference, BlockScope scope)
boolean	JmlAstVisitor.visit(JmlResultReference resultReference, BlockScope scope) The primary \result can only be used in non-void method.
boolean	DefaultRacAstVisitor.visit(JmlResultReference resultReference, BlockScope scope)
boolean	AstDirtyBitsRetriever.visit(JmlResultReference resultReference, BlockScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlResultReference resultReference, BlockScope scope)