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

Packages that use JmlQuantifiedExpression

org.eclipse.jdt.internal.compiler
org.jmlspecs.jml4.esc.gc
org.jmlspecs.jml4.fspv
org.jmlspecs.jml4.rac
org.jmlspecs.jml4.rac.quantifiedexpression

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

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

void	ASTVisitor.endVisit(JmlQuantifiedExpression expr, BlockScope scope)
boolean	ASTVisitor.visit(JmlQuantifiedExpression expr, BlockScope scope)

Uses of JmlQuantifiedExpression in org.jmlspecs.jml4.esc.gc

Methods in org.jmlspecs.jml4.esc.gc with parameters of type JmlQuantifiedExpression

boolean

Ast2SugaredVisitor.visit(JmlQuantifiedExpression quantExpr, BlockScope scope)

Uses of JmlQuantifiedExpression in org.jmlspecs.jml4.fspv

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

void	TraceAstVisitor.endVisit(JmlQuantifiedExpression expr, BlockScope scope)
void	TheoryTranslator.endVisit(JmlQuantifiedExpression expr, BlockScope scope)
boolean	TraceAstVisitor.visit(JmlQuantifiedExpression expr, BlockScope scope)
boolean	TheoryTranslator.visit(JmlQuantifiedExpression expr, BlockScope scope)

Uses of JmlQuantifiedExpression in org.jmlspecs.jml4.rac

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

void	JmlAstVisitor.endVisit(JmlQuantifiedExpression jmlQuantifiedExpression, BlockScope blockScope)
void	DefaultRacAstVisitor.endVisit(JmlQuantifiedExpression jmlQuantifiedExpression, BlockScope blockScope)
void	AstDirtyBitsRetriever.endVisit(JmlQuantifiedExpression expr, BlockScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlQuantifiedExpression expr, BlockScope scope)
java.lang.String	ExpressionTranslator.translate(JmlQuantifiedExpression quantiExp, Expression expr, SourceTypeBinding typeBinding, RacResult racResult)
boolean	JmlAstVisitor.visit(JmlQuantifiedExpression jmlQuantifiedExpression, BlockScope blockScope)
boolean	DefaultRacAstVisitor.visit(JmlQuantifiedExpression jmlQuantifiedExpression, BlockScope blockScope)
boolean	AstDirtyBitsRetriever.visit(JmlQuantifiedExpression expr, BlockScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlQuantifiedExpression expr, BlockScope scope)

Uses of JmlQuantifiedExpression in org.jmlspecs.jml4.rac.quantifiedexpression

Methods in org.jmlspecs.jml4.rac.quantifiedexpression with parameters of type JmlQuantifiedExpression

static StaticAnalysis

StaticAnalysis.getInstance(VariableGenerator varGen, RacContext ctx, JmlQuantifiedExpression expr, java.lang.String resultVar, PostStateExpressionTranslator transExp, RacResult racResult, SourceTypeBinding typeBinding) Returns an instance of StaticAnalysis, that translates JML quantified expressions into Java source code.

Constructors in org.jmlspecs.jml4.rac.quantifiedexpression with parameters of type JmlQuantifiedExpression

QuantifiedExpressionTranslator(VariableGenerator varGen, RacContext context, JmlQuantifiedExpression expr, java.lang.String resultVar, PostStateExpressionTranslator transExp, RacResult racResult, SourceTypeBinding typeBinding)
Constructs a new instance.