Uses of Class
org.jmlspecs.checker.JmlRequiresClause

Packages that use JmlRequiresClause

org.jmlspecs.checker	Contains the source code for a parser and typechecker for JML annotations and java code.
org.jmlspecs.jmldoc.jmldoc_142
org.jmlspecs.jmlrac	Generates Java classes from JML specifications that check assertions at runtime.

Uses of JmlRequiresClause in org.jmlspecs.checker

Fields in org.jmlspecs.checker declared as JmlRequiresClause

protected JmlRequiresClause[]	JmlGeneralSpecCase.specHeader
private JmlRequiresClause[]	JmlExample.specHeader

Methods in org.jmlspecs.checker that return JmlRequiresClause

JmlRequiresClause[]	JmlGeneralSpecCase.specHeader()
JmlRequiresClause[]	JmlExample.specHeader()
JmlRequiresClause[]	JmlParser.jmlSpecHeader()
JmlRequiresClause	JmlParser.jmlRequiresClause()
protected JmlRequiresClause	TestJmlParser.Helper.getRequiresClause(String sourceCode)

Methods in org.jmlspecs.checker with parameters of type JmlRequiresClause

void	JmlAbstractVisitor.visitJmlRequiresClause(JmlRequiresClause self)
abstract void	JmlVisitor.visitJmlRequiresClause(JmlRequiresClause self)
void	JmlGeneralSpecCase.addRequiresClause(JmlRequiresClause req) Add the given requires clause to this specification case.
void	JmlVisitorNI.visitJmlRequiresClause(JmlRequiresClause self)

Constructors in org.jmlspecs.checker with parameters of type JmlRequiresClause

JmlGeneralSpecCase(TokenReference where, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlSpecBody specBody)
Creates a new JmlGeneralSpecCase instance.

JmlAbruptSpecCase(TokenReference sourceRef, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlAbruptSpecBody abruptSpecBody)

JmlExample(TokenReference where, long privacy, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlSpecBodyClause[] specBody)
Constructs a new instance with given arguments.

JmlExample(TokenReference where, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlSpecBodyClause[] specBody)
Constructs a new instance with given arguments.

JmlExceptionalExample(TokenReference where, long privacy, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlSpecBodyClause[] specClauses)
Constructs a new instance with given arguments.

JmlExceptionalSpecCase(TokenReference sourceRef, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlExceptionalSpecBody exceptionalSpecBody)

JmlGenericSpecCase(TokenReference sourceRef, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlGenericSpecBody genericSpecBody)

JmlNormalExample(TokenReference where, long privacy, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlSpecBodyClause[] specClauses)
Constructs a new instance with given arguments.

JmlNormalSpecCase(TokenReference sourceRef, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlNormalSpecBody normalSpecBody)

Uses of JmlRequiresClause in org.jmlspecs.jmldoc.jmldoc_142

Methods in org.jmlspecs.jmldoc.jmldoc_142 with parameters of type JmlRequiresClause

void	SpecWriter.visitJmlRequiresClause(JmlRequiresClause self)

Uses of JmlRequiresClause in org.jmlspecs.jmlrac

Methods in org.jmlspecs.jmlrac that return JmlRequiresClause

protected JmlRequiresClause

DesugarSpec.defaultRequiresClause(TokenReference where) Returns a default requires clause for an behavior spec case.

Methods in org.jmlspecs.jmlrac with parameters of type JmlRequiresClause

private JmlGenericSpecCase	DesugarSpec.add(JmlGenericSpecCase specCase, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader) Adds the given spec var decls, specVarDecls, and spec header, specHeader, to the spec case, specCase.
void	RacPrettyPrinter.visitJmlRequiresClause(JmlRequiresClause self) Prints a JML requires clause.