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

Packages that use JmlSpecCaseHeader

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

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

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

void	ASTVisitor.endVisit(JmlSpecCaseHeader jmlSpecCaseHeader, BlockScope scope)
boolean	ASTVisitor.visit(JmlSpecCaseHeader jmlSpecCaseHeader, BlockScope scope)

Uses of JmlSpecCaseHeader in org.jmlspecs.jml4.ast

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

JmlSpecCaseHeader

JmlSpecCaseBody.header

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

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

Uses of JmlSpecCaseHeader in org.jmlspecs.jml4.rac

Methods in org.jmlspecs.jml4.rac that return JmlSpecCaseHeader

JmlSpecCaseHeader

DesugarSpec.addRequiresClause(JmlSpecCaseBody bs, JmlRequiresClause req) Add the given requires clause to this specification case.

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

void	JmlAstVisitor.endVisit(JmlSpecCaseHeader jmlSpecCaseHeader, BlockScope scope)
void	AstDirtyBitsRetriever.endVisit(JmlSpecCaseHeader jmlSpecCaseHeader, BlockScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlSpecCaseHeader jmlSpecCaseHeader, BlockScope scope)
boolean	JmlAstVisitor.visit(JmlSpecCaseHeader jmlSpecCaseHeader, BlockScope scope) Method specification for checking precondition of method or constructor.
boolean	AstDirtyBitsRetriever.visit(JmlSpecCaseHeader jmlSpecCaseHeader, BlockScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlSpecCaseHeader jmlSpecCaseHeader, BlockScope scope)