Uses of Class
org.jmlspecs.checker.JmlGeneralSpecCase

Packages that use JmlGeneralSpecCase

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

Subclasses of JmlGeneralSpecCase in org.jmlspecs.checker

class	JmlAbruptSpecCase JmlAbruptSpecCase.java
class	JmlExceptionalSpecCase An AST node class for the JML exceptional-spec-case.
class	JmlGenericSpecCase An AST node class for the JML generic-spec-case.
class	JmlNormalSpecCase An AST node class for the JML normal-spec-case.

Fields in org.jmlspecs.checker declared as JmlGeneralSpecCase

protected JmlGeneralSpecCase[]	JmlSpecBody.specCases
private JmlGeneralSpecCase	JmlHeavyweightSpec.specCase
private JmlGeneralSpecCase	JmlSpecStatement.specCase

Methods in org.jmlspecs.checker that return JmlGeneralSpecCase

JmlGeneralSpecCase[]	JmlSpecBody.specCases()
JmlGeneralSpecCase	JmlHeavyweightSpec.specCase()
JmlGeneralSpecCase	JmlSpecStatement.specCase()
JmlGeneralSpecCase[]	JmlParser.jmlExceptionalSpecCaseSeq()
JmlGeneralSpecCase[]	JmlParser.jmlNormalSpecCaseSeq()
JmlGeneralSpecCase[]	JmlParser.jmlAbruptSpecCaseSeq()
private JmlGeneralSpecCase	TestJmlParser.getSpecCase(String sourceCode)

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

void	JmlAbstractVisitor.visitJmlGeneralSpecCase(JmlGeneralSpecCase self)
abstract void	JmlVisitor.visitJmlGeneralSpecCase(JmlGeneralSpecCase self)
void	JmlVisitorNI.visitJmlGeneralSpecCase(JmlGeneralSpecCase self)
void	JmlAccumSubclassingInfo.visitJmlGeneralSpecCase(JmlGeneralSpecCase self)

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

JmlSpecBody(JmlGeneralSpecCase[] specCases)

JmlAbruptSpecBody(JmlGeneralSpecCase[] specCases)

JmlHeavyweightSpec(TokenReference where, long privacy, JmlGeneralSpecCase specCase)

JmlBehaviorSpec(TokenReference where, long privacy, JmlGeneralSpecCase specCase)

JmlExceptionalBehaviorSpec(TokenReference where, long privacy, JmlGeneralSpecCase specCase)

JmlExceptionalSpecBody(JmlGeneralSpecCase[] specCases)

JmlNormalBehaviorSpec(TokenReference where, long privacy, JmlGeneralSpecCase specCase)

JmlNormalSpecBody(JmlGeneralSpecCase[] specCases)

JmlSpecStatement(TokenReference where, JmlGeneralSpecCase specCase, JavaStyleComment[] comments)
Construct a JMLSpecStatement.

Uses of JmlGeneralSpecCase in org.jmlspecs.jmldoc.jmldoc_142

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

void	SpecWriter.visitJmlGeneralSpecCase(JmlGeneralSpecCase self)
void	SpecWriter.visitJmlGeneralSpecCaseHelper(JmlGeneralSpecCase self, boolean indent)

Uses of JmlGeneralSpecCase in org.jmlspecs.jmlrac

Fields in org.jmlspecs.jmlrac declared as JmlGeneralSpecCase

private JmlGeneralSpecCase

TransMethod.GeneralSpecCase.spec The spec case whose specification clauses to be conjoined.

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

private void	DesugarSpec.visitSpecCase(JmlGeneralSpecCase self) Desugars a specification case (general, normal, exceptional).
void	RacPrettyPrinter.visitGeneralSpecCase(JmlGeneralSpecCase self) Prints the given general spec case.
void	RacPrettyPrinter.visitJmlGeneralSpecCase(JmlGeneralSpecCase self)

Constructors in org.jmlspecs.jmlrac with parameters of type JmlGeneralSpecCase

TransMethod.GeneralSpecCase(JmlGeneralSpecCase spec)
Constructs a new instance.