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

Packages that use JmlSpecCase

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

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

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

void	ASTVisitor.endVisit(JmlSpecCase jmlSpecCase, BlockScope scope)
boolean	ASTVisitor.visit(JmlSpecCase jmlSpecCase, BlockScope scope)

Uses of JmlSpecCase in org.jmlspecs.jml4.ast

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

static JmlSpecCase[]

JmlSpecCase.EMPTY_SPEC_CASE_ARRAY

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

JmlSpecCase[]	JmlMethodSpecification.getRedundantSpecCases()
JmlSpecCase[]	JmlMethodSpecification.getSpecCases()

Methods in org.jmlspecs.jml4.ast with parameters of type JmlSpecCase

void	JmlMethodSpecification.setRedundantSpecCases(JmlSpecCase[] redundantSpecCases)
void	JmlMethodSpecification.setSpecCases(JmlSpecCase[] specCases)

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

JmlMethodSpecification(JmlSpecCase[] specCases, JmlSpecCase[] impliedSpecCases, boolean isExtending)

JmlMethodSpecification(JmlSpecCase[] specCases, JmlSpecCase[] impliedSpecCases, boolean isExtending)

Uses of JmlSpecCase in org.jmlspecs.jml4.rac

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

void	JmlAstVisitor.endVisit(JmlSpecCase jmlSpecCase, BlockScope scope)
void	AstDirtyBitsRetriever.endVisit(JmlSpecCase jmlSpecCase, BlockScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlSpecCase jmlSpecCase, BlockScope scope)
boolean	JmlAstVisitor.visit(JmlSpecCase jmlSpecCase, BlockScope scope)
boolean	DesugarSpec.visit(JmlSpecCase jmlSpecCase, BlockScope scope)
boolean	AstDirtyBitsRetriever.visit(JmlSpecCase jmlSpecCase, BlockScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlSpecCase jmlSpecCase, BlockScope scope)
void	DesugarSpec.visitJmlBehaviorSpec(JmlSpecCase self) Desugars a behavior specification.
void	DesugarSpec.visitJmlExceptionalBehaviorSpec(JmlSpecCase self) Desugars an exceptional behavior specification.
void	DesugarSpec.visitJmlNormalBehaviorSpec(JmlSpecCase self) Desugars a normal behavior specification.