Uses of Class
org.jmlspecs.jml4.ast.JmlSignalsClause

Packages that use JmlSignalsClause

org.jmlspecs.jml4.rac

Uses of JmlSignalsClause in org.jmlspecs.jml4.rac

Methods in org.jmlspecs.jml4.rac with parameters of type JmlSignalsClause

void	JmlAstVisitor.endVisit(JmlSignalsClause jmlSignalsClause, BlockScope scope)
void	DefaultRacAstVisitor.endVisit(JmlSignalsClause jmlSignalsClause, BlockScope scope)
void	AstDirtyBitsRetriever.endVisit(JmlSignalsClause jmlSignalsClause, BlockScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlSignalsClause jmlSignalsClause, BlockScope scope)
boolean	JmlAstVisitor.visit(JmlSignalsClause jmlSignalsClause, BlockScope scope) Specifies the exceptional or abnormal postcondition, i.e., the property that is guaranteed to hold at the end of a method (or constructor) invocation when this method (or constructor) invocation terminates abruptly by throwing a given exception.
boolean	DefaultRacAstVisitor.visit(JmlSignalsClause jmlSignalsClause, BlockScope scope)
boolean	AstDirtyBitsRetriever.visit(JmlSignalsClause jmlSignalsClause, BlockScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlSignalsClause jmlSignalsClause, BlockScope scope)