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

Packages that use RacResult

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

Uses of RacResult in org.jmlspecs.jml4.rac

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

RacResult	RacResult.combine(RacResult racResult) Combines the argument to this and returns this result.
RacResult	MethodSpecificationTranslator.translate(AbstractMethodDeclaration meth) Translates the given method to RAC code.
RacResult	MethodDeclarationTranslator.translate(AbstractMethodDeclaration meth) Translates the given method to RAC code.
RacResult	MethodDeclarationTranslator.translate(MethodBinding meth) Translates the given method to RAC code.

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

RacResult	RacResult.combine(RacResult racResult) Combines the argument to this and returns this result.
CodeBuffer	ExpressionTranslator.embedSpecCase(Expression e, SourceTypeBinding sourceTypeBinding, RacResult result, java.lang.String var, VariableGenerator varGen, CompilationResult compilationResult, RacConstants.Condition condition)
MethodDeclaration	PreconditionMethod.generate(java.lang.StringBuffer stmt, java.util.Collection<RacOldExpression> preExprs, java.util.Set<ASTNode> terms, RacResult result) Generates and returns a precondition checking method.
RacMethodDeclaration	PreconditionMethod.generate(java.lang.StringBuffer stmt, java.util.Set<ASTNode> terms, RacResult result) Overridden here to throw an exception, as this method is not supported by this class.
MethodDeclaration	PostconditionMethod.generate(java.lang.StringBuffer stmt, java.util.Set<ASTNode> terms, RacResult result) Generate and return a postcondition checking method.
RacMethodDeclaration	InvariantLikeMethod.generate(java.lang.StringBuffer stmt, java.util.Set<ASTNode> terms, RacResult result) Generates an type-level assertion check method.
MethodDeclaration	ExceptionalPostconditionMethod.generate(java.lang.StringBuffer stmt, java.util.Set<ASTNode> terms, RacResult result) Returns an exceptional postcondition checking method.
abstract AbstractMethodDeclaration	AssertionMethod.generate(java.lang.StringBuffer code, java.util.Set<ASTNode> terms, RacResult racResult) Generates an assertion check method.
RacMethodDeclaration	ConstraintMethod.generate(java.lang.StringBuffer stmt, java.util.Set<ASTNode> terms, RacResult result, boolean inherit, boolean isTopLevelInstance, java.lang.String methodPrefix) Overridden method to generate a type-level constraint check method.
MethodDeclaration	PreconditionTranslator.getPreconditionMethod(java.util.Collection<RacOldExpression> oldExprs, RacResult racResult) Returns a precondition check method that also executes the given old expressions (in the pre-state).
java.lang.StringBuffer	InlineAssertionVisitor.translate(AbstractMethodDeclaration meth, RacResult result) Translates all in-line assertions contained in the body of the given method to RAC code in the AST visitor traversal order and return the translated RAC code.
java.lang.StringBuffer	InlineAssertionTranslator.translate(AbstractMethodDeclaration meth, RacResult result) Translates in-line assertions contained in the body of the given method to RAC code.
java.lang.String	ExpressionTranslator.translate(Expression expression, RacResult result)
java.lang.String	ExpressionTranslator.translate(Expression expression, SourceTypeBinding type, RacResult result) Translates the given expression of the given type.
java.lang.String	PostStateExpressionTranslator.translate(Expression expr, TypeBinding type, boolean isStaticExpr, VariableGenerator vgen, RacResult result) Translates the given expression of the given type.
java.lang.String	PreconditionTranslator.translate(Expression expression, TypeBinding type, RacResult result) Translates the given expression of the given type.
java.lang.String	PostconditionTranslator.translate(Expression expression, TypeBinding type, RacResult result) Translates the given expression of the given type.
java.lang.String	ExpressionTranslator.translate(Expression expression, TypeDeclaration type, RacResult result) Translates the given expression of the given type.
java.lang.StringBuffer	InlineAssertionVisitor.translate(Initializer initBlock, RacResult result) Translates all jml-assertion statements in Initializer blocks.
java.lang.StringBuffer	InlineAssertionTranslator.translate(Initializer initBlock, RacResult result)
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.
java.lang.String	ExpressionTranslator.translate(JmlQuantifiedExpression quantiExp, Expression expr, SourceTypeBinding typeBinding, RacResult racResult)
java.lang.StringBuffer	InlineAssertionVisitor.translate(Statement stmt, AbstractMethodDeclaration meth, RacResult result) Translates the given (in-line assertion) statement in the context of the given method and returns the translated RAC code.
java.util.List<AbstractMethodDeclaration>	TypeAssertionTranslator.translate(TypeDeclaration type, RacResult racResult)
java.util.List<AbstractMethodDeclaration>	InvariantTranslator.translate(TypeDeclaration type, RacResult result) Translates the invariant clauses of the given type to RAC code and returns a list of invariant checking methods.
java.util.List<AbstractMethodDeclaration>	ConstraintTranslator.translate(TypeDeclaration type, RacResult result) Translates the constraint clauses of the given type to RAC code and returns a list of constraint checking methods.
java.lang.StringBuffer	MethodBodyTranslator.translateInlineAssertions(AbstractMethodDeclaration sourceMethod, RacResult result) Translates all in-line assertions of sourceMethod to RAC code and attach them to targetMethod.
java.lang.StringBuffer	MethodBodyTranslator.translateInlineAssertions(Initializer initBlock, RacResult result)

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

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

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 RacResult

QInterval(Expression expr, java.lang.String var, java.util.Collection xvars, TypeBinding type, RacResult racResult, SourceTypeBinding typeBinding)
Construct a QInterval object representing the quantifed interval for a (quantified) variable var with respect to the expression expr.

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