Uses of Class
org.jmlspecs.checker.JmlGenericSpecCase

Packages that use JmlGenericSpecCase

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 JmlGenericSpecCase in org.jmlspecs.checker

Methods in org.jmlspecs.checker that return JmlGenericSpecCase

JmlGenericSpecCase[]	JmlGenericSpecBody.genericSpecCases()
JmlGenericSpecCase	JmlParser.jmlGenericSpecCase(boolean isInSpecStatement)
JmlGenericSpecCase[]	JmlParser.jmlGenericSpecCaseSeq(boolean isInSpecStatement)
protected JmlGenericSpecCase	TestJmlParser.Helper.getGenericSpecCase(String sourceCode)
protected JmlGenericSpecCase	TestJmlParser.Helper.getGenericSpecStatementCase(String sourceCode)

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

void	JmlAbstractVisitor.visitJmlGenericSpecCase(JmlGenericSpecCase self)
abstract void	JmlVisitor.visitJmlGenericSpecCase(JmlGenericSpecCase self)
void	JmlVisitorNI.visitJmlGenericSpecCase(JmlGenericSpecCase self)
void	JmlAccumSubclassingInfo.visitJmlGenericSpecCase(JmlGenericSpecCase self)

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

JmlGenericSpecBody(JmlGenericSpecCase[] specCases)

Uses of JmlGenericSpecCase in org.jmlspecs.jmldoc.jmldoc_142

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

void	SpecWriter.visitJmlGenericSpecCase(JmlGenericSpecCase self)
void	SpecWriter.visitJmlNormalSpecCase(JmlGenericSpecCase self)
void	SpecWriter.visitJmlExceptionalSpecCase(JmlGenericSpecCase self)

Uses of JmlGenericSpecCase in org.jmlspecs.jmlrac

Methods in org.jmlspecs.jmlrac that return JmlGenericSpecCase

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.

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

void	DesugarSpec.visitJmlGenericSpecCase(JmlGenericSpecCase self) Desugars a generic specification case.
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.visitJmlGenericSpecCase(JmlGenericSpecCase self) Prints a JML generic spec case.