Uses of Class
org.jmlspecs.jmlrac.RacContext

Packages that use RacContext

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 RacContext in org.jmlspecs.jmlrac

Fields in org.jmlspecs.jmlrac declared as RacContext

protected RacContext	TransExpression.context Current translation context.
protected RacContext	TransExpression2.context Current translation context.

Methods in org.jmlspecs.jmlrac that return RacContext

static RacContext	RacContext.createPositive() Returns a new positive context.
static RacContext	RacContext.createNegative() Returns a new negative context.
static RacContext	RacContext.createNeutral() Returns a new neutral context.
static RacContext	RacContext.createOpposite(RacContext ctx) Returns a new context that has the opposite polarity to the given context, but with the same status.

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

static RacContext	RacContext.createOpposite(RacContext ctx) Returns a new context that has the opposite polarity to the given context, but with the same status.
protected TransPostcondition	TransMethod.createPostconditionTranslator(VarGenerator postVarGen, RacContext ctx, VarGenerator preVarGen, boolean isStatic, JExpression pred, String var) Creates an appropriate postcondition translator.
private RacNode	TransExpression.guardUndefined(RacContext ctx, RacNode stmt, CType restype, String resvar, String demvar, String angvar)
protected RacNode	TransExpression.guardUndefined(RacContext ctx, RacNode stmt, String var) Returns a new RacNode that wraps the given statement, stmt, inside a try-catch statement to guard against undefinedness caused by runtime exceptions and non-executable expression.

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

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.

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.

Uses of RacContext in org.jmlspecs.jmlrac.qexpr

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

protected RacContext	Translator.context current translation context
private RacContext	TransQuantifiedExpression.context Current translation context.

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

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 RacContext

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.