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

Packages that use JmlRequiresClause

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

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

void	ASTVisitor.endVisit(JmlRequiresClause requiresClause, BlockScope scope)
boolean	ASTVisitor.visit(JmlRequiresClause requiresClause, BlockScope scope)

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

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

boolean

PrintVisitor.visit(JmlRequiresClause requiresClause, BlockScope scope) Deprecated.

Uses of JmlRequiresClause in org.jmlspecs.jml4.ast

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

static JmlRequiresClause[]	JmlSpecCaseHeader.NoRequiresClauses
JmlRequiresClause[]	JmlSpecCaseHeader.requiresClauses

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

JmlSpecCaseHeader(JmlRequiresClause[] requires)

Uses of JmlRequiresClause in org.jmlspecs.jml4.fspv

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

void	TraceAstVisitor.endVisit(JmlRequiresClause requiresClause, BlockScope scope)
boolean	TraceAstVisitor.visit(JmlRequiresClause requiresClause, BlockScope scope)

Uses of JmlRequiresClause in org.jmlspecs.jml4.rac

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

JmlSpecCaseHeader	DesugarSpec.addRequiresClause(JmlSpecCaseBody bs, JmlRequiresClause req) Add the given requires clause to this specification case.
void	JmlAstVisitor.endVisit(JmlRequiresClause requiresClause, BlockScope scope)
void	DefaultRacAstVisitor.endVisit(JmlRequiresClause requiresClause, BlockScope scope)
void	AstDirtyBitsRetriever.endVisit(JmlRequiresClause requiresClause, BlockScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlRequiresClause requiresClause, BlockScope scope)
boolean	JmlAstVisitor.visit(JmlRequiresClause requiresClause, BlockScope scope) Specifies a precondition of method or constructor.
boolean	DefaultRacAstVisitor.visit(JmlRequiresClause requiresClause, BlockScope scope)
boolean	AstDirtyBitsRetriever.visit(JmlRequiresClause requiresClause, BlockScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlRequiresClause requiresClause, BlockScope scope)