Uses of Class
org.jmlspecs.checker.JmlHenceByStatement

Packages that use JmlHenceByStatement

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

Uses of JmlHenceByStatement in org.jmlspecs.checker

Methods in org.jmlspecs.checker that return JmlHenceByStatement

JmlHenceByStatement

JmlParser.jmlHenceByStatement()

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

void	JmlAbstractVisitor.visitJmlHenceByStatement(JmlHenceByStatement self)
abstract void	JmlVisitor.visitJmlHenceByStatement(JmlHenceByStatement self)
void	JmlVisitorNI.visitJmlHenceByStatement(JmlHenceByStatement self)
void	JmlAccumSubclassingInfo.visitJmlHenceByStatement(JmlHenceByStatement self)

Uses of JmlHenceByStatement in org.jmlspecs.jmlrac

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

void	RacPrettyPrinter.visitJmlHenceByStatement(JmlHenceByStatement self) Prints a JML henceby statement.
private static boolean	TransMethodBody.isCheckable(JmlHenceByStatement clause) Returns true if the given hence_by statement is checkable.
void	TransMethodBody.visitJmlHenceByStatement(JmlHenceByStatement self) Translates the given JML hence_by and stores the translated assertion check code into the AST node.