org.jmlspecs.jml4.rac
Class ExpressionTranslator

java.lang.Object
  org.jmlspecs.jml4.rac.ExpressionTranslator

Direct Known Subclasses:

InlineAssertionTranslator, InvariantTranslator, PostStateExpressionTranslator

public class ExpressionTranslator
extends java.lang.Object

Translates various Java and JML expressions to RAC code. The translated code is also an expression; perhaps, this approach may not work for complex JML expressions such as quantifiers which are currently not supported.

Author:

Amritam Sarcar and Yoonsik Cheon

Field Summary

java.util.List<java.lang.String>	localclassTransformation
java.util.Map<ASTNode,VariableBinding>	terms Terms of which values are to be reported upon an assertion violation.

Constructor Summary

ExpressionTranslator(VariableGenerator varGenerator)

ExpressionTranslator(VariableGenerator varGenerator, boolean isOn)

Method Summary

CodeBuffer	embedSpecCase(Expression e, SourceTypeBinding sourceTypeBinding, RacResult result, java.lang.String var, VariableGenerator varGen, CompilationResult compilationResult, RacConstants.Condition condition)
java.util.Map<ASTNode,VariableBinding>	getTerms() Returns a set of terms or values that can be printed upon an assertion violation to describe the program state.
boolean	isPresent(java.lang.String temp)
void	setEvaluatorPDef(java.lang.String str)
void	setEvaluatorPUse(java.lang.String str)
java.lang.String	translate(Expression expression)
java.lang.String	translate(Expression expression, RacResult result)
java.lang.String	translate(Expression expression, SourceTypeBinding type, RacResult result) Translates the given expression of the given type.
java.lang.String	translate(Expression expression, TypeDeclaration type, RacResult result) Translates the given expression of the given type.
java.lang.String	translate(JmlQuantifiedExpression quantiExp, Expression expr, SourceTypeBinding typeBinding, RacResult racResult)

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

terms

public java.util.Map<ASTNode,VariableBinding> terms

Terms of which values are to be reported upon an assertion violation.

localclassTransformation

public java.util.List<java.lang.String> localclassTransformation

Constructor Detail

ExpressionTranslator

public ExpressionTranslator(VariableGenerator varGenerator)

ExpressionTranslator

public ExpressionTranslator(VariableGenerator varGenerator,
                            boolean isOn)

Method Detail

translate

public java.lang.String translate(Expression expression,
                                  SourceTypeBinding type,
                                  RacResult result)

Translates the given expression of the given type. The returned value is a string representation of the translated expression, which is also an expression.

translate

public java.lang.String translate(JmlQuantifiedExpression quantiExp,
                                  Expression expr,
                                  SourceTypeBinding typeBinding,
                                  RacResult racResult)

translate

public java.lang.String translate(Expression expression,
                                  TypeDeclaration type,
                                  RacResult result)

Translates the given expression of the given type. The returned value is a string representation of the translated expression, which is also an expression.

translate

public java.lang.String translate(Expression expression,
                                  RacResult result)

translate

public java.lang.String translate(Expression expression)

getTerms

public java.util.Map<ASTNode,VariableBinding> getTerms()

Returns a set of terms or values that can be printed upon an assertion violation to describe the program state.

embedSpecCase

public CodeBuffer embedSpecCase(Expression e,
                                SourceTypeBinding sourceTypeBinding,
                                RacResult result,
                                java.lang.String var,
                                VariableGenerator varGen,
                                CompilationResult compilationResult,
                                RacConstants.Condition condition)

setEvaluatorPUse

public void setEvaluatorPUse(java.lang.String str)

setEvaluatorPDef

public void setEvaluatorPDef(java.lang.String str)

isPresent

public boolean isPresent(java.lang.String temp)