Uses of Class
org.jmlspecs.jml4.rac.VariableGenerator

Packages that use VariableGenerator

org.jmlspecs.jml4.rac
org.jmlspecs.jml4.rac.quantifiedexpression

Uses of VariableGenerator in org.jmlspecs.jml4.rac

Methods in org.jmlspecs.jml4.rac that return VariableGenerator

static VariableGenerator	VariableGenerator.forClass() Return a variable generator for classes
static VariableGenerator	VariableGenerator.forMethod(VariableGenerator varGen) Return a variable generator for methods

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

CodeBuffer	ExpressionTranslator.embedSpecCase(Expression e, SourceTypeBinding sourceTypeBinding, RacResult result, java.lang.String var, VariableGenerator varGen, CompilationResult compilationResult, RacConstants.Condition condition)
static MethodDeclarationTranslator	MethodDeclarationTranslator.forClass(JmlTypeDeclaration typeDecl, VariableGenerator varGen) Creates a translator for translating methods contained in the given type.
static MethodDeclarationTranslator	MethodDeclarationTranslator.forInterface(JmlTypeDeclaration typeDecl, VariableGenerator varGen, boolean tSpec) Creates a translator for translating methods contained in the given type.
static VariableGenerator	VariableGenerator.forMethod(VariableGenerator varGen) Return a variable generator for methods
java.lang.String	PostStateExpressionTranslator.translate(Expression expr, TypeBinding type, boolean isStaticExpr, VariableGenerator vgen, RacResult result) Translates the given expression of the given type.
MethodDeclaration	PostconditionTranslator.translate(JmlMethodSpecification methSpec, AbstractMethodDeclaration meth, java.util.List<java.lang.String> preVars, VariableGenerator vgen, RacResult result) Translates the postcondition of the given method or constructor and returns a postcondition check method.
MethodDeclaration	ExceptionalPostconditionTranslator.translate(JmlMethodSpecification methSpec, AbstractMethodDeclaration meth, java.util.List<java.lang.String> preVars, VariableGenerator vgen, RacResult result) Translates the exceptional precondition of the given method or constructor and returns an exceptional postcondition check method.
void	PreconditionTranslator.translate(JmlMethodSpecification methSpec, AbstractMethodDeclaration meth, VariableGenerator vgen, RacResult result) Translates the precondition of the given method into RAC code.

Constructors in org.jmlspecs.jml4.rac with parameters of type VariableGenerator

ConstraintTranslator(JmlTypeDeclaration type, VariableGenerator varGen)
Creates a new translator.

ConstructorBodyTranslator(CompilationUnitDeclaration source, VariableGenerator varGen)
Creates a new translator for translating constructor bodies of classes contained in the given compilation unit.

ExceptionalPostconditionTranslator(JmlTypeDeclaration sourceType, VariableGenerator varGen)
Creates a new postcondition translator for the given type.

ExpressionTranslator(VariableGenerator varGenerator)

ExpressionTranslator(VariableGenerator varGenerator, boolean isOn)

InlineAssertionTranslator(VariableGenerator varGen)

InvariantTranslator(VariableGenerator varGen)
Creates a new translator.

MethodBodyTranslator(CompilationUnitDeclaration source, VariableGenerator varGen)
Creates a new translator for the given compilation unit.

MethodSpecificationTranslator(JmlTypeDeclaration typeDecl, VariableGenerator varGen)
Creates a new translator for translating methods of the given type declaration that uses the given variable generator.

PostconditionTranslator(JmlTypeDeclaration sourceType, VariableGenerator varGen)
Creates a new postcondition translator for the given type.

PostStateExpressionTranslator(JmlTypeDeclaration sourceType, VariableGenerator varGenerator)

PostStateExpressionTranslator(VariableGenerator varGenerator, boolean isOn)

PreconditionTranslator(JmlTypeDeclaration sourceType, VariableGenerator varGen)
Creates a new precondition translator for the given type.

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

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

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.
java.lang.String	QInterval.translate(VariableGenerator varGen, java.lang.String lowerVar, java.lang.String upperVar, PostStateExpressionTranslator transExp) Return Java source code that, if executed, evaluates the quantfied interval, i.e., its lower and upper bound values.

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

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