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

Packages that use JmlLocalDeclaration

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

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

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

void	ASTVisitor.endVisit(JmlLocalDeclaration localDeclaration, BlockScope scope)
boolean	ASTVisitor.visit(JmlLocalDeclaration localDeclaration, BlockScope scope)

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

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

boolean

PrintVisitor.visit(JmlLocalDeclaration localDeclaration, BlockScope scope) Deprecated.

Uses of JmlLocalDeclaration in org.jmlspecs.jml4.ast

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

static JmlLocalDeclaration[]	JmlSpecCaseBody.NoLocalDeclarations
JmlLocalDeclaration	JmlMethodDeclaration.resultValue

Methods in org.jmlspecs.jml4.ast that return JmlLocalDeclaration

JmlLocalDeclaration[]	JmlSpecCaseBody.getForallVars()
JmlLocalDeclaration[]	JmlSpecCaseBody.getOldVars()

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

JmlSpecCaseBody(JmlLocalDeclaration[] forallVars, JmlLocalDeclaration[] oldVars, JmlSpecCaseHeader header, JmlSpecCaseRest rest)

JmlSpecCaseBody(JmlLocalDeclaration[] forallVars, JmlLocalDeclaration[] oldVars, JmlSpecCaseHeader header, JmlSpecCaseRest rest)

Uses of JmlLocalDeclaration in org.jmlspecs.jml4.fspv

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

void	TraceAstVisitor.endVisit(JmlLocalDeclaration localDeclaration, BlockScope scope)
boolean	TraceAstVisitor.visit(JmlLocalDeclaration localDeclaration, BlockScope scope)

Uses of JmlLocalDeclaration in org.jmlspecs.jml4.rac

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

void	JmlAstVisitor.endVisit(JmlLocalDeclaration localDeclaration, BlockScope scope)
void	DefaultRacAstVisitor.endVisit(JmlLocalDeclaration localDeclaration, BlockScope scope)
void	AstDirtyBitsRetriever.endVisit(JmlLocalDeclaration localDeclaration, BlockScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlLocalDeclaration localDeclaration, BlockScope scope)
boolean	JmlAstVisitor.visit(JmlLocalDeclaration localDeclaration, BlockScope scope)
boolean	DefaultRacAstVisitor.visit(JmlLocalDeclaration localDeclaration, BlockScope scope)
boolean	AstDirtyBitsRetriever.visit(JmlLocalDeclaration localDeclaration, BlockScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlLocalDeclaration localDeclaration, BlockScope scope)