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

Packages that use JmlOldExpression

org.eclipse.jdt.internal.compiler
org.jmlspecs.jml4.fspv
org.jmlspecs.jml4.fspv.phases
org.jmlspecs.jml4.rac

Uses of JmlOldExpression in org.eclipse.jdt.internal.compiler

Methods in org.eclipse.jdt.internal.compiler with parameters of type JmlOldExpression

void	ASTVisitor.endVisit(JmlOldExpression jmlOldExpression, BlockScope scope)
boolean	ASTVisitor.visit(JmlOldExpression jmlOldExpression, BlockScope scope)

Uses of JmlOldExpression in org.jmlspecs.jml4.fspv

Methods in org.jmlspecs.jml4.fspv with parameters of type JmlOldExpression

void	TraceAstVisitor.endVisit(JmlOldExpression jmlOldExpression, BlockScope scope)
boolean	TraceAstVisitor.visit(JmlOldExpression jmlOldExpression, BlockScope scope)

Uses of JmlOldExpression in org.jmlspecs.jml4.fspv.phases

Methods in org.jmlspecs.jml4.fspv.phases with parameters of type JmlOldExpression

void	TheoryTranslation.endVisit(JmlOldExpression jmlOldExpression, BlockScope scope)
boolean	TheoryTranslation.visit(JmlOldExpression jmlOldExpression, BlockScope scope)

Uses of JmlOldExpression in org.jmlspecs.jml4.rac

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

void	JmlAstVisitor.endVisit(JmlOldExpression jmlOldExpression, BlockScope scope)
void	DefaultRacAstVisitor.endVisit(JmlOldExpression jmlOldExpression, BlockScope scope)
void	AstDirtyBitsRetriever.endVisit(JmlOldExpression jmlOldExpression, BlockScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlOldExpression jmlOldExpression, BlockScope scope)
boolean	JmlAstVisitor.visit(JmlOldExpression jmlOldExpression, BlockScope scope) Refers to the value that the expression had in the pre-state of a method.
boolean	DefaultRacAstVisitor.visit(JmlOldExpression jmlOldExpression, BlockScope scope)
boolean	AstDirtyBitsRetriever.visit(JmlOldExpression jmlOldExpression, BlockScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlOldExpression jmlOldExpression, BlockScope scope)