Uses of Class
org.jmlspecs.jmlrac.VarGenerator

Packages that use VarGenerator

org.jmlspecs.jmlrac	Generates Java classes from JML specifications that check assertions at runtime.
org.jmlspecs.jmlrac.qexpr	Translates JML quantified expressions into Java source code to evaluate them at runtime.

Uses of VarGenerator in org.jmlspecs.jmlrac

Subclasses of VarGenerator in org.jmlspecs.jmlrac

private static class	VarGenerator.VarGenForClass A variable generator for classes.
private static class	VarGenerator.VarGenForMethod A variable generator for methods.

Fields in org.jmlspecs.jmlrac declared as VarGenerator

private VarGenerator	TransInvariant.varGen variable generator to be used in the translation
private VarGenerator	LocalConstraintMethod.varGen The variable generator to be used in the translation.
protected VarGenerator	TransType.varGen Variable generator for generating fresh variable names.
protected VarGenerator	TransMethod.varGen for generating fresh variables needed in the generated Java code
private VarGenerator	TransConstraint.varGen The variable generator to be used in the translation.
protected VarGenerator	TransMethodBody.varGen variable generator to generate fresh local variables
protected VarGenerator	TransExpression.varGen Generator of unique variable names.
protected VarGenerator	TransExpression2.varGen Generator of unique variable names.
private VarGenerator	TransPostcondition.oldVarGen Variable generator to be used in the translation of old expression.
private VarGenerator	TransPostExpression2.oldVarGen Variable generator to be used in the translation of old expression.
private VarGenerator	VarGenerator.VarGenForMethod.forClass

Methods in org.jmlspecs.jmlrac that return VarGenerator

static VarGenerator	VarGenerator.forClass() Return a variable generator for classes
static VarGenerator	VarGenerator.forMethod(VarGenerator forcls) Return a variable generator for methods

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

static VarGenerator	VarGenerator.forMethod(VarGenerator forcls) Return a variable generator for methods
protected TransPostcondition	TransMethod.createPostconditionTranslator(VarGenerator postVarGen, RacContext ctx, VarGenerator preVarGen, boolean isStatic, JExpression pred, String var) Creates an appropriate postcondition translator.
protected List	TransMethod.translateSpecVarDecls(JmlSpecVarDecl[] varDecls, VarGenerator varGen) Translates specification variable declarations.
protected List	TransMethod.translateLetVarDecl(JmlSpecVarDecl varDecl, VarGenerator varGen) Translates the given old variable declarations.
protected List	TransMethod.translateForAllVarDecl(JmlSpecVarDecl varDecl, VarGenerator varGen) Translates the given forall variable declarations.
protected RacNode	TransMethod.translateSignalsClause(VarGenerator varGen, VarGenerator oldVarGen, JmlSignalsClause sigClause, String preVar, RacNode stmt, List oldExprs) Translates the given signals clause.
private String	TransConstraint.evalSuperHC(VarGenerator varGen, boolean forStatic, CClass clazz) Return code that evaluates the old expressions of the given supertype, clazz, by making an appropriate call to its old expression evaluation method.
static RacNode	TransMethodBody.getGhostFieldSetter(JClassFieldExpression fieldExpr, String argVar, VarGenerator varGen) Returns Java source code that makes a dynamic call to the setter method of the given ghost field, fieldExpr, to set the ghost value to the value of the given variable, argVar.
private static RacNode	TransMethodBody.transPrefix(VarGenerator varGen, JClassFieldExpression fieldExpr) Translates the prefix expression of the given field reference expression, fieldExpr.

Constructors in org.jmlspecs.jmlrac with parameters of type VarGenerator

TransInvariant(JmlTypeDeclaration typeDecl, VarGenerator varGen)
Constructs a TransInvariant object.

LocalConstraintMethod(VarGenerator varGen, boolean isStatic, JmlTypeDeclaration typeDecl, JmlMethodName[] names, int suffix)
Construct a new instance.

TransMethod(JmlTypeDeclaration typeDecl, VarGenerator varGen)
Constructs a new TransMethod object.

TransConstraint(JmlTypeDeclaration typeDecl, VarGenerator varGen)
Constructs a TransConstraint object.

TransConstructor(JmlTypeDeclaration typeDecl, VarGenerator varGen)
Construct a new TransConstructor object.

TransMethodBody(VarGenerator varGen, JmlMethodDeclaration mdecl, JTypeDeclarationType typeDecl)
Construct an object of TransMethodBody.

TransConstructorBody(VarGenerator varGen, JmlMethodDeclaration mdecl, JTypeDeclarationType typeDecl)
Construct an object of TransConstructorBody.

TransExpression(VarGenerator varGen, RacContext ctx, JExpression expr, String resultVar, JTypeDeclarationType typeDecl)
Constructs an instance and translates the given expression.

TransExpression2(VarGenerator varGen, RacContext ctx, JExpression expr, String resultVar, JTypeDeclarationType typeDecl, String errorType)
Constructs an instance and translates the given expression.

TransExpressionSideEffect(VarGenerator varGen, RacContext ctx, JExpression expr, String resultVar, JTypeDeclarationType typeDecl)
Constructs an instance and translates the given expression.

TransExpressionSideEffect(VarGenerator varGen, JExpression expr, String resultVar, JTypeDeclarationType typeDecl)
Constructs an instance and translates the given expression.

TransPredicate(VarGenerator varGen, RacContext ctx, JExpression pred, String resultVar, JTypeDeclarationType typeDecl)
Constructs a new instance.

TransPostcondition(VarGenerator varGen, RacContext ctx, VarGenerator oldVarGen, boolean forStatic, JExpression pred, String resultVar, JTypeDeclarationType typeDecl)
Constructs a new instance and translates the given postcondition, pred.

TransOldExpression(VarGenerator varGen, RacContext ctx, JExpression expr, String resultVar, JTypeDeclarationType typeDecl)
Construct an object of TransOldExpression.

TransPostExpression2(VarGenerator varGen, RacContext ctx, VarGenerator oldVarGen, boolean forStatic, JExpression pred, String resultVar, JTypeDeclarationType typeDecl, String errorType)
Constructs a new instance and translates the given post-expression.

VarGenerator.VarGenForMethod(VarGenerator forClass)

Uses of VarGenerator in org.jmlspecs.jmlrac.qexpr

Fields in org.jmlspecs.jmlrac.qexpr declared as VarGenerator

protected VarGenerator	Translator.varGen variable generator for generating unique local variables
private VarGenerator	TransQuantifiedExpression.varGen variable generator for generating unique local variables.

Methods in org.jmlspecs.jmlrac.qexpr with parameters of type VarGenerator

private RacNode	QInterval.transLBound(VarGenerator varGen, String var, AbstractExpressionTranslator transExpr, QInterval.Bound bound) Returns code that evaluates the given lower bound.
private RacNode	QInterval.transUBound(VarGenerator varGen, String var, AbstractExpressionTranslator transExpr, QInterval.Bound bound) Returns code that evaluates the given upper bound.
private RacNode	QInterval.transBound(VarGenerator varGen, String var, AbstractExpressionTranslator transExp, QInterval.Bound bound, int opr) Returns code that evaluates the given lower or upper bound.
RacNode	QInterval.translate(VarGenerator varGen, String lowerVar, String upperVar, AbstractExpressionTranslator transExp) Return Java source code that, if executed, evaluates the quantfied interval, i.e., its lower and upper bound values.
abstract RacNode	QSet.translate(VarGenerator varGen, String resultVar, AbstractExpressionTranslator transExp) Returns Java source code that computes the qset represented by this object.
RacNode	QSet.Top.translate(VarGenerator varGen, String resultVar, AbstractExpressionTranslator transExp) Return Java source code that computes the qset represented by this object.
RacNode	QSet.Leaf.translate(VarGenerator varGen, String resultVar, AbstractExpressionTranslator transExp) Return Java source code that computes the qset represented by this object.
RacNode	QSet.Union.translate(VarGenerator varGen, String resultVar, AbstractExpressionTranslator transExp) Return Java source code that computes the qset represented by this object.
RacNode	QSet.Intersection.translate(VarGenerator varGen, String resultVar, AbstractExpressionTranslator transExp) Return Java source code that computes the qset represented by this object.
static StaticAnalysis	StaticAnalysis.getInstance(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp) Returns an instance of StaticAnalysis, that translates JML quantified expressions into Java source code.

Constructors in org.jmlspecs.jmlrac.qexpr with parameters of type VarGenerator

Translator(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)
Construct a TransQuantifiedExpression object.

StaticAnalysis(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)
Constructs a StaticAnalysis object.

StaticAnalysis.SetBased(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)
Constructs a SetBased object.

StaticAnalysis.IntervalBased(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)
Constructs a IntervalBased object.

StaticAnalysis.EnumerationBased(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)
Constructs a EnumerationBased object.

TransQuantifiedExpression(VarGenerator varGen, RacContext context, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)
Constructs a new instance.