Uses of Interface
org.jmlspecs.jmlrac.RacNode

Packages that use RacNode

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

Classes in org.jmlspecs.jmlrac that implement RacNode

static class	RacParser.RacBlock A RAC node class for representing blocks.
static class	RacParser.RacMethodDeclaration A RAC node class for representing method declarations.
static class	RacParser.RacStatement A RAC node class for representing statements.

Fields in org.jmlspecs.jmlrac declared as RacNode

RacNode	TransExpression.StringAndNodePair.node
RacNode	TransExpression.DynamicCallArg.node
private RacNode	TransInterface.invMethod Invariant check methods for the current interface.
private RacNode	TransInterface.hcMethod History constraint check methods for the current interface.

Methods in org.jmlspecs.jmlrac that return RacNode

RacNode	TransInvariant.translate(JmlInvariant[] invariants) Generates both static and instance invariant check methods and return them.
private RacNode	TransInvariant.translate(JmlInvariant[] invariants, boolean forStatic) Generates and returns a static or an instance invariant check method for the given invariant clauses, invariants.
abstract RacNode	RacNode.incrIndent() Increments indentation level of this node .
private RacNode	LocalConstraintMethod.isApplicable(JmlMethodName[] names) Returns code that tests if the given JML method name, name, is applicable to the method name given as a parameter (rac$name and rac$params) to the constraint check method.
(package private) RacNode	PreValueVars.saveCode() Returns a piece of code that, if executed, saves the values of private fields contained in this object into local temporary variables.
(package private) RacNode	PreValueVars.restoreCode() Return a piece of code that, if executed, restored the values of private fields contained in this object from their corresponding local temporary variables.
(package private) RacNode	PreValueVars.saveCode(String var)
(package private) RacNode	PreValueVars.restoreCode(String var)
RacNode	RacParser.RacMethodDeclaration.incrIndent()
RacNode	RacParser.RacStatement.incrIndent()
RacNode	RacParser.RacBlock.incrIndent()
protected RacNode	TransMethod.translateSignalsClause(VarGenerator varGen, VarGenerator oldVarGen, JmlSignalsClause sigClause, String preVar, RacNode stmt, List oldExprs) Translates the given signals clause.
RacNode	TransConstraint.translate(JmlConstraint[] constraints) Translates the given history constraints, constraints, and returns the translation result.
private RacNode	TransConstraint.constraintMethod(JmlConstraint[] constraints, boolean forStatic) Returns a static or an instance constraint check method for the given history constraints, constraints.
private RacNode	TransConstraint.constraintMethod(JmlConstraint constraint, int cnt) Returns a constraint check method for the given hisotry constraint, constraint.
private RacNode	TransConstraint.constraintMethod(boolean forStatic, int cnt, JExpression pred, JmlMethodName[] names) Returns a constraint check method that checks the given predicate, pred as a hisotry constraint.
private RacNode	TransConstraint.oldMethod(List exprs, boolean forStatic) Returns an old-expression evaluation method for the given old expressions, exprs.
private RacNode	TransConstraint.genStackMethods(boolean forStatic, String stackVar, List oldExprs) Returns a private stack field declaration with a pair of push and pop methods.
private RacNode	TransMethodBody.invariantCheckCode(JmlLoopInvariant[] invs) Returns code that checks the given loop invariants.
private RacNode	TransMethodBody.variantCheckCode(JmlVariantFunction[] vars) Returns code that checks the given loop variants.
private RacNode	TransMethodBody.ghostFieldSetter(JClassFieldExpression fieldExpr, String argVar) 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.
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.
RacNode	TransExpression.stmt() Returns the result of translating the expression.
RacNode	TransExpression.wrappedStmt(String eval, String nval) Returns the result of translating the expression wrapped in a try-catch statement to assign the given default values if an exception or non-executability happens while evaluating the expression.
private RacNode	TransExpression.translatePrimitiveType(CType type, String var) Translates the given primitive type.
protected RacNode	TransExpression.wrapBooleanResult(RacNode argEval, String stmt, String resVar, String demVar, String angVar)
protected RacNode	TransExpression.wrapBooleanResultTC(RacNode argEval, String stmt, String resVar, String demVar, String angVar)
private RacNode	TransExpression.checkUndefined(String demvar, String angvar)
private RacNode	TransExpression.guardUndefined(RacContext ctx, RacNode stmt, CType restype, String resvar, String demvar, String angvar)
protected RacNode	TransExpression.transPrefix(JExpression prefix, String format) Translates a prefix of a field or method call expression, build a RacNode using the given format, and return the result.
protected RacNode	TransExpression.transPrefixSpec(JExpression prefix, String format, boolean addDelegee)
private RacNode	TransExpression.receiverForDynamicCall(JExpression expr) Returns the receiver for executing the given expression, expr using a dynamic call.
private RacNode	TransExpression.transFieldReference(JClassFieldExpression self, String resultVar, String accPrefix) Translates a class field expression that references a model, ghost, spec_public, or spec_protected field.
protected RacNode	TransExpression.translate(JPhylum node, String var) Translates an AST into Java statements.
protected RacNode	TransExpression.translate(JPhylum node, String resvar, String demvar, String angvar) Translates an AST into Java statements.
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.
RacNode	TransExpression2.stmt(boolean wrapped) Returns the result of translating the expression.
protected RacNode	TransExpression2.wrap(RacNode node)
RacNode	TransExpression2.addPrebuiltNode(RacNode initial)
private RacNode	TransExpressionSideEffect.assignStmt(JExpression expr, String var) Generates a statement that assigns the value of var to expr.
private RacNode	TransInterface.concreteMethods() Returns concrete method declarations, often called delegation methods, that implements the abstract methods declared in the interface (and its super-interfaces).
RacNode	TransPredicate.wrappedStmt() Returns the result of translating the expression wrapped in a try-catch statement to assign the given default values if an exception or non-executability happens while evaluating the expression.

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

abstract JMethodDeclarationType	AssertionMethod.generate(RacNode stmt) Generates and returns an assertion checking method.
protected String	AssertionMethod.checker(boolean initValue, RacNode stmt, JFormalParameter[] params) Returnd the assertion check code (stmt) wrapped with code to inherit superclass's assertions if any, and to signal an assertion violation if it happens at runtime.
void	RacAbstractVisitor.visitRacNode(RacNode self) Visits the given RAC node, self.
abstract void	RacVisitor.visitRacNode(RacNode self) Visits the given RAC node, self.
JMethodDeclarationType	InvariantLikeMethod.generate(RacNode stmt) Generate and return a type-level assertion check method such as invariants and history constraints.
JMethodDeclarationType	PostconditionMethod.generate(RacNode stmt) Generate and return a postcondition checking method.
JMethodDeclarationType	ExceptionalPostconditionMethod.generate(RacNode stmt) Returns an exceptional postcondition checking method.
JMethodDeclarationType	LocalConstraintMethod.generate(RacNode stmt) Generates a constrain check method by using the given block of code, stmt, as the main body.
JMethodDeclarationType	MotherConstraintMethod.generate(RacNode stmt) Returns a constraint check method with the given body, stmt.
protected String	MotherConstraintMethod.checker(boolean initValue, RacNode stmt, JFormalParameter[] params) Returns the given constraint check code, stmt, wrapped with code to inherit supertypes's constraints.
JMethodDeclarationType	PreconditionMethod.generate(RacNode stmt)
JMethodDeclarationType	PreconditionMethod.generate(RacNode stmt, List preExprs) Generates and returns a precondition checking method.
protected String	PreconditionMethod.checker(boolean start, RacNode stmt, JFormalParameter[] params) Returns the precondition check code (stmt) wrapped with code to inherit superclass's preconditions if any, and to signal an assertion violation if it happens at runtime.
void	RacPrettyPrinter.visitRacNode(RacNode self) Prints a given RacNode.
protected String	SubtypeConstraintMethod.checker(boolean initValue, RacNode stmt, JFormalParameter[] params) Returns the local constraint check code (stmt) wrapped with code to inherit supertypes's constraints.
protected RacNode	TransMethod.translateSignalsClause(VarGenerator varGen, VarGenerator oldVarGen, JmlSignalsClause sigClause, String preVar, RacNode stmt, List oldExprs) Translates the given signals clause.
private void	TransMethodBody.transWhileLoop(JmlLoopStatement self, RacNode checkInv, RacNode checkVar) Translates the given JML loop statement with the given invariant check code and variant check code.
private void	TransMethodBody.transDoLoop(JmlLoopStatement self, RacNode checkInv, RacNode checkVar) Translates the given JML loop statement with the given invariant check code and variant check code.
private void	TransMethodBody.transForLoop(JmlLoopStatement self, RacNode checkInv, RacNode checkVar) Translates the given JML loop statement with the given invariant check code and variant check code.
protected RacNode	TransExpression.wrapBooleanResult(RacNode argEval, String stmt, String resVar, String demVar, String angVar)
protected RacNode	TransExpression.wrapBooleanResultTC(RacNode argEval, String stmt, String resVar, String demVar, String angVar)
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.
protected RacNode	TransExpression2.wrap(RacNode node)
RacNode	TransExpression2.addPrebuiltNode(RacNode initial)
private void	TransInterface.genSurrogateClass(RacNode newFdecls, RacNode newMdecls) Generates a surrogate class for the interface declaration being translated.
protected String	TransInterface.surrogatePlaceHolders(RacNode newFdecls, RacNode newMdecls, RacNode mdecls) Returns a place holder string ($0...
protected Object[]	TransInterface.surrogatePlaceValues(RacNode newFdecls, RacNode newMdecls, RacNode mdecls) Returns an array of objects representing actual values for the place holder.

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

TransExpression.StringAndNodePair(String str, RacNode node)

TransExpression.DynamicCallArg(String types, String args, RacNode node)

Uses of RacNode in org.jmlspecs.jmlrac.qexpr

Methods in org.jmlspecs.jmlrac.qexpr that return RacNode

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.
abstract RacNode	Translator.translate() Translate a JML quantified expression into Java source code and return the result.
abstract RacNode	Translator.generateLoop(RacNode body) Returns a loop code that evaluates the given body with the quantified variable bound to each possible value of the range.
protected RacNode	Translator.transExpression(JExpression expr, String var) Returns code for evaluating expression expr and storing the result to the variable var.
RacNode	StaticAnalysis.translate() Translate a JML quantified expression into Java source code and return the result.
private RacNode	StaticAnalysis.translateForAll() Return Java source code for evaluating a JML quantified expression of a univeral quantifier.
private RacNode	StaticAnalysis.translateExists() Return Java source code for evaluating a JML quantified expression of an existential quantifier.
private RacNode	StaticAnalysis.translateSum() Return Java source code for evaluating a JML quantified expression of a generalized quantifier \sum.
private RacNode	StaticAnalysis.translateProduct() Return Java source code for evaluating a JML quantified expression of a generalized quantifier \product.
private RacNode	StaticAnalysis.translateMin() Return Java source code for evaluating a JML quantified expression of a generalized quantifier \min.
private RacNode	StaticAnalysis.translateMax() Return Java source code for evaluating a JML quantified expression of a generalized quantifier \max.
private RacNode	StaticAnalysis.translateNumOf() Returns code for evaluating numerical quantifiers\num_of.
private RacNode	StaticAnalysis.transForAllOrExists() Returns Java source code for evaluating the JML quantified expression, which is either a universal or existential quantifier.
private RacNode	StaticAnalysis.transSumOrProduct() Returns Java source code for evaluating the JML quantified expression, which is a generalized quantifier \sum or \product.
private RacNode	StaticAnalysis.transMinOrMax() Returns Java source code for evaluating the JML quantified expression, which is a generalized quantifier \min or \max.
RacNode	StaticAnalysis.generateLoop(RacNode body) Returns a loop code that evaluates the given body with the quantified variable bound to each possible value of the range.
protected abstract RacNode	StaticAnalysis.generateLoop(JVariableDefinition varDef, JExpression qexpr, String cond, RacNode result) Returns a loop code evaluating the body of the quantified predicate.
protected RacNode	StaticAnalysis.SetBased.generateLoop(JVariableDefinition varDef, JExpression qexpr, String cond, RacNode result) Returns Java source code for evaluating quantified expressions using the QSet-based translation.
protected RacNode	StaticAnalysis.IntervalBased.generateLoop(JVariableDefinition varDef, JExpression pred, String cond, RacNode result) Returns a loop code for evaluating quantified expressions using the interval-based analysis.
protected RacNode	StaticAnalysis.EnumerationBased.generateLoop(JVariableDefinition varDef, JExpression qexpr, String cond, RacNode result) Returns Java source code for evaluating quantified expressions using the QSet-based translation.
RacNode	TransQuantifiedExpression.translate() Translates a JML quantified expression into Java source code and return the translated code.
RacNode	TransQuantifiedExpression.generateLoop(RacNode node) Tanslates a JML quantified expression into Java source code that, if executed, evaluates the given statement, node for each combination of bound variables of the quantified expression.
private RacNode	TransQuantifiedExpression.nonExecutableQuantifiedExpression() Translates a non-executable quantified expression.

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

abstract RacNode	Translator.generateLoop(RacNode body) Returns a loop code that evaluates the given body with the quantified variable bound to each possible value of the range.
RacNode	StaticAnalysis.generateLoop(RacNode body) Returns a loop code that evaluates the given body with the quantified variable bound to each possible value of the range.
protected abstract RacNode	StaticAnalysis.generateLoop(JVariableDefinition varDef, JExpression qexpr, String cond, RacNode result) Returns a loop code evaluating the body of the quantified predicate.
protected RacNode	StaticAnalysis.SetBased.generateLoop(JVariableDefinition varDef, JExpression qexpr, String cond, RacNode result) Returns Java source code for evaluating quantified expressions using the QSet-based translation.
protected RacNode	StaticAnalysis.IntervalBased.generateLoop(JVariableDefinition varDef, JExpression pred, String cond, RacNode result) Returns a loop code for evaluating quantified expressions using the interval-based analysis.
protected RacNode	StaticAnalysis.EnumerationBased.generateLoop(JVariableDefinition varDef, JExpression qexpr, String cond, RacNode result) Returns Java source code for evaluating quantified expressions using the QSet-based translation.
RacNode	TransQuantifiedExpression.generateLoop(RacNode node) Tanslates a JML quantified expression into Java source code that, if executed, evaluates the given statement, node for each combination of bound variables of the quantified expression.