Uses of Class
org.jmlspecs.checker.JmlGuardedStatement

Packages that use JmlGuardedStatement

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

Fields in org.jmlspecs.checker declared as JmlGuardedStatement

private JmlGuardedStatement[]

JmlNondetIfStatement.guardedStatements

Methods in org.jmlspecs.checker that return JmlGuardedStatement

JmlGuardedStatement[]	JmlNondetIfStatement.guardedStatements()
JmlGuardedStatement[]	JmlParser.jmlGuardedStatements()
JmlGuardedStatement	JmlParser.jmlGuardedStatement()
private JmlGuardedStatement	TestJmlParser.getGuardedStatementFrom(String sourceCode)

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

void	JmlAbstractVisitor.visitJmlGuardedStatement(JmlGuardedStatement self)
abstract void	JmlVisitor.visitJmlGuardedStatement(JmlGuardedStatement self)
void	JmlVisitorNI.visitJmlGuardedStatement(JmlGuardedStatement self)
void	JmlAccumSubclassingInfo.visitJmlGuardedStatement(JmlGuardedStatement self)

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

JmlNondetIfStatement(TokenReference where, JmlGuardedStatement[] guardedStatements, JStatement[] elseStatements, JavaStyleComment[] comments)

Uses of JmlGuardedStatement in org.jmlspecs.jmldoc.jmldoc_142

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

void	SpecWriter.visitJmlGuardedStatement(JmlGuardedStatement self)

Uses of JmlGuardedStatement in org.jmlspecs.jmlrac

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

void	RacPrettyPrinter.visitJmlGuardedStatement(JmlGuardedStatement self) Prints a JML guarded statement.
void	TransMethodBody.visitJmlGuardedStatement(JmlGuardedStatement self) Translates the given JML guarded statement.